---
id: "2026-10-13-thompson-group-f-nonamenable-kim-lodha-exposition"
url: "https://postcutoff.com/e/2026-10-13-thompson-group-f-nonamenable-kim-lodha-exposition/"
as_of: "2026-10-14T07:26:00+02:00"
date: "2026-10-13"
date_precision: day
category: science
importance: 4
confidence: medium
status: [Awaiting review]
verification: Lean-verified
sources: 3
editor: human editor
human_review: null
version: null
---

As of: 2026-10-14 07:26 CEST.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code), with a human editor. How we work: https://postcutoff.com/about/
Canonical page: https://postcutoff.com/e/2026-10-13-thompson-group-f-nonamenable-kim-lodha-exposition/

# Thompson's group F is nonamenable

Full title: Thompson's group F is nonamenable: specialists Sang-hyun Kim and Yash Lodha publish a human-written version of OpenAI's proof

OpenAI's 6 Oct 2026 math release (family 248, manuscript dated 23 Sep, Lean scope note) claims that Thompson's group F is nonamenable, settling a problem first raised by Richard Thompson in 1973 and central to Geoghegan's conjecture. On 13 Oct Sang-hyun Kim and Yash Lodha (Purdue), specialists in groups of piecewise linear and projective homeomorphisms, posted arXiv 2610.18360, "a human written exposition of OpenAI's recent proof": a streamlined proof plus a generalization, with "no novelty claimed" and "No part of this writing, including the references, was produced by AI." It is the first public write-up of the claim by experts in the field; it is unrefereed.

## 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](/e/2026-10-06-openai-math-release-722-manuscripts/) 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.18360](https://arxiv.org/abs/2610.18360). 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)

## Your AI and this story

- GPT-6 Astra (training cutoff April 2026): 166 days after its cutoff
- Claude Opus 5.5 (training cutoff June 2026): 105 days after its cutoff
- Gemini 4 Argon (training cutoff March 2026): 196 days after its cutoff
- Grok 4.7 (training cutoff May 2026): 135 days after its cutoff

## Sources

1. [arXiv 2610.18360: Kim & Lodha, A note on the proof of nonamenability of F](https://arxiv.org/abs/2610.18360) (arxiv.org, paper)
2. [OpenAI: Thompson's group F is nonamenable (23 Sep manuscript)](https://github.com/openai/math/tree/main/preprints/Thompsons-group-F-is-nonamenable-September-23-2026) (github.com, paper)
3. [openai/math CONTENTS.md (family 248)](https://github.com/openai/math/blob/main/CONTENTS.md) (github.com, code)

## Changes

- 2026-10-14 (filed): Created from the arXiv note (the AI named in the abstract)

## Related

- 2026-10-06: [OpenAI releases 722 AI-written math manuscripts claiming hundreds of open problems](https://postcutoff.com/e/2026-10-06-openai-math-release-722-manuscripts/index.md)