Finitely generated simple amenable groups

DefinitionKourovka Problem 15.5 (statement): infinite finitely generated simple amenable groups#✓fully proved

The statement that there exists a group \(G\) that is infinite, finitely generated, simple and amenable, where amenable means that \(G\) satisfies the Følner condition.

def infiniteFGSimpleAmenableGroup : Prop :=
  ∃ (G : Type) (_ : Group G), Infinite G ∧ Group.FG G ∧ IsSimpleGroup G ∧ IsAmenable G

Uses 1 · Used by 1

Statement usesAmenable group (Følner condition)

Used byJuschenko–Monod theorem (Kourovka Problem 15.5)

TheoremJuschenko–Monod theorem (Kourovka Problem 15.5)#●ready to prove

There exists a group \(G\) that is infinite, finitely generated, simple and amenable, where amenable means that \(G\) satisfies the Følner condition.

public theorem_wanted infiniteFGSimpleAmenableGroup_holds : infiniteFGSimpleAmenableGroup

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 15.5 (P. de la Harpe); resolution: K. Juschenko and N. Monod, Cantor systems, piecewise translations and simple amenable groups, Ann. of Math. (2) 178 (2013), no. 2, 775-787, arXiv:1204.2132, abstract (the first examples of finitely generated simple groups that are amenable and infinite); Kourovka Archive, Problem 15.5 (answer: Yes, it does; another example in V. Nekrashevych, Ann. of Math. 187 (2018), 667-719), https://arxiv.org/abs/1204.2132.

Uses 1

Statement usesKourovka Problem 15.5 (statement): infinite finitely generated simple amenable groups

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.