From c34a2745bda284f23284f4b234da08e2a715b25d Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Mon, 13 Apr 2026 21:42:26 +1000
Subject: [PATCH] feat: add Cayley graph connectivity eval problem

Uses the newly defined Cayley graph (SimpleGraph.mulCayley) to state
that connectivity of the Cayley graph is equivalent to the generating
set generating the group. A foundational result in geometric group theory.

Bumps mathlib to include the Cayley graph definition PR.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
---
 .../Combinatorics/CayleyConnected.lean        | 30 +++++++++++++++++++
 lake-manifest.json                            | 22 +++++++-------
 manifests/problems.toml                       | 11 +++++++
 3 files changed, 52 insertions(+), 11 deletions(-)
 create mode 100644 FormalMathEval/Combinatorics/CayleyConnected.lean

diff --git a/FormalMathEval/Combinatorics/CayleyConnected.lean b/FormalMathEval/Combinatorics/CayleyConnected.lean
new file mode 100644
index 000000000..72cc91940
--- /dev/null
+++ b/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
diff --git a/lake-manifest.json b/lake-manifest.json
index 52d5fd89b..5d875c344 100644
--- a/lake-manifest.json
+++ b/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",
diff --git a/manifests/problems.toml b/manifests/problems.toml
index c70a46099..3b08cb45f 100644
--- a/manifests/problems.toml
+++ b/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."