Can this group be averaged?
An AI preprint claims Thompson’s group F is nonamenable
Covers result 248 in OpenAI’s catalog: its one paper. See its connections to other results and the work it cites.
4:46. English captions available. The video loads from YouTube when you press play.
Chapters
The claim, in plain words
A group is amenable if it has finite sets that almost do not move when shifted. In the plane, shifting a large ball by one step changes only its edge. In a free group on two generators, whose picture is a tree, every finite set leaks a fixed fraction however large it is. Thompson’s group F consists of increasing piecewise-linear maps of the unit interval, with breakpoints at dyadic fractions and slopes that are powers of two. Brin and Squier showed in 1985 that F contains no free group on two generators, and it is not built from finite and abelian pieces, so neither standard argument settles it. Geoghegan conjectured in 1979 that F is not amenable. Proofs were claimed in both directions over the years, and several were withdrawn.
Result 248 is one OpenAI preprint, 13 pages, dated September 23, 2026. It claims to prove Geoghegan’s conjecture. Concretely, there is one fixed finite set of elements such that, for every nonempty finite set of the group, one of them moves a fixed positive fraction of its points outside it.
What it doesn’t claim
An explicit constant. Unwinding the Lean definitions for the paper’s own map, we get tens of billions of intervals and a certified fraction below one in ten billion; any positive fraction is enough. F is also not the first nonamenable group without nonabelian free subgroups: Ol’shanskii found one in 1980, and Monod, and Lodha and Moore, gave piecewise-projective examples, close cousins of F. The paper’s two corollaries rest on other, unrefereed release papers.
Where it stands
- Posted as a preprint
- OpenAI, 13 pages, dated September 23, 2026
- Peer reviewed
- Not yet
- Checked in Lean
- Yes: the whole proof of the main theorem (docs)
Last checked October 19, 2026. The preprint has not been revised. In Lean, the whole proof of the main theorem is formalized, including the infinite-dimensional map: about 9,500 lines with no unproved steps (we did not build it). OSVerify has not reviewed the paper. Sang-hyun Kim and Yash Lodha posted their own human-written exposition of the proof on arXiv on October 13, and no error has been reported. Wikipedia still lists the problem as open, pending independent published sources.
How the proof goes
- Moving intervals. Every element of F turns a fine uniform grid into a dyadic partition, and F can carry any two separated dyadic intervals inside the unit interval onto any other two, in the same order, stretching each evenly.
- Colours. Each partition gets a colour, a point in the unit ball of an infinite-dimensional Hilbert space: zoom into each of D parent intervals, colour the zoomed partitions recursively, average, and apply a map f that moves every point of the ball by at least 1/2. In finite dimensions no such map exists (Brouwer). In infinite dimensions Benyamini and Sternfeld showed a Lipschitz one does, and the appendix builds one from a curve that comes in from far away and then spirals forever at radius 5/16.
- The contradiction. If F had nearly invariant finite sets, the colours on any two separated intervals would have the same average correlation, because one fixed element carries each such pair onto a reference pair. A variance count then makes the average colour almost a fixed point of f, which is impossible.
The numbers in the video
- Ours: the average number of edges leaving a ball, per element. Diamond-shaped balls in the plane go from 1.54 at radius 2 to 0.04 at radius 100. Balls in F are still about 1.9 at radius 9, but balls also fail in the amenable lamplighter group, whose real Følner sets go down to 0.17.
- Ours: closed walks up to 26 steps. The 2n-th root of the return probability is 0.756 for F, 0.753 for the free group and 0.866 for the plane, which is still far below 1. Short walks cannot decide amenability.
- Ours: the paper’s transport lemma, carrying [1/8, 1/4] and [5/8, 3/4] onto [1/2, 9/16] and [3/4, 7/8]. It gave a valid map for 300 of 300 random pairs.
Read the source
- Thompson's group F is nonamenable (PDF), 13 pages.
- The Lean formalization notes.
- Kim and Lodha’s human-written exposition (arXiv, October 2026).
- The collection’s catalog, where this is result 248.
The paper
OpenAI groups related papers into one result; this one has a single paper.
Transcript
Read the full script
0:00The question
Can you average over a group? On the integers or the plane, yes: take a huge square of points; shifting it one step changes only its edge. A group with such nearly invariant finite sets is called amenable. Our computer measured how many of each element’s 4 edges leave the set, on average: for balls in the plane, which are diamonds, it falls to 0.04 at radius 100. In a free group on two generators, a tree, every set leaks a fixed fraction, however large. Thompson’s group F is made of bent lines: increasing piecewise-linear maps of the unit interval, with breakpoints at dyadic fractions and slopes powers of two. It is generated by two such maps, x₀ and x₁, with two relations, which our computer checked hold exactly. Brin and Squier showed it contains no free group on two generators, so the usual reason for nonamenability fails; but it is not built from finite and abelian pieces either. In 1979 Geoghegan conjectured it is not amenable. Computers could not settle it. Our counts of closed walks, up to 26 steps, track the free group almost exactly; but at that length even the plane, which is amenable, is still far below one, the value amenability needs. Balls in F still have about 1.9 leaving edges per element at radius nine, but in the amenable lamplighter group balls fail too. Over the years, proofs were claimed in both directions; several were withdrawn.
1:31The claim
Result 248 is one OpenAI preprint, 13 pages, dated September 23, 2026. It claims to prove Geoghegan’s conjecture: Thompson’s group F is not amenable. Concretely, there is one fixed finite set of elements such that, for every nonempty finite set of the group, one of them moves a fixed positive fraction of its points outside it. Not claimed: an explicit constant. Unwinding the Lean definitions for the paper’s own map, we get tens of billions of intervals and a guaranteed fraction below one in ten billion, which is enough, since anything above zero will do. It is also not the first nonamenable group without nonabelian free subgroups: Ol’shanskii found one in 1980, and Monod, and Lodha and Moore, gave piecewise-projective examples, close cousins of F. And the two corollaries rest on other, unrefereed release papers.
2:29How the proof goes
The proof works with dyadic partitions of the interval. Any element of F turns a fine uniform grid into such a partition. And F can carry any two separated dyadic intervals inside it onto any other two, in the same order, stretching each evenly. Our computer built one example, carrying [1/8, 1/4] onto [1/2, 9/16], and found a valid map for 300 random pairs. Now colour each partition by a point in the unit ball of an infinite-dimensional Hilbert space: zoom into each of D parent intervals, colour the zoomed partitions recursively, average, and apply a map f. The trick is f: it moves every point of the ball by at least 1/2. In finite dimensions that is impossible, by Brouwer’s fixed point theorem; in infinite dimensions Benyamini and Sternfeld showed it can be done with a Lipschitz map, one that stretches distances by at most a fixed factor. The appendix builds one from a curve that comes in from far away and then spirals forever at radius 5/16, without coming back near itself. If F had nearly invariant finite sets, the colours on any two separated intervals would have the same average correlation, because one fixed element of F carries each such pair onto a single reference pair. A variance count then makes the average colour almost a fixed point of f. But f moves everything by a half. So nearly invariant sets cannot exist.
3:59Where it stands
The preprint is unrefereed and unchanged since release. In Lean, the whole proof of the main theorem is formalized, including the infinite-dimensional map, about 9,500 lines with no unproved steps; we did not build it. OSVerify has not reviewed it. Sang-hyun Kim and Yash Lodha posted their own human-written exposition of the proof on October 13, and no error has been reported; Wikipedia still lists the problem as open, pending independent sources. If it holds, Thompson’s group, after nearly half a century on the fence, cannot be averaged: pushed off by a colouring of intervals and a map that leaves no point where it was.
Spot a mistake?
This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.