Just finite presentations

DefinitionBarnea's question on just finite presentations (Kourovka 21.10)#✓fully proved

The statement that every finite group \(G\) has a just finite presentation: a presentation \(\langle X \mid R \rangle\) with \(X\) and \(R\) finite that defines \(G\) and such that removing any single relator from \(R\) gives a presentation of an infinite group.

def finiteGroupHasJustFinitePresentation : Prop :=
  ∀ (G : Type) [Group G] [Finite G], ∃ (n : ℕ) (R : Finset (FreeGroup (Fin n))),
    Nonempty (PresentedGroup (R : Set (FreeGroup (Fin n))) ≃* G) ∧
    ∀ r ∈ R, Infinite (PresentedGroup ((R.erase r : Finset (FreeGroup (Fin n))) :
      Set (FreeGroup (Fin n))))

Used by 1

Used byEvery finite group has a just finite presentation

TheoremEvery finite group has a just finite presentation#●ready to prove

For every finite group \(G\) there are a natural number \(n\) and a finite subset \(R\) of the free group on \(n\) generators \(x_1, \dots, x_n\) such that the group \(\langle x_1, \dots, x_n \mid R \rangle\) is isomorphic to \(G\) and, for every \(r \in R\), the group \(\langle x_1, \dots, x_n \mid R \setminus \{r\} \rangle\) is infinite. That is, the answer to Kourovka Problem 21.10 is positive.

Lackenby's paper acknowledges assistance from the Google DeepMind AI co-mathematician tool.

public theorem_wanted finiteGroupHasJustFinitePresentation_holds :
    finiteGroupHasJustFinitePresentation

Sources

• E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 21.10 (Y. Barnea); resolution: M. Lackenby, Every finite group admits a just finite presentation, preprint, arXiv:2605.10402 (2026), Theorem 1: every finite group admits a finite, just finite presentation (a consequence of Theorem 2 on just-(FA) presentations); Kourovka Notebook (21st issue), Problem 21.10: Yes, it is true, https://arxiv.org/abs/2605.10402.

Uses 1

Statement usesBarnea's question on just finite presentations (Kourovka 21.10)

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.