Thompson's group F is nonamenable

Follow-up works

• Sang-hyun Kim and Yash Lodha, A note on the proof of nonamenability of F (arXiv:2610.18360, 13 Oct 2026). Describes itself as "a human written exposition of OpenAI's recent proof that Thompson's group F is nonamenable"; it gives a streamlined argument by showing the action of F on the dyadic rationals is not extensively amenable, and states a generalization (Theorem 2.7) to groups of permutations of a set, with its proof omitted.
• Koji Fujiwara, Thompson's group F is not weakly amenable (arXiv:2610.27932, 20 Oct 2026). Embeds the semidirect product of Z^(D) (D the dyadic rationals in [0,1]) by F into F and deduces non-weak-amenability from nonamenability of F, citing this paper as Theorem 1.1 and the Kim–Lodha note for a streamlined proof.
• Chris Bruce and Shirly Geffen, C*-selflessness and Z-stability for Thompson's group F (arXiv:2610.28473, 20 Oct 2026). Proves that the reduced C*-algebra of F is Z-stable and selfless, using this paper's nonamenability theorem together with another release preprint (The Kirchberg–Rørdam character criterion).
• acprk, An explicit isoperimetric constant for Thompson's group F (GitHub, version 0.1.0, 2026-10-10). Gives an explicit edge-isoperimetric (Cheeger) lower bound for F with generators {x0, x1} (about 2.1e-19 unconditionally) by making this paper's constants explicit, conditional on the upstream proof's correctness, and states that the work has neither human peer review nor a Lean formalization. [AI-generated per source]

Comments and discussion

• Ville Salo, Paradoxical decompositions of Thompson's F (MathOverflow, 2026-10-08). Asks how to extract concrete translation sets and a paradoxical decomposition from this paper's Følner argument, identifying the auxiliary map's Lipschitz constant as an obstacle to making the construction explicit.
• Elliot Glazer (@ElliotGlazer), post on X (2026-10-18). Shares commentary by Justin Moore on OpenAI's proof of the nonamenability of F, posted as an image.
• Liu Yao 刘杳 (@liuyao12), post on X (2026-10-19). In the context of Justin Moore's reaction to this result, recalls that Moore claimed a proof around 2012 and gave a videotaped lecture before an error was found and the claim was retracted.

Formalization

• OpenAI math release, Lean scope note for family 248 (release repository, 2026-10-06). States that the formalization rules out a positive normalized left-invariant mean on bounded real functions on the standard dyadic piecewise-linear group, with no explicit boundary constant or prescribed generating set.
• OpenAI math release, ThompsonNonamenability.lean (comparator statement) (release repository, Oct 2026). Gives the target statement thompson_F_nonamenable_composition: F is a group under composition of dyadic PL homeomorphisms of [0,1] with no InvariantMean. This file contains the statement only, with sorry.
• OpenAI math release, Thompson/Main.lean (release repository, Oct 2026). Proves thompson_F_nonamenable_composition from thompson_F_not_amenable in imported modules; this file has no sorry.

Related prior literature mentioned by others

• Kate Juschenko, Nicolás Matte Bon, Nicolas Monod and Mikael de la Salle, Extensive amenability and an application to interval exchanges (arXiv:1503.04977, 2015; Ergodic Theory and Dynamical Systems 38, 2018). Kim and Lodha cite this work in Lemma 1.2 when recasting the nonamenability argument using extensive amenability and invariant means on finite subsets.
• Sebastián Barbieri, Mathieu Sablik and Ville Salo, Self-simulable groups (arXiv:2104.05141, 2021; revised 2025-02-24). Salo's October 2026 blog post applies this work's equivalence between nonamenability and self-simulability of Thompson's F to derive symbolic-dynamical consequences of OpenAI's result.

Possibly relevant literature (found by the agent, not checked)

• Victor Guba, Amenability problem for Thompson's group F: state of the art (arXiv:2305.07113, J. Groups Complex. Cryptol. 15(1), 2023). A survey of density estimates and approaches to the problem; it relates to the paper's discussion of Guba's work, which cites two of Guba's articles but not this survey.
• Bronislaw Wajnryb and Pawel Witowicz, Richard Thompson group F is not amenable (arXiv:1408.2188, 2014; withdrawn 2015). An earlier claimed nonamenability proof that the authors withdrew because of an uncorrectable mistake; it is not among the earlier claims listed in the paper's introduction.
• Leva Beklaryan, The classification theorem for groups of homeomorphisms of the line. Nonamenability of Thompson's group F (arXiv:1112.1942, 2011; withdrawn 2012). Another earlier claimed nonamenability proof, withdrawn for "a crucial error in Theorem B*"; it is not among the earlier claims listed in the introduction.

Digests and expositions

• Ying Xie, What the Machine Invented: Mining New Mathematical Instruments from OpenAI's October 2026 Release of AI-Generated Mathematics (arXiv:2610.17090, 2026-10-12). Section 8.4.3 analyzes the recursive Hilbert-ball coloring, separated-pair transports and averaged displacement estimate, with disclosed AI assistance and an explicit statement that the survey does not certify the full proof. [AI-generated per source]

News and blogs

• Ville Salo, Thompson's F is self-simulable (SHIFT HAPPENS, 2026-10-08). Explains how the claimed nonamenability yields self-simulability and symbolic presentations of natural actions, while noting the difficulty of extracting explicit constructions from the paper.
• Azmat, Thompson's Group F: How OpenAI Tackles the Decades-Old Amenability Mystery (BinaryVerse AI, 2026-10-09). Gives a popular account of the recursive-coloring and approximate-fixed-point argument, the documented Lean scope and the distinction between the main proof and its companion-dependent corollaries.