Thompson’s group F is nonamenable
Specialists Sang-hyun Kim and Yash Lodha publish a human-written version of OpenAI’s proof
Awaiting review
Importance: major (4 of 5)The takeaway
The amenability of Thompson’s group F, open since the 1970s, was one of the headline claims of OpenAI’s 6 Oct math release. Two experts on groups of piecewise linear maps have now written the proof out themselves and generalized it, without AI.
Status
- Claim
Awaiting review
- Our reporting
- Medium confidence
- Verification
- Lean-verified
- Importance
- Major (4 of 5)
- Last verified
- 14 October 2026
Your AI and this story
- GPT-6 Astra166 days after its cutoff
- Claude Opus 5.5105 days after its cutoff
- Gemini 4 Argon196 days after its cutoff
- Grok 4.7135 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 105 days before it.
Key facts
- Claim: OpenAI family 248, ‘Thompson’s group F is nonamenable’ (manuscript dated 23 Sep 2026): ‘This confirms Geoghegan’s conjecture and resolves the amenability problem for F’; the catalogue links a Lean scope note (lean/docs/248.md)
- Exposition: Sang-hyun Kim (Korea Institute for Advanced Study) and Yash Lodha (Purdue), ‘A note on the proof of nonamenability of F’, arXiv 2610.18360 [math.GR], dated 13 Oct 2026
- Quote: ‘It has been a long standing open problem whether F is amenable … Recently, OpenAI announced a solution. Using the same idea, we give a streamlined proof, and describe a generalization in Theorem 2.7. All the arguments here are based on simplifications of those in the OpenAI announcement, and no novelty is claimed here. No part of this writing, including the references, was produced by AI.’
- History (the note): first considered by Richard Thompson (letter to George Francis, 26 Sep 1973) and popularized by Ross Geoghegan as part of his conjecture
- Lodha’s earlier work includes a nonamenable type-F∞ group of piecewise projective homeomorphisms (J. Topology 2020), so the authors are specialists in exactly this problem area
What happened
OpenAI’s 6 Oct release listed, as family 248, a proof that Thompson’s group F is nonamenable, with a Lean scope note. F, the group of dyadic piecewise linear homeomorphisms of [0, 1], is a central test case in the theory of amenable groups, and the question had been open since Thompson raised it in 1973 (Kim and Lodha cite his letter to George Francis of 26 Sep 1973).
On 13 Oct Sang-hyun Kim and Yash Lodha posted arXiv 2610.183601. They give “a streamlined proof” using “the same idea” as OpenAI’s manuscript, add a generalization (Theorem 2.7), and state that no part of the note was produced by AI. They claim no novelty.
No further expert reactions were found on 14 Oct (web search; X not searched directly).
Why it matters
Most of the release’s famous claims still await reading by specialists. This is one of the first cases where experts in the exact area have reconstructed an AI proof of a famous problem by hand, which makes errors much less likely than for a claim checked only by its authors’ Lean scope note. Formal publication and wider expert review are still to come.
What is disputed or not yet verified
| Verification | Lean scope note by OpenAI; human exposition by two specialists (unrefereed) |
|---|
Sources
3 sources from 2 sites. Numbers match the chips in the text.
3 sources: 3 primary
Primary
- arXiv 2610.18360: Kim & Lodha, A note on the proof of nonamenability of Farxiv.org, paper
- OpenAI: Thompson’s group F is nonamenable (23 Sep manuscript)github.com, paper
- openai/math CONTENTS.md (family 248)github.com, code
Changes
- Filed from the arXiv note (the AI named in the abstract)