From f30e7d5cd38ae4663ec19e87ad8eb56c887df678 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 25 Sep 2026 17:21:10 +0000 Subject: [PATCH] feat: add the classification of finite simple groups to v2 Add a problem stating the classification of finite simple groups over the list constructed in Tau Ceti, and add it to the draft v2 set. This makes TauCeti a dependency: the root lakefile requires it before Mathlib so that Mathlib's transitive pins win, generated workspaces get the requires their problem imports (lean-eval-generator 2de7404), and CI gives each generated workspace the root manifest instead of re-resolving dependencies inside the shared package directory. Co-Authored-By: Claude Opus 5.5 (1M context) --- .github/workflows/ci.yml | 17 ++++---- EvalTools/RunEval.lean | 4 +- .../ClassificationFiniteSimpleGroups.lean | 43 +++++++++++++++++++ lake-manifest.json | 14 +++++- lakefile.toml | 11 ++++- .../classification_finite_simple_groups.toml | 17 ++++++++ manifests/sets/v2.toml | 1 + 7 files changed, 93 insertions(+), 14 deletions(-) create mode 100644 LeanEval/GroupTheory/ClassificationFiniteSimpleGroups.lean create mode 100644 manifests/problems/classification_finite_simple_groups.toml diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 975966bc..3e65d683 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -351,19 +351,18 @@ jobs: done fi - # Every workspace has the same pinned Mathlib dependency. Reuse the - # root cache with symlinks instead of cloning/decompressing it once - # and hard-link-walking ~13 GB hundreds of times. + # Every workspace requires a subset of the root's pinned dependencies + # (always Mathlib, plus e.g. TauCeti for problems that import it). + # Reuse the root cache with symlinks instead of cloning/decompressing + # it once and hard-link-walking ~13 GB hundreds of times, and give + # each workspace the root manifest, which pins all of them. Running + # `lake update` here instead could re-resolve transitive dependencies + # and check them out inside the shared package directory. for problem in "${selected[@]}"; do mkdir -p "generated/$problem/.lake" ln -s "$GITHUB_WORKSPACE/.lake/packages" \ "generated/$problem/.lake/packages" - done - first="${selected[0]}" - (cd "generated/$first" && lake update) - for problem in "${selected[@]:1}"; do - cp "generated/$first/lake-manifest.json" \ - "generated/$problem/lake-manifest.json" + cp lake-manifest.json "generated/$problem/lake-manifest.json" done build_args=() diff --git a/EvalTools/RunEval.lean b/EvalTools/RunEval.lean index c9deca4f..b98700bd 100644 --- a/EvalTools/RunEval.lean +++ b/EvalTools/RunEval.lean @@ -81,7 +81,7 @@ def runProblemTest (workspace : System.FilePath) : IO UInt32 := do def scoreProblems (root : System.FilePath) (problems : Array EvalProblemMetadata) (workspacesRoot : System.FilePath) : IO (Array ProblemScore) := do let toolchain ← IO.FS.readFile (root / "lean-toolchain") - let mathlibDep ← loadRootMathlibDependency root + let deps ← loadRootDependencies root let workspaceTest ← loadWorkspaceTestTemplate root let mut scores : Array ProblemScore := #[] for entry in problems do @@ -89,7 +89,7 @@ def scoreProblems (root : System.FilePath) (problems : Array EvalProblemMetadata for hole in entry.holes do let e ← extractOne root entry hole extracteds := extracteds.push e - let expectedFiles ← renderWorkspace root entry extracteds toolchain mathlibDep workspaceTest + let expectedFiles ← renderWorkspace root entry extracteds toolchain deps workspaceTest let workspace ← workspacePathForProblem root entry.id workspacesRoot let relDisplay := let wsStr := workspace.toString diff --git a/LeanEval/GroupTheory/ClassificationFiniteSimpleGroups.lean b/LeanEval/GroupTheory/ClassificationFiniteSimpleGroups.lean new file mode 100644 index 00000000..95945570 --- /dev/null +++ b/LeanEval/GroupTheory/ClassificationFiniteSimpleGroups.lean @@ -0,0 +1,43 @@ +import TauCeti.GroupTheory.SpecificGroups.CFSG.Classification +import EvalTools.Markers + +namespace LeanEval +namespace GroupTheory + +/-! +# The classification of finite simple groups + +Every finite simple group is isomorphic to one of: + +* a cyclic group of prime order; +* an alternating group `Aₙ` with `n ≥ 5`; +* a finite simple group of Lie type, from one of the sixteen families + `Aₙ(q)`, `²Aₙ(q)`, `Bₙ(q)`, `Cₙ(q)`, `Dₙ(q)`, `²Dₙ(q)`, `E₆(q)`, `²E₆(q)`, + `E₇(q)`, `E₈(q)`, `F₄(q)`, `G₂(q)`, `³D₄(q)`, `²B₂(2^(2m+1))`, + `²G₂(3^(2m+1))`, `²F₄(2^(2m+1))`, or the Tits group `²F₄(2)'`; +* one of the twenty-six sporadic groups. + +The list, and the groups on it, are those of the Tau Ceti project +(`TauCeti.CFSGIndex` and `TauCeti.CFSGIndex.Group`): the cyclic and alternating +entries are `Multiplicative (ZMod p)` and Mathlib's `alternatingGroup (Fin n)`; +each Lie-type entry is an explicit construction, the derived subgroup of the +fixed points of a Steinberg endomorphism modulo its centre; and each sporadic +entry is the group of an explicit finite presentation. The index carries the +conventional parameter ranges and excludes the small duplicates, following +Gorenstein, Lyons and Solomon and the ATLAS. + +The statement is exactly `TauCeti.ClassificationStatement`, spelled out. It asks +only that every finite simple group appear on the list, and does not ask for the +converse (that each listed group is finite and simple) or for the list to be +irredundant. +-/ + +/-- **The classification of finite simple groups.** -/ +@[eval_problem] +theorem classification_finite_simple_groups + (G : Type) [Group G] [Finite G] [IsSimpleGroup G] : + ∃ i : TauCeti.CFSGIndex, Nonempty (G ≃* i.Group) := by + sorry + +end GroupTheory +end LeanEval diff --git a/lake-manifest.json b/lake-manifest.json index 5274c739..771709cf 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "77373a539b31f8f304c852f288d7d8469cceebff", + "rev": "2de74049bd91d2c592e7009df8f5e5968599a272", "name": "«lean-eval-generator»", "manifestFile": "lake-manifest.json", - "inputRev": "77373a539b31f8f304c852f288d7d8469cceebff", + "inputRev": "2de74049bd91d2c592e7009df8f5e5968599a272", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", @@ -31,6 +31,16 @@ "inputRev": "d13f23b723b8a846827a245b89c10fc7d3f11612", "inherited": false, "configFile": "lakefile.lean"}, + {"url": "https://github.com/TauCetiProject/TauCeti", + "type": "git", + "subDir": null, + "scope": "", + "rev": "9965de63baed364af97a4148480b71072a4d21e3", + "name": "TauCeti", + "manifestFile": "lake-manifest.json", + "inputRev": "9965de63baed364af97a4148480b71072a4d21e3", + "inherited": false, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, diff --git a/lakefile.toml b/lakefile.toml index 99f3830a..4c67958e 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -4,6 +4,15 @@ defaultTargets = ["LeanEval"] [leanOptions] autoImplicit = false +# TauCeti supplies the definitions in the classification of finite simple groups +# problem. Its rev must build against the Mathlib rev below. It is listed before +# Mathlib because Lake takes shared transitive dependencies (batteries, aesop, ...) +# from the later require, and those must be Mathlib's. +[[require]] +name = "TauCeti" +git = "https://github.com/TauCetiProject/TauCeti" +rev = "9965de63baed364af97a4148480b71072a4d21e3" + [[require]] name = "mathlib" git = "https://github.com/leanprover-community/mathlib4.git" @@ -17,7 +26,7 @@ rev = "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204" [[require]] name = "lean-eval-generator" git = "https://github.com/leanprover/lean-eval-generator.git" -rev = "77373a539b31f8f304c852f288d7d8469cceebff" +rev = "2de74049bd91d2c592e7009df8f5e5968599a272" [[lean_lib]] name = "LeanEval" diff --git a/manifests/problems/classification_finite_simple_groups.toml b/manifests/problems/classification_finite_simple_groups.toml new file mode 100644 index 00000000..ed0fcde2 --- /dev/null +++ b/manifests/problems/classification_finite_simple_groups.toml @@ -0,0 +1,17 @@ +id = "classification_finite_simple_groups" +title = "The classification of finite simple groups" +group = "formalization-evaluation" +status = "active" +visible = true +statement_revision = 1 +tags = [] +module = "LeanEval.GroupTheory.ClassificationFiniteSimpleGroups" +holes = ["classification_finite_simple_groups"] +submitter = "Kim Morrison" +notes = "Every finite simple group is isomorphic to a cyclic group of prime order, an alternating group Aₙ with n ≥ 5, a group of Lie type, or one of the twenty-six sporadic groups. The list is the Tau Ceti project's TauCeti.CFSGIndex, and the statement is TauCeti.ClassificationStatement spelled out. The Lie-type groups are explicit constructions (the derived subgroup of the fixed points of a Steinberg endomorphism, modulo its centre), and the sporadic groups are given by explicit finite presentations; the problem inherits the correctness of those definitions from Tau Ceti. Only the direction 'every finite simple group is on the list' is required: finiteness, simplicity and irredundancy of the listed groups are not part of the statement." +source = "D. Gorenstein, R. Lyons and R. Solomon, The Classification of the Finite Simple Groups (AMS Mathematical Surveys and Monographs 40, 1994–); M. Aschbacher, R. Lyons, S. D. Smith and R. Solomon, The Classification of Finite Simple Groups: Groups of Characteristic 2 Type (AMS, 2011). Statement: https://github.com/TauCetiProject/TauCeti/blob/main/TauCeti/GroupTheory/SpecificGroups/CFSG/Classification.lean" + +[[status_history]] +status = "active" +effective_date = "2026-09-25" +reason = "policy" diff --git a/manifests/sets/v2.toml b/manifests/sets/v2.toml index 585319ad..2b5ee5cf 100644 --- a/manifests/sets/v2.toml +++ b/manifests/sets/v2.toml @@ -3,5 +3,6 @@ id = "v2" title = "LeanEval v2" frozen = false members = [ + { problem_id = "classification_finite_simple_groups", statement_revision = 1 }, { problem_id = "hopf_s6_complex_structure", statement_revision = 1 }, ]