The amenability problem for Thompson's group F (Geoghegan's conjecture)
Thompson's group is the group, under composition, of increasing piecewise linear homeomorphisms of with finitely many pieces, dyadic rational breakpoints and slopes in . A discrete group is amenable if its bounded real functions carry a positive normalized left-invariant mean. has no nonabelian free subgroup (Brin-Squier), so the free-subgroup obstruction does not apply, yet it is not elementary amenable. Geoghegan conjectured in 1979 that is not amenable. Is Thompson's group nonamenable?
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Geometric group theory; amenability
- Posed by
- Ross Geoghegan (1979), as recorded by J. W. Cannon, W. J. Floyd and W. R. Parry, Introductory notes on Richard Thompson's groups (Enseign. Math., 1996), p. 227
- Year posed
- 1979
- Years open
- 47y
- 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
- 58 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Theorem 1.1: Thompson's group is not amenable. The proof finds a fixed finite set and with for some , for every nonempty finite , so no Folner sets exist. It converts approximate invariance of finite averages into an approximate fixed point of a Lipschitz self-map of a Hilbert ball, contradicting a Benyamini-Sternfeld displacement map that the paper constructs explicitly. It confirms Geoghegan's conjecture. The formal version gives no explicit expansion constant for a standard generating set, and the paper does not address other questions about such as its exact isoperimetric profile.
What the AI did
The release README states that the vast majority of its results were produced by one fixed procedure with an unreleased internal OpenAI model, using on average about three hours of ChatGPT Pro thinking compute per result; roughly 4,000 problems were posed and the output was aggregated into result families and manuscripts, keeping those judged significant enough. This single-manuscript family is dated September 23, 2026 and comes with a Lean formalization in the release's lean/ library. The manuscript is credited to 'OpenAI' alone, names no human author and has no acknowledgements. The README's two exceptions to the fixed procedure (the zeta zero-free region work, whose Re(s) > 11/12 write-up was also human-edited, and the Hodge conjecture for CM abelian varieties) do not concern this family, so the result is presented as found and written up by the model. The release does not say how problems were chosen or how much human review happened before publication.
Verification
No independent mathematician has checked this yet. The formalization catalogue lists comparator config ComparatorChallenges/ThompsonNonamenability.json with declaration OAI.ThompsonNonamenability.thompson_F_nonamenable_composition in OAI/GroupTheory/Thompson/Main.lean, permitted axioms propext, Quot.sound and Classical.choice. The comparator statement file was read: it defines F concretely as strictly increasing homeomorphisms of [0,1] with finitely many dyadic knots, each piece affine with slope an integer power of 2; it defines an invariant mean as a positive, normalized, left-invariant real-linear functional on bounded real functions on the group; and it states that there is a group structure on F whose product is composition and that no invariant mean exists. That is the headline claim. Not rebuilt here: the Lean build and axiom check were not run. Given the problem's history of withdrawn claims, an expert reading is still wanted even with a formal proof; the Lean statement was read for fidelity here, not audited independently.