Browse › Group theory › 250 Boone–Higman embeddings with higher finiteness
Simple F∞ overgroups of groups with decidable word problem
Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion
Edit NOTES.md · Existing issues · Source on GitHub
Abstract
Every finitely generated group with decidable word problem embeds in a simple group of type F∞. This resolves the higher-finiteness strengthening of the Boone–Higman conjecture.
If the PDF does not display here, open it directly: Open PDF.
Notes
No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.
Automatically collected notes (unreviewed)
work in progress
Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.
Formalization
- OpenAI math release, Lean scope notes for family 250 (lean/docs/250.md) (OpenAI math release, 2026-10-06). The release's scope notes state that the Lean development proves Theorem 1.1 (embedding of every finitely generated group with decidable word problem into a nontrivial simple group of type $F_\infty$), with the comparator statement in
lean/ComparatorChallenges/SimpleOvergroups.lean. [family-level] - lean-eval benchmark, Kuznetsov's theorem: finitely presented simple groups have solvable word problem (
boone_higman_simple) (Lean FRO lean-eval benchmark, undated). An independent Lean benchmark statement of the classical converse used in the introduction to characterize the groups in Theorem 1.1; on the page the proof issorry.
Related prior literature mentioned by others
- James Belk, Collin Bleak, Francesco Matucci and Matthew C. B. Zaremsky, Hyperbolic groups satisfy the Boone–Higman conjecture (arXiv:2309.06224, 2023; v3, 20 August 2025). The AI Proved What? family exposition identifies this earlier hyperbolic-group case as background to the general embedding claims. [family-level]
Possibly relevant literature (found by the agent, not checked)
- Fan Wu, Xiaolei Wu, Mengfei Zhao, Zixiang Zhou, Embedding groups into boundedly acyclic groups (arXiv:2407.07703, to appear in J. London Math. Soc.). Embeds every group of type F_n into a boundedly acyclic group of type F_n, and every finitely generated group into a finitely generated simple group via twisted Brin–Thompson groups; this is relevant to the paper's survey of earlier simple overgroups with finiteness properties.
- Francesco Fournier-Facio, Xiaolei Wu, Matthew C. B. Zaremsky, Abstract twisted Brin–Thompson groups (arXiv:2603.24687, 2026-03-25). Extends the twisted Brin–Thompson construction (the final step of this paper) to non-faithful actions, and relates the Boone–Higman conjecture to a characterization of solvable word problem within these groups.
Digests and expositions
- AI Proved What?, Decidable means simple inside? Three AI preprints claim the Boone–Higman conjecture (episode 250, October 2026). This AI-assisted video and transcript distinguish the three claimed results and outline the affine-action and higher-finiteness constructions. [AI-generated per source] [family-level]
Elsewhere
- VibeMathed: Problem record
- Emergent Mind: family 250
Independent sites; their content is not reviewed here.
Cite
@misc{OAI:Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem-September-23-2026,
author = {{OpenAI}},
title = {{Simple $F_\infty$ overgroups of groups with decidable word problem}},
howpublished = {OpenAI Math Release preprint
\href{https://github.com/openai/math/blob/main/preprints/Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem-September-23-2026/paper.pdf}{OAI:Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem-September-23-2026}},
year = {2026}
}Lean formalization
OpenAI provides Lean files for this family: lean/docs/250.md. The Lean statements have not been checked by people against the paper's claims.
Family 250: Boone–Higman embeddings with higher finiteness
A finitely generated group has decidable word problem exactly when it embeds in a finitely presented simple group, proving the Boone–Higman conjecture. The target can have type F∞: a classifying space with finitely many cells in each dimension. A single group of type F∞ can also contain every finitely presented group.
Other papers in this family:
- Finite algebraic envelopes and the Boone–Higman conjecture · September 23, 2026
- A universal group of type F∞ · September 23, 2026