From d6ec53aa6bc276448d70a93232ea3313288585fd Mon Sep 17 00:00:00 2001
From: Vasily Ilin <vasilin97@gmail.com>
Date: Sat, 25 Jul 2026 23:54:19 -0700
Subject: [PATCH] Formalize the McKay conjecture statement

---
 .github/workflows/mckay-conjecture-ci.yml     | 29 ++++++
 README.md                                     |  4 +
 mckay-conjecture/.gitignore                   | 10 ++
 mckay-conjecture/McKayConjecture.lean         |  1 +
 .../McKayConjecture/IrreducibleCharacter.lean | 80 ++++++++++++++++
 .../McKayConjecture/Statement.lean            | 40 ++++++++
 mckay-conjecture/README.md                    | 33 +++++++
 mckay-conjecture/lake-manifest.json           | 96 +++++++++++++++++++
 mckay-conjecture/lakefile.toml                | 16 ++++
 mckay-conjecture/lean-toolchain               |  1 +
 10 files changed, 310 insertions(+)
 create mode 100644 .github/workflows/mckay-conjecture-ci.yml
 create mode 100644 mckay-conjecture/.gitignore
 create mode 100644 mckay-conjecture/McKayConjecture.lean
 create mode 100644 mckay-conjecture/McKayConjecture/IrreducibleCharacter.lean
 create mode 100644 mckay-conjecture/McKayConjecture/Statement.lean
 create mode 100644 mckay-conjecture/README.md
 create mode 100644 mckay-conjecture/lake-manifest.json
 create mode 100644 mckay-conjecture/lakefile.toml
 create mode 100644 mckay-conjecture/lean-toolchain

diff --git a/.github/workflows/mckay-conjecture-ci.yml b/.github/workflows/mckay-conjecture-ci.yml
new file mode 100644
index 00000000..8f894649
--- /dev/null
+++ b/.github/workflows/mckay-conjecture-ci.yml
@@ -0,0 +1,29 @@
+name: McKay Conjecture CI
+
+on:
+  push:
+    paths:
+      - 'mckay-conjecture/**'
+      - '.github/workflows/mckay-conjecture-ci.yml'
+  pull_request:
+    paths:
+      - 'mckay-conjecture/**'
+      - '.github/workflows/mckay-conjecture-ci.yml'
+  workflow_dispatch:
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v5
+      - uses: leanprover/lean-action@v1
+        with:
+          lake-package-directory: mckay-conjecture
diff --git a/README.md b/README.md
index 0824f75f..3adb1555 100644
--- a/README.md
+++ b/README.md
@@ -21,6 +21,10 @@ This repository hosts two completed formalization projects. Each is a self-conta
 | **Paper** | [arXiv:2603.15929](https://arxiv.org/abs/2603.15929) · [HF paper](https://huggingface.co/papers/2603.15929) | [Technical report](grothendieck-vanishing/TECHNICAL_REPORT_GV.md) |
 | **Read more** | [README](landau/README.md) · [Technical report](landau/TECHNICAL_REPORT.md) · [Blueprint](https://vilin97.github.io/Clawristotle/landau/blueprint/) | [README](grothendieck-vanishing/README.md) · [Brian's review](grothendieck-vanishing/review.md) · [Blueprint](https://vilin97.github.io/Clawristotle/grothendieck-vanishing/blueprint/) |
 
+An additional project, [`mckay-conjecture/`](mckay-conjecture/), is in active
+development. Its first milestone is a compiled, adversarially audited Lean
+statement of the McKay conjecture for ordinary irreducible complex characters.
+
 ## How it works
 
 The human steers — choosing the theorem, fixing the definitions, auditing the final statement — while AI agents handle the implementation: writing the Lean code, searching for proofs, dispatching hard lemmas to the [Aristotle](https://aristotle.harmonic.fun/) cloud prover, and reviewing their own output in autonomous critique–plan–prove–simplify loops. Each project's README describes its agent stack and how the method evolved between the two projects.
diff --git a/mckay-conjecture/.gitignore b/mckay-conjecture/.gitignore
new file mode 100644
index 00000000..d24d644c
--- /dev/null
+++ b/mckay-conjecture/.gitignore
@@ -0,0 +1,10 @@
+/.lake/
+*.olean
+*.ilean
+*.log
+*.aux
+*.fdb_latexmk
+*.fls
+*.out
+*.pdf
+*.synctex.gz
diff --git a/mckay-conjecture/McKayConjecture.lean b/mckay-conjecture/McKayConjecture.lean
new file mode 100644
index 00000000..5ce9c773
--- /dev/null
+++ b/mckay-conjecture/McKayConjecture.lean
@@ -0,0 +1 @@
+import McKayConjecture.Statement
diff --git a/mckay-conjecture/McKayConjecture/IrreducibleCharacter.lean b/mckay-conjecture/McKayConjecture/IrreducibleCharacter.lean
new file mode 100644
index 00000000..5b6830f5
--- /dev/null
+++ b/mckay-conjecture/McKayConjecture/IrreducibleCharacter.lean
@@ -0,0 +1,80 @@
+/-
+Copyright (c) 2026 Clawristotle contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Clawristotle contributors
+-/
+import Mathlib.Data.Complex.Basic
+import Mathlib.RepresentationTheory.Character
+
+/-!
+# Ordinary irreducible complex characters
+
+This file packages an ordinary irreducible complex character together with its
+(natural-number-valued) degree.  The witness field ensures that the values and
+degree come from one simple finite-dimensional complex representation.
+-/
+
+noncomputable section
+
+open CategoryTheory
+
+universe u
+
+namespace McKayConjecture
+
+variable (G : Type u) [Group G]
+
+/-- An ordinary irreducible complex character of `G`.
+
+Equality is equality of the character values and degree, rather than equality
+of a chosen representation.  Thus isomorphic representations, and more
+generally any representations with the same character, determine the same
+element of this type.
+-/
+structure IrreducibleCharacter where
+  /-- The values of the character on elements of the group. -/
+  values : G → ℂ
+  /-- The character degree, equivalently the dimension of a realizing representation. -/
+  degree : ℕ
+  /-- A simple finite-dimensional complex representation realizing the data. -/
+  isIrreducible :
+    ∃ V : FDRep ℂ G,
+      Simple V ∧
+        V.character = values ∧
+          Module.finrank ℂ V = degree
+
+namespace IrreducibleCharacter
+
+variable {G}
+
+/-- Evaluating an irreducible character at the identity gives its degree. -/
+@[simp]
+theorem value_one (χ : IrreducibleCharacter G) : χ.values 1 = (χ.degree : ℂ) := by
+  obtain ⟨V, _, hvalues, hdegree⟩ := χ.isIrreducible
+  rw [← hvalues, FDRep.char_one, hdegree]
+
+/-- The character values determine the certified degree. -/
+theorem degree_eq_of_values_eq {χ ψ : IrreducibleCharacter G}
+    (hvalues : χ.values = ψ.values) : χ.degree = ψ.degree := by
+  apply Nat.cast_injective (R := ℂ)
+  rw [← χ.value_one, ← ψ.value_one, hvalues]
+
+/-- Irreducible characters are equal when their character functions are equal. -/
+@[ext]
+theorem ext {χ ψ : IrreducibleCharacter G} (hvalues : χ.values = ψ.values) : χ = ψ := by
+  have hdegree := degree_eq_of_values_eq hvalues
+  cases χ
+  cases ψ
+  simp_all
+
+/-- An irreducible character has `p'`-degree when `p` does not divide its degree. -/
+def IsPPrimeDegree (p : ℕ) (χ : IrreducibleCharacter G) : Prop :=
+  ¬p ∣ χ.degree
+
+end IrreducibleCharacter
+
+/-- The type denoted `Irr_{p'}(G)` in the McKay conjecture. -/
+def PPrimeIrreducibleCharacter (p : ℕ) :=
+  {χ : IrreducibleCharacter G // χ.IsPPrimeDegree p}
+
+end McKayConjecture
diff --git a/mckay-conjecture/McKayConjecture/Statement.lean b/mckay-conjecture/McKayConjecture/Statement.lean
new file mode 100644
index 00000000..5ea85cf9
--- /dev/null
+++ b/mckay-conjecture/McKayConjecture/Statement.lean
@@ -0,0 +1,40 @@
+/-
+Copyright (c) 2026 Clawristotle contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Clawristotle contributors
+-/
+import Mathlib.GroupTheory.Sylow
+import McKayConjecture.IrreducibleCharacter
+
+/-!
+# The McKay conjecture
+
+This file states the McKay conjecture for ordinary irreducible complex
+characters.  The cardinal equality is used directly, so its meaning does not
+silently collapse to `0 = 0` if a finiteness instance has not yet been built.
+-/
+
+noncomputable section
+
+universe u
+
+namespace McKayConjecture
+
+variable {G : Type u} [Group G]
+
+/-- The normalizer `N_G(P)` of a Sylow subgroup, regarded as a group in its own right. -/
+abbrev SylowNormalizer {p : ℕ} (P : Sylow p G) : Type u :=
+  Subgroup.normalizer (P : Set G)
+
+/-- The statement of the McKay conjecture for a finite group `G`, a prime `p`,
+and a Sylow `p`-subgroup `P`.
+
+It asserts that the irreducible complex characters of `G` whose degrees are
+not divisible by `p` and those of `N_G(P)` have the same cardinality.
+-/
+def Statement (G : Type u) [Finite G] [Group G] (p : ℕ) [Fact p.Prime]
+    (P : Sylow p G) : Prop :=
+  Cardinal.mk (PPrimeIrreducibleCharacter G p) =
+    Cardinal.mk (PPrimeIrreducibleCharacter (SylowNormalizer P) p)
+
+end McKayConjecture
diff --git a/mckay-conjecture/README.md b/mckay-conjecture/README.md
new file mode 100644
index 00000000..073b2e1e
--- /dev/null
+++ b/mckay-conjecture/README.md
@@ -0,0 +1,33 @@
+# The McKay Conjecture
+
+This Lean 4 package formalizes the statement of the McKay conjecture for
+ordinary irreducible complex characters.
+
+For a finite group `G`, a prime `p`, and a Sylow `p`-subgroup `P`, let
+`Irr_{p'}(G)` be the irreducible complex characters of `G` whose degrees are not
+divisible by `p`. The conjecture asserts
+
+```text
+|Irr_{p'}(G)| = |Irr_{p'}(N_G(P))|.
+```
+
+The package is pinned to mathlib commit
+`9cebae57f419f984d008f357605b2621a1d9f13b` (Lean `v4.33.0-rc1`), which was the
+tip of mathlib's `master` branch when the project was created on 2026-07-25.
+
+## Layout
+
+- `McKayConjecture/IrreducibleCharacter.lean` defines ordinary irreducible
+  complex characters and the `p'`-degree condition.
+- `McKayConjecture/Statement.lean` defines the Sylow normalizer and the
+  proposition `McKayConjecture.Statement`.
+
+## Build
+
+```bash
+lake exe cache get
+lake build
+```
+
+The first milestone contains only the audited proposition; it does not assume
+the conjecture as an axiom or hide an unfinished proof behind `sorry`.
diff --git a/mckay-conjecture/lake-manifest.json b/mckay-conjecture/lake-manifest.json
new file mode 100644
index 00000000..0970b402
--- /dev/null
+++ b/mckay-conjecture/lake-manifest.json
@@ -0,0 +1,96 @@
+{"version": "1.2.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover-community/mathlib4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "9cebae57f419f984d008f357605b2621a1d9f13b",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "9cebae57f419f984d008f357605b2621a1d9f13b",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "b1c4a69a7e247ab7df20460212001673d74f08c0",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "0498c7c070c143a3bf7379f4d99a2c63bb9d9715",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "18a90119a5d316358fde6c86e0ca24e59212e32c",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "b1436dc749e722c9920036b52cdc43b3451d0b69",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "57d3325be72a842920813bcb40f96a6f7393c185",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "ee41917ae11d38479fb8fb24745f7ca4bf0a784d",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "d60e6444e6fd881dfa077ff36e96de75753afa28",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "da07ca808b6718cb2aed14dba154e5a08b8f8ecf",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.33.0-rc1",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
+ "name": "«mckay-conjecture»",
+ "lakeDir": ".lake",
+ "fixedToolchain": false}
diff --git a/mckay-conjecture/lakefile.toml b/mckay-conjecture/lakefile.toml
new file mode 100644
index 00000000..a8fba6cb
--- /dev/null
+++ b/mckay-conjecture/lakefile.toml
@@ -0,0 +1,16 @@
+name = "mckay-conjecture"
+version = "0.1.0"
+defaultTargets = ["McKayConjecture"]
+
+[leanOptions]
+pp.unicode.fun = true
+relaxedAutoImplicit = false
+weak.linter.mathlibStandardSet = true
+
+[[require]]
+name = "mathlib"
+scope = "leanprover-community"
+rev = "9cebae57f419f984d008f357605b2621a1d9f13b"
+
+[[lean_lib]]
+name = "McKayConjecture"
diff --git a/mckay-conjecture/lean-toolchain b/mckay-conjecture/lean-toolchain
new file mode 100644
index 00000000..fd85b262
--- /dev/null
+++ b/mckay-conjecture/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.33.0-rc1