Isospectral finite simple groups

DefinitionSpectrum of a group#✓fully proved

The spectrum \(\omega(G)\) of a group \(G\) is the set of orders of its elements, where an element of infinite order is counted as having order \(0\).

def spectrum (G : Type*) [Group G] : Set ℕ :=
  Set.range (orderOf : G → ℕ)

Used by 1

Used byThree isospectral finite simple groups

DefinitionThree isospectral finite simple groups#✓fully proved

Kourovka 16.25 (A. V. Vasil'ev): there are three pairwise non-isomorphic finite non-abelian simple groups with the same spectrum.

def threeIsospectralSimpleGroups : Prop :=
  ∃ (G₁ G₂ G₃ : Type) (_ : Group G₁) (_ : Group G₂) (_ : Group G₃)
    (_ : Finite G₁) (_ : Finite G₂) (_ : Finite G₃),
    IsSimpleGroup G₁ ∧ IsSimpleGroup G₂ ∧ IsSimpleGroup G₃ ∧
    (∃ a b : G₁, a * b ≠ b * a) ∧ (∃ a b : G₂, a * b ≠ b * a) ∧ (∃ a b : G₃, a * b ≠ b * a) ∧
    IsEmpty (G₁ ≃* G₂) ∧ IsEmpty (G₁ ≃* G₃) ∧ IsEmpty (G₂ ≃* G₃) ∧
    spectrum G₁ = spectrum G₂ ∧ spectrum G₂ = spectrum G₃

Uses 1 · Used by 1

Statement usesSpectrum of a group

Used byNo three non-isomorphic finite non-abelian simple groups are isospectral

TheoremNo three non-isomorphic finite non-abelian simple groups are isospectral#●ready to prove

There do not exist three pairwise non-isomorphic finite non-abelian simple groups \(G_1, G_2, G_3\) with \(\omega(G_1) = \omega(G_2) = \omega(G_3)\), where the spectrum \(\omega(G)\) of a group \(G\) is the set of orders of its elements.

This answers Kourovka Problem 16.25 (A. V. Vasil'ev) in the negative; the Kourovka Archive cites Buturlakin (2010).

public theorem_wanted threeIsospectralSimpleGroups_refuted : ¬ threeIsospectralSimpleGroups

def threeIsospectralSimpleGroups : Prop :=
  ∃ (G₁ G₂ G₃ : Type) (_ : Group G₁) (_ : Group G₂) (_ : Group G₃)
    (_ : Finite G₁) (_ : Finite G₂) (_ : Finite G₃),
    IsSimpleGroup G₁ ∧ IsSimpleGroup G₂ ∧ IsSimpleGroup G₃ ∧
    (∃ a b : G₁, a * b ≠ b * a) ∧ (∃ a b : G₂, a * b ≠ b * a) ∧ (∃ a b : G₃, a * b ≠ b * a) ∧
    IsEmpty (G₁ ≃* G₂) ∧ IsEmpty (G₁ ≃* G₃) ∧ IsEmpty (G₂ ≃* G₃) ∧
    spectrum G₁ = spectrum G₂ ∧ spectrum G₂ = spectrum G₃

WantedExt/GroupTheory/ThreeIsospectralSimpleGroupsKourovka16Problem25Wanted.lean:41

Sources

E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Archive of Solved Problems, Problem 16.25 (A. V. Vasil'ev); resolution: A. A. Buturlakin, Sib. Èlektron. Mat. Izv. 7 (2010), 111-114, Kourovka Archive, Problem 16.25 (No).

Uses 1

Statement usesThree isospectral finite simple groups

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.