/-
Copyright 2026 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtilBabai–Seress Conjectures on the Diameter of Finite Groups
References:
Wikipedia, Diameter (group theory)
H. A. Helfgott and Á. Seress, On the diameter of permutation groups
This file contains two conjectures from the Babai–Seress paper:
Conjecture 1.5: $\operatorname{diam}(A_n) < n^C$ for some absolute constant $C$, where $A_n$ is the alternating group on $n$ elements.
Conjecture 1.7: $\operatorname{diam}(G) < (\log |G|)^C$ for some absolute constant $C$, where $G$ ranges over all non-abelian finite simple groups.
Conjecture 1.7 generalises Conjecture 1.5, since for $G = A_n$ we have $\log |A_n| \approx n \log n$, so a polylogarithmic bound in $|G|$ implies a polynomial bound in $n$.
namespace BabaiSeressConjecturesThe (undirected) Cayley graph of a group $G$ with respect to a generating set $S$. Two elements $g, h \in G$ are adjacent iff $g \neq h$ and $g^{-1} h \in S$ or $h^{-1} g \in S$.
This is constructed using SimpleGraph.fromRel, which takes the relation
$g \sim h \iff g^{-1} h \in S$ and automatically symmetrizes it (via disjunction with the
reverse relation) and enforces irreflexivity (via $g \neq h$). In particular, this definition
effectively uses the symmetrization $S \cup S^{-1}$, so it produces a standard undirected
Cayley graph even when $S$ is not itself symmetric.
def cayleyGraph {G : Type*} [Group G] (S : Set G) : SimpleGraph G :=
SimpleGraph.fromRel (fun g h => g⁻¹ * h ∈ S)The diameter of a finite group $G$, defined as the maximum diameter of the Cayley graphs $\Gamma(G, A)$ over all generating sets $A$ of $G$.
noncomputable def groupDiam (G : Type*) [Group G] [Fintype G] : ℕ :=
sSup { d : ℕ | ∃ S : Set G, Subgroup.closure S = ⊤ ∧ (cayleyGraph S).diam = d }For the trivial group (with one element), the group diameter is zero, since every Cayley graph has only one vertex and hence diameter zero.
@[category test, AMS 20]
theorem groupDiam_fin_one : groupDiam (alternatingGroup (Fin 0)) = 0 := ⊢ groupDiam ↥(alternatingGroup (Fin 0)) = 0
⊢ sSup {d | ∃ S, Subgroup.closure S = ⊤ ∧ (cayleyGraph S).diam = d} = 0
⊢ sSup {d | ∃ S, Subgroup.closure S = ⊤ ∧ (cayleyGraph S).diam = d} ≤ 0
⊢ {d | ∃ S, Subgroup.closure S = ⊤ ∧ (cayleyGraph S).diam = d}.Nonempty⊢ ∀ b ∈ {d | ∃ S, Subgroup.closure S = ⊤ ∧ (cayleyGraph S).diam = d}, b ≤ 0
⊢ {d | ∃ S, Subgroup.closure S = ⊤ ∧ (cayleyGraph S).diam = d}.Nonempty All goals completed! 🐙
⊢ ∀ b ∈ {d | ∃ S, Subgroup.closure S = ⊤ ∧ (cayleyGraph S).diam = d}, b ≤ 0 d:ℕS:Set ↥(alternatingGroup (Fin 0))left✝:Subgroup.closure S = ⊤hd:(cayleyGraph S).diam = d⊢ d ≤ 0
All goals completed! 🐙The alternating group $A_3 \cong \mathbb{Z}/3\mathbb{Z}$ has group diameter $1$: every non-trivial generating set produces a complete Cayley graph $K_3$, since any single non-identity element and its inverse already reach the entire group.
All goals completed! 🐙The symmetric group $S_2 \cong \mathbb{Z}/2\mathbb{Z}$ has group diameter $1$: the unique generating set ${(01)}$ produces the complete graph $K_2$, since the single non-identity element and its inverse (which are equal) cover the only other vertex.
All goals completed! 🐙Babai–Seress Conjecture (Conjecture 1.5): There exists an absolute constant $C$ such that the diameter of the alternating group $A_n$ satisfies $$\operatorname{diam}(A_n) \leq n^C.$$
@[category research open, AMS 5 20 68]
theorem babai_seress_conjecture_alternating :
∃ C : ℕ, ∀ n : ℕ,
(groupDiam (alternatingGroup (Fin n)) : ℝ) ≤ (n : ℝ) ^ C := ⊢ ∃ C, ∀ (n : ℕ), ↑(groupDiam ↥(alternatingGroup (Fin n))) ≤ ↑n ^ C
All goals completed! 🐙Babai–Seress Conjecture (Conjecture 1.7): There exists an absolute constant $C$ such that every finite simple non-abelian group $G$ satisfies $$\operatorname{diam}(G) \leq (\log |G|)^C.$$
@[category research open, AMS 5 20 68]
theorem babai_seress_conjecture :
∃ C : ℕ,
∀ (G : Type) [Group G] [Fintype G] [IsSimpleGroup G],
(∃ a b : G, a * b ≠ b * a) →
(groupDiam G : ℝ) ≤ (Real.log (Fintype.card G : ℝ)) ^ C := ⊢ ∃ C,
∀ (G : Type) [inst : Group G] [inst_1 : Fintype G] [IsSimpleGroup G],
(∃ a b, a * b ≠ b * a) → ↑(groupDiam G) ≤ Real.log ↑(Fintype.card G) ^ C
All goals completed! 🐙end BabaiSeressConjectures