The Boone–Higman conjecture
From OpenAI Aftermath
The Boone–Higman conjecture predicts that a finitely generated group has decidable word problem exactly when it embeds in a finitely presented simple group. Three manuscripts in OpenAI's public mathematics collection (github.com/openai/math), all dated 23 September 2026, claim the conjecture, its strengthening to simple groups of type F∞, and a single group of type F∞ containing every finitely presented group. The collection includes a Lean formalization of all three statements. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
Background
- As recounted in the introductions of the manuscripts:
- Higman's embedding theorem characterizes the finitely generated subgroups of finitely presented groups as the recursively presented groups. Boone and Higman showed that a finitely generated group has decidable word problem if and only if it embeds in a simple subgroup of a finitely presented group, and asked whether the simple group could itself be finitely presented. Thompson obtained a finitely generated simple overgroup with decidable word problem.
- Positive cases of the conjecture include hyperbolic and contracting self-similar groups (Belk, Bleak, Matucci and Zaremsky), Baumslag–Solitar and free-by-cyclic groups (Bux, Llosa Isenrich and Wu), and automorphism groups of free groups and mapping class groups (Belk, Fournier-Facio, Hyde and Zaremsky). The twisted Brin–Thompson groups of Belk and Zaremsky, with Zaremsky's finite-presentation criterion, embed a suitable acting group in a simple group.
- The question of simple overgroups of type F∞ appears in the survey of Belk, Bleak, Matucci and Zaremsky. Leary proved that every countable group embeds in a group of type FP2, and Fournier-Facio and Zaremsky asked whether recursively presented groups embed in groups of type Fn and related the question to embeddings into groups of type FPn.
The original results
- Claim. Theorem 1.1 of Finite algebraic envelopes and the Boone–Higman conjecture states that a finitely generated group has decidable word problem if and only if it embeds in a finitely presented simple group. Theorem 1.1 of Simple F∞ overgroups of groups with decidable word problem states that every finitely generated group with decidable word problem embeds in a nontrivial simple group of type F∞. Theorem 1.1 of A universal group of type F∞ states that there is a group of type F∞ into which every finitely presented group embeds, so that its finitely generated subgroups are exactly the recursively presented groups.
- Method, as described: the Boone–Higman manuscript embeds the given group in a finitely presented group with a faithful two-transitive action on a countable set whose point stabilizers are finitely generated, built from Steinberg groups over a finitely presented algebra, and then applies Zaremsky's criterion for twisted Brin–Thompson groups. The higher-finiteness manuscript uses a highly transitive action whose point stabilizers satisfy a new criterion for type F∞, and the universal-group manuscript proves that an ascending HNN extension of a universal finitely presented group has type F∞ by uniform chain fillings.
- Sources. The manuscripts Finite algebraic envelopes and the Boone–Higman conjecture, Simple F∞ overgroups of groups with decidable word problem and A universal group of type F∞ at commit
1581d4c. - Formalization, as described by the repository. The scope note states that the formalization proves the Boone–Higman equivalence in full, the embedding of every finitely generated group with decidable word problem into a nontrivial simple group of type F∞, and the existence of one group of type F∞, fixed in advance, containing every finitely presented group; the universal manuscript's converse about recursively presented subgroups is not included. The Comparator statements are
BooneHigman.lean,SimpleOvergroups.leanandUniversalFInfinity.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 20 October 2026) |
|---|---|---|---|---|
| 2026-10-08 | L. Bartholdi and R. Mikhailov, Every countable group embeds in a group of type FPn, arXiv:2609.37562v2 | Extension (appendix) | Proves that for every n ≥ 2 every countable group embeds in a group of type FPn, and constructs a group of type Fn containing every recursively presented group. Version 2 records that, after the manuscript was completed, OpenAI proved that every finitely presented group embeds in a group of type F∞, citing the universal-group manuscript at commit adc7f12, and adds an appendix combining its controlled-filling argument with their construction to prove that every countable group embeds in a two-generator group of type FP∞. |
arXiv preprint; version 1 of 29 September 2026, version 2 of 8 October 2026. The arXiv record states that the paper was produced with the help of ChatGPT Astra. |
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026) |
Review (fidelity of the formal statements) | Rates this family "full": all three claims are stated, with decidability of the word problem as a computable predicate and type F∞ as an aspherical CW complex with finitely many cells in each dimension. It records sandboxed Comparator passes for BooneHigman, SimpleOvergroups and UniversalFInfinity. |
MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-10 | cert-machine, openai/math lane K: BooneHigman (run 38017370880), SimpleOvergroups and UniversalFInfinity (run 38019899278) | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept the three solutions, in 321 s, 958 s and 411 s. The project reports two-kernel certification of 398 of 416 challenges of the collection. | Repository. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (time-outs, memory, errors) lists none of the three challenges, so all were accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-16 | J. Jardine, Lattice24, referee reviews of the Boone–Higman manuscript and the higher-finiteness manuscript in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995) | Review (AI-assisted audit) | Both reviews report no gap and state that the whole manuscript was read. For the Boone–Higman manuscript the minor notes are that Zaremsky's finite-presentation criterion and the Krstić–McCool presentation theorem are cited rather than proved, and that one invariance case analysis in the compiler appendix is terse but was re-derived. For the higher-finiteness manuscript they are that one substitution argument in the encoding section is very terse, and that the proof depends on two results of the companion manuscript, whose statements the reviewer matched; the second review adds that its independent pass on those companion results found no gap. | Part of an audit of the collection's manuscripts that the audit describes as complete. The reviews are published under CC BY 4.0. |
Notes
- The earlier results are due to the authors named in the Background section, as recounted by the manuscripts.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
