Thompson's group F is nonamenable

Proves that Thompson's group F, the group of dyadic piecewise linear homeomorphisms of the interval, is nonamenable, resolving its longstanding amenability problem. (Lean)

Manuscript

Thompson's group F is nonamenable

September 23, 2026 · source · Lean formalization available · cite as \cite{OAI:Thompsons-group-F-is-nonamenable-September-23-2026}

We prove that Thompson's group F is nonamenable. This confirms Geoghegan's conjecture and resolves the amenability problem for F.

Result 248 · Group theory. Imported from openai/math, a collection of manuscripts produced by an OpenAI model; results are at different stages of verification. Discussion below is by Lemma members.