feat: add Cayley graph connectivity eval problem

FormalMathEval/Combinatorics/CayleyConnected.lean

@@ -0,0 +1,30 @@
+import Mathlib.Combinatorics.SimpleGraph.Cayley
+import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
+import Mathlib.Algebra.Group.Subgroup.Lattice
+import EvalTools.Markers
+
+namespace FormalMathEval
+namespace Combinatorics
+
+/-!
+A Cayley graph is connected if and only if its generators generate the group.
+
+The Cayley graph of a group `G` with generators `S` has vertex set `G` and an edge between
+`x` and `y` whenever `x * g = y` for some `g ∈ S`. This theorem characterises connectivity:
+the Cayley graph is connected if and only if `S` generates `G` as a group. The forward
+direction constructs a path from `1` to any `g ∈ G` via the generators; the reverse shows
+that any path in the graph corresponds to a product of generators.
+
+This is a foundational result in geometric group theory, connecting algebraic generation
+to graph-theoretic connectivity.
+-/
+
+@[eval_problem]
+theorem mulCayley_connected_iff_closure_eq_top
+    {G : Type*} [Group G]
+    (S : Set G) :
+    (SimpleGraph.mulCayley S).Connected ↔ Subgroup.closure S = ⊤ := by
+  sorry
+
+end Combinatorics
+end FormalMathEval

lake-manifest.json

@@ -1,7 +1,17 @@
 {"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover-community/mathlib4.git",
+ [{"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "f7d0ca7c926cdde0562af20394dd25d028b839a5",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.30.0-rc1",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
    "scope": "",
@@ -80,16 +90,6 @@
    "manifestFile": "lake-manifest.json",
    "inputRev": "v4.30.0-rc1",
    "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover/lean4-cli",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover",
-   "rev": "f7d0ca7c926cdde0562af20394dd25d028b839a5",
-   "name": "Cli",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.30.0-rc1",
-   "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "«formal-math-eval»",
  "lakeDir": ".lake",

manifests/problems.toml

@@ -219,3 +219,14 @@ submitter = "Kim Morrison"
 notes = "Part of the Schur-Polya-Loewner theory of entrywise functions preserving PSD. The proof uses the Schur product theorem iteratively: exp_⊙(A) = ∑ A^{⊙k}/k!, each Hadamard power is PSD, and the convergent series of PSD matrices is PSD."
 source = "I.J. Schoenberg, Positive definite functions on spheres, 1942."
 informal_solution = "Write exp(a_{ij}) as the convergent series ∑ (a_{ij})^k / k!. The matrix with entries (a_{ij})^k is the k-fold Hadamard product A^{⊙k}, which is PSD by iterated Schur product. The partial sums are nonneg combinations of PSD matrices, hence PSD. PSD is a closed condition, so the limit is PSD."
+
+[[problem]]
+id = "mulCayley_connected_iff_closure_eq_top"
+title = "Cayley graph connected iff generators generate the group"
+test = false
+module = "FormalMathEval.Combinatorics.CayleyConnected"
+theorem = "mulCayley_connected_iff_closure_eq_top"
+submitter = "Kim Morrison"
+notes = "A foundational result in geometric group theory using the newly defined Cayley graph. Connectivity of the Cayley graph is equivalent to the generating set S generating G as a group."
+source = "A. Cayley, On the theory of groups, as depending on the symbolic equation θ^n = 1, 1878."
+informal_solution = "Forward: if connected, any g ∈ G is reached from 1 by a path, which corresponds to a product of generators. Reverse: if S generates, any g is a product of generators, giving a path from 1 to g."