Thompson's group F is nonamenable
Thompson's group F is nonamenable is the title of a manuscript dated 23 September 2026 in OpenAI's public mathematics collection (github.com/openai/math). Thompson's group F is the group of piecewise linear homeomorphisms of the unit interval with finitely many breakpoints, all at dyadic rationals, and slopes that are integer powers of 2. Whether F is amenable had been a long-standing open problem. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
The original result
- Claim. Thompson's group F is not amenable. The abstract states that this confirms Geoghegan's conjecture and resolves the amenability problem for F. Source: Thompson's group F is nonamenable (23 September 2026).
- Formalization, as described by the repository. The scope note lean/docs/248.md states that the Lean formalization rules out a positive normalized left-invariant mean on bounded real functions for the standard group of dyadic piecewise-linear homeomorphisms of the interval, proving nonamenability; no explicit boundary constant or prescribed generating set is given.
- Background. For the state of the problem before the manuscript, see V. Guba, Amenability problem for Thompson's group F: state of the art (arXiv:2305.07113).
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 14 October 2026) |
|---|---|---|---|---|
2026-10-08 (latest commit a371d87, 10 October 2026) |
J. Guo, Consequences of results in the OpenAI mathematics release, entry 6, in the GitHub repository aster2024/openai-math-followups | Use (conditional consequences) | Combining the nonamenability of F with published results of Le Boudec and Matte Bon; Breuillard, Kalantar, Kennedy and Ozawa; and Bartholdi and Kielak: Thompson's group T is C*-simple (the list names this the Haagerup–Olesen question) and its reduced C*-algebra has a unique tracial state; F, Aut(F) and Comm(F) are C*-simple; for every field K the group algebra K[F] is a domain but not an Ore domain; and Myhill's property fails over F. The entry notes that the C*-simplicity of T and of F also appears as entry GR-5 of the catalogue atimics/math2 (8 October 2026). | The list states that each entry is conditional on the release theorem it names. |
| 2026-10-08 | MathVet (GitHub; review of openai/math at commit adc7f12, tables at repository commit cd0063d, 13 October 2026) |
Review (fidelity of the formal statements) | Rates this family "full": the Lean statement is the nonamenability of F, with F defined by dyadic breakpoints and slopes that are powers of 2 and with composition as the group law. Its per-challenge table records a sandboxed Comparator pass for the challenge ThompsonNonamenability (8 October 2026). |
The review states that "full" means the Lean states the headline and "does not say the mathematics is correct beyond what Lean checked"; it describes itself as a model-assisted reading without a referee yet. |
| 2026-10-13 | S.-h. Kim, Y. Lodha, A note on the proof of nonamenability of F (arXiv:2610.18360, v1) | Exposition | The abstract states that the note provides "a human written exposition of OpenAI's recent proof that Thompson's group F is nonamenable". | arXiv v1. |
Notes
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.