feat: add the classification of finite simple groups to v2

.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=()

EvalTools/RunEval.lean

@@ -81,15 +81,15 @@ 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
     let mut extracteds : Array ExtractedTheorem := #[]
     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

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

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,

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"

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"

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 },
 ]