Simple, amenable, finitely presented?
An AI preprint claims an infinite group with all three properties
Covers result 253 in OpenAI’s catalog: its one paper. See its connections to other results and the work it cites.
4:13. English captions available. The video loads from YouTube when you press play.
Chapters
The claim, in plain words
Three properties of a group:
- Finitely presented: finitely many generators and rules.
- Simple: no normal subgroups except the trivial ones.
- Amenable: there are finite sets that barely move.
Finite simple groups have all three, but trivially. Infinite examples had only two at a time. Thompson’s group V (1965) is finitely presented and simple, but it contains free groups, so it is not amenable. Groups built from one-dimensional cut-and-shift dynamics are simple (Matui) and amenable (Juschenko and Monod, 2012), but they are never finitely presented. The question of all three at once was on record by 2008, and Juschenko and Monod named it the next problem. In 2021 de Cornulier wrote that, as far as he knew, there was not even a plausible candidate.
Result 253 is one OpenAI preprint, 58 pages, dated September 23, 2026. It claims an infinite group that is finitely presented, simple and amenable. The group rearranges pieces of several unit squares. The squares are cut along lines whose positions, and two of whose slopes, come from the golden ratio. The group is generated by cycling three identical pieces.
What it doesn’t claim
- An explicit list of rules. The relations are all words up to some length that are trivial in the group, and that length is never given. With the Lean version’s 206 squares, the paper’s list of generators alone has about 354 billion entries, by our count.
- The stronger finiteness condition called type F∞.
- Anything about other two-dimensional groups in general.
Where it stands
- Posted as a preprint
- OpenAI, 58 pages, dated September 23, 2026
- Peer reviewed
- Not yet
- Formalized in Lean
- Yes, for 206 squares (docs)
Last checked October 19, 2026. The preprint has not been revised. In Lean, the whole statement is formalized for 206 squares: infinite, finitely presented, simple and amenable. That is about 85,000 lines with no unproved steps (we did not build it). OSVerify has not reviewed the paper. On October 8, Matthew Zaremsky crossed the question off his list of open problems. We found no detailed public check, and no error has been reported.
How the proof goes
- Simple. After cutting, any piece fits into any piece of larger area, so small rearrangements can be built from cycles of three pieces. The alternating group on five letters is perfect. So a normal subgroup containing one nontrivial element contains small copies of it, and moving those copies around produces every generator.
- Amenable. For any finitely many moves, the paper builds random partitions of the squares into polygon cells. Each move just slides the cells, and the random law barely notices the slide. In two dimensions independent random choices are not enough, so the paper correlates them.
- Finitely presented. The group’s Schur multiplier is finitely generated. The paper builds a finitely presented central cover, using steep lines whose golden-ratio conjugate slope is tiny. Finitely many more relations then kill the central kernel.
The numbers in the video
- Ours: shifting an n×n square changes a fraction 2/n of it (0.031 at n = 64). A ball in a free group always changes by more than its own size.
- Ours: with independent random bits, a one-step slide becomes undetectable like 1/N in one dimension, but stays near 0.84 in two.
- Ours: under the Lean’s constants the steep slope is at least about 439,000, and its conjugate is under 0.000002 in size.
- Ours: a central cover of order 120 becomes the simple group of order 60 by adding one relation.
Read the source
- An infinite finitely presented simple amenable group (PDF), 58 pages.
- The Lean formalization notes.
- The collection’s catalog, where this is result 253.
The paper
OpenAI groups related papers into one result; this one has a single paper.
Transcript
Read the full script
0:00The question
Three properties of a group. Finitely presented: finitely many generators and rules. Simple: no normal subgroups except the trivial ones, so it cannot be broken into smaller groups. Amenable: it has finite sets that barely move, like a large square on a grid; our computer checked that shifting an n×n square changes a fraction 2/n of it, while a ball in a free group always changes by more than its own size. Finite simple groups have all three, but trivially. Infinite examples had two at a time. Thompson’s group V, from 1965, is finitely presented and simple, but contains free groups, so it is not amenable. Matui showed that groups built from 1-dimensional cut-and-shift dynamics are simple, and in 2012 Juschenko and Monod showed they are amenable; but such groups are never finitely presented. So all three at once was the obvious question: it was on record by 2008, and Juschenko and Monod named it the next problem. In two dimensions, cut-and-shift groups can contain free groups, so amenability can fail; in 2021 de Cornulier wrote that, as far as he knew, there was not even a plausible candidate.
1:12The claim
Result 253 is one OpenAI preprint, 58 pages, dated September 23, 2026. It claims an infinite, finitely presented, simple, amenable group. The group rearranges pieces of several unit squares, cut along lines whose positions, and two of whose slopes, come from the golden ratio; it is generated by cycling three identical pieces. Not claimed: an explicit list of rules. The relations are all words up to some length that are trivial in the group, and that length is never given. With the Lean version’s choice of 206 squares, the paper’s list of generators alone has about 354 billion entries, by our count. Also not claimed: the stronger finiteness condition called type F∞, or anything about other 2-dimensional groups in general.
2:03How the proof goes
Simple: after cutting, any piece fits into any piece of larger area, so any small rearrangement can be built from cycles of three pieces. Because the alternating group on 5 letters is perfect, a normal subgroup with one nontrivial element contains small copies of it, and moving those copies around produces every generator. Our computer checked the key identity: a 3-cycle is a commutator of two even permutations of 5 things. Amenable: for any finitely many moves, the paper builds random partitions of the squares into polygon cells that each move just slides, with a law that barely notices the slide. In two dimensions, independent random choices are not enough; our toy: in one dimension their detectability falls like 1/N, in two it stays near 0.84. The paper correlates them. Finitely presented: the paper shows the group’s Schur multiplier is finitely generated, and builds a finitely presented central cover, using steep lines whose golden-ratio conjugate slope is tiny. Under the Lean version’s constants, that slope must be at least about 439,000, and its conjugate under 0.000002 in size. Finitely many more relations then kill the central kernel. Our toy of that last step: a group of order 120 becomes the simple group of order 60 by adding one relation.
3:30Where it stands
The preprint is unrefereed and unchanged since release. In Lean, the whole statement is formalized for 206 squares: infinite, finitely presented, simple and amenable, about 85,000 lines with no unproved steps; we did not build it. OSVerify has not reviewed it. On October 8 Matthew Zaremsky crossed the question off his list of open problems; we found no detailed public check, and no error has been reported. If it holds, finitely presented, simple and amenable can live together: a golden-ratio jigsaw, 206 boards in the Lean version, with a finite rulebook that no one has written down.
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.