Episode 250, October 2026

Decidable means simple inside?

Three AI preprints claim the Boone–Higman conjecture, with higher finiteness

Covers result 250 in OpenAI’s catalog: all 3 papers. See its connections to other results and the work it cites.

Play Episode 250: Decidable means simple inside? An element of Thompson's group V cutting and pasting pieces of an interval.

4:46. English captions available. The video loads from YouTube when you press play.

Chapters

The claim, in plain words

Give a group by generators and rules. The word problem asks whether a given string of generators equals the identity. For many groups a computer can always tell, but in the 1950s Novikov and Boone built finitely presented groups whose word problem no computer can solve. There is a classical test: if a group sits inside a finitely presented simple group, run two searches at once. One looks for a proof that the word equals 1, the other for a proof that setting it to 1 collapses the simple group. Simplicity guarantees that one of them ends. In 1973 and 1974 William Boone and Graham Higman asked for the converse: does every finitely generated group with decidable word problem embed in a finitely presented simple group? Many families were already known, and since 2023 Belk, Bleak, Matucci, Zaremsky and others have added many more, including hyperbolic groups.

Result 250 is three OpenAI preprints of 35, 30 and 18 pages, all dated September 23, 2026. The first claims the Boone–Higman conjecture: a finitely generated group has decidable word problem exactly when it embeds in a finitely presented simple group. The second claims that the simple group can even be of type F∞, with a classifying space that has finitely many cells in each dimension. The third claims a single group of type F∞ that contains every finitely presented group.

What it doesn’t claim

An explicit or natural embedding: the construction goes through computability. The easy direction is classical. The universal group of the third paper is not simple. It maps onto the integers, and since it contains every finitely presented group, its own word problem cannot be decidable.

Where it stands

Posted as preprints: OpenAI, 3 papers, 83 pages, dated September 23, 2026
Peer reviewed: Not yet
Formalized in Lean: Yes: all three main theorems (docs)

Last checked October 19, 2026. None of the preprints has been revised. In Lean, all three main theorems are formalized: about 111,000 lines with no unproved steps. The formalization includes Higman’s embedding theorem and the Thompson-group theorems in the forms the papers use. We did not build it, and only the universal group is in the repository’s formalization list. OSVerify has not reviewed the papers. On October 8, Matthew Zaremsky crossed the conjecture off his public list of open problems. No detailed public check has appeared, and no error has been reported.

How the proof goes

The target. A twisted Brin–Thompson group of Belk and Zaremsky cuts and pastes pieces of a Cantor set. It is always simple and contains Thompson’s group V. Zaremsky proved in 2024 that it is also finitely presented when a finitely presented group acts faithfully and 2-transitively with finitely generated stabilizers.
The action. The first paper builds that action by one general method that works for any group with decidable word problem. It makes every element a commutator and builds an algebra over the two-element field from a program that knows its own code, with a simple core. Matrices over the algebra act on vectors, and the paper kills the hidden Steinberg kernel. Simplicity then lets any nonzero vector reach any other.
Type F∞. The second paper adds a combinatorial fact. Two finite families of idempotent matrices, one over the field with two elements and one over the field with three, force a homology class to be killed by both 2 and 3, so it is zero. A theorem of Belk and Zaremsky then finishes the proof.

The numbers in the video

Ours: for the rotation group of the icosahedron, rewriting gives 7 rules and 60 normal forms. The two searches settled all 8 test words there. In a non-simple group of order 12, 3 of 8 words left both searches stuck.
Ours: with 2-by-2 matrices over the two-element field, two-sided row operations put all 255 nonzero vectors in one orbit. One-sided operations split them into four.
Ours: 158 idempotents over the two-element field and 680 over the three-element field. The class has order exactly 2 and exactly 3, and its order becomes infinite without the relations linking the copies.

Read the source

Finite algebraic envelopes and the Boone–Higman conjecture (PDF), 35 pages.
Simple F∞ overgroups of groups with decidable word problem (PDF), 30 pages.
A universal group of type F∞ (PDF), 18 pages.
The Lean formalization notes.
The collection’s catalog, where this is result 250.

The 3 papers in this result

OpenAI groups related papers, such as alternative proofs, supporting results and consequences, into one result; we label the first paper it lists the main paper and the others companions.

Finite algebraic envelopes and the Boone–Higman conjecture main paper
Simple F∞ overgroups of groups with decidable word problem companion
A universal group of type F∞ companion

Transcript

Read the full script

0:00The question

Give a group by generators and rules. The word problem asks: does a given string of generators equal the identity? For many groups a computer can always tell; for the group of rotations of an icosahedron, ours found 7 rewriting rules that reduce every word to one of 60 normal forms. But in the 1950s Novikov and Boone built finitely presented groups whose word problem no computer can solve. There is a classical test. If a group sits inside a finitely presented simple group, run two searches at once: one for a proof that the word equals one, and one for a proof that setting it to one collapses the whole simple group. Simplicity guarantees that one search ends. Our toy: in the simple group of order 60, one search won for every test word; in a group of order 12 that is not simple, 3 of 8 words left both searches stuck. In 1973 and 1974, William Boone and Graham Higman asked for the converse: does every finitely generated group with a decidable word problem embed in a finitely presented simple group? Many families were already known, and since 2023 Belk, Bleak, Matucci, Zaremsky and others have added many more, including hyperbolic groups, using Thompson-like groups.

1:17The claim

Result 250 is three OpenAI preprints, 35, 30 and 18 pages, all dated September 23, 2026. The first claims the Boone–Higman conjecture: a finitely generated group has decidable word problem exactly when it embeds in a finitely presented simple group. The second claims the simple group can even be of type F∞: it has a classifying space with finitely many cells in each dimension. The third claims one group of type F∞ that contains every finitely presented group. Not claimed: an explicit or natural embedding, since the construction goes through computability. The easy direction is classical. And the universal group of the third paper is not simple: it maps onto the integers, and since it contains every finitely presented group, its own word problem cannot be decidable.

2:14How the proof goes

The target is a twisted Brin–Thompson group of Belk and Zaremsky, which cuts and pastes pieces of a Cantor set, is always simple, and contains Thompson’s group V. Zaremsky proved in 2024 that it is also finitely presented when a finitely presented group acts faithfully and 2-transitively, with finitely generated stabilizers. Our computer checked the commutator trick behind such simplicity, in Thompson’s group V, in 200 random trials. So the paper builds that action, by one general method that works for any group with decidable word problem. It makes every element a commutator, then builds an algebra over the two-element field from a program that knows its own code, with a simple core. Matrices over it act on vectors; the paper kills the hidden Steinberg kernel; and simplicity lets any nonzero vector reach any other. Our toy: with 2-by-2 matrices and two-sided row operations, all 255 nonzero vectors form one orbit; with one-sided operations, they split into four. For type F∞, the second paper adds a tiny combinatorial fact: two finite families of idempotent matrices, one over the field with two elements and one over the field with three, force a homology class to be killed both by two and by three, so it is zero; a theorem of Belk and Zaremsky then finishes. Our computer found 158 and 680 idempotents, and orders exactly two and three; drop the relations that link the copies, and the class has infinite order.

3:53Where it stands

The preprints are unrefereed and unchanged since release. In Lean, all three main theorems are formalized, about 111,000 lines with no unproved steps, including Higman’s embedding theorem and the Thompson-group theorems in the forms the papers use; we did not build it, and only the universal group is in the repository’s formalization list. OSVerify has not reviewed them. On October 8 Matthew Zaremsky crossed the conjecture off his public list of open problems; no detailed public check has appeared, and no error has been reported. If they hold, a computer can solve the word problem of a finitely generated group exactly when it lives inside a finitely presented simple group: an answer, 52 years after Boone and Higman asked.

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.