Is there an infinite finitely presented simple amenable group?
A discrete group is amenable if it has Folner sets: for every finite and there is a nonempty finite with for all . Juschenko and Monod (2013) proved that topological full groups of minimal Cantor homeomorphisms are amenable, which with Matui's work gives infinite finitely generated simple amenable groups. Those derived groups are not finitely presented (Matui), and the local embeddability of full groups into finite groups (Grigorchuk-Medynets) explains why such examples cannot be. Does there exist an infinite group that is finitely presented, simple and amenable?
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Construction
- Field
- Geometric group theory: amenable and simple groups
- Posed by
- Recorded by J. O. Button, Largeness of LERF and 1-relator groups, Groups Geom. Dyn. 4 (2010), p. 729; raised again by Juschenko and Monod, Ann. of Math. 178 (2013), p. 776
- Year posed
- 2010
- Years open
- 16y
- Solved
- 2026-09-23
- Model
- Unreleased internal OpenAI model
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Collection
- OpenAI math release (October 2026), version adc7f12
- Significance
- 40 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Theorem 1.1: there exists an infinite finitely presented simple amenable group. It is an alternating subgroup of a polygon exchange group (piecewise translations of finitely many squares over a real quadratic ring, with two inclined edge directions besides the coordinate ones). Finite presentation comes from propagating relations over a fixed finite generating set with a homological argument in the style of Szymik-Wahl; amenability from correlated random polygonal partitions giving almost-invariant measures. No explicit bound on the sizes of the generating set or relators is given.
What the AI did
The OpenAI math release (github.com/openai/math, commit adc7f12) states that its results were produced by an unreleased internal OpenAI model under one fixed procedure, averaging about three hours of ChatGPT Pro thinking compute per result, across roughly 4,000 posed problems; outputs were then grouped into families and filtered for significance. This result is not among the README's stated exceptions (the Riemann zeta zero-free region work and the Hodge conjecture for CM abelian varieties). The manuscript is credited to OpenAI alone and names no human author.
Verification
No independent mathematician has checked this yet. Checked here: the introduction and Theorem 1.1 of the TeX source; the construction and proofs were not refereed. Lean-checked on the Comparator challenge SimpleAmenable, listed in the release's formalization catalogue (OAI.SimpleAmenable.main, OAI/GroupTheory/SimpleAmenable/Main.lean). Its statement: there exists a group that is infinite, finitely presented (Mathlib's Group.IsFinitelyPresented), simple (Mathlib's IsSimpleGroup) and satisfies the Folner condition as displayed in the problem statement. That is the headline claim, with amenability in its Folner form. The release's Lean notes say the paper's later general claims (central kernels, enlargements across families) are not formalized. Permitted axioms: propext, Quot.sound, Classical.choice. Not rebuilt here.