Cayley graph connected iff generators generate the group

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.

theorem declaration uses `sorry`mulCayley_connected_iff_closure_eq_top {G : Type*} [Group G]
    (S : Set G) :
    (SimpleGraph.mulCayley S).Connected ↔ Subgroup.closure S = ⊤ := byG:Type u_1inst✝:Group GS:Set G⊢ (SimpleGraph.mulCayley S).Connected ↔ Subgroup.closure S = ⊤
  sorryAll goals completed! 🐙

Solved by

• @kim-em with Aristotle (Harmonic) on May 1, 2026 (proof)

• @rkirov with Claude Opus 4.7 (1M context) on May 2, 2026 (proof)

• @sqrt-of-2 with GPT-5.5 on May 7, 2026 (proof)

• @antpavzhi with Aleph Prover(logicalintelligence.com) on May 8, 2026

• @sqrt-of-2 with Gemini 3.1 Pro on May 10, 2026 (proof)

• @daouid with Antigravity (Multi-Model Ensemble: Gemini 3.1 Pro, Gemini 3 Flash, Claude 4.6 Sonnet/Opus) on May 13, 2026 (proof)

• @GanjinZero with Seed Prover (ByteDance) on May 20, 2026