Simple overgroups of type F-infinity for groups with solvable word problem (higher-finiteness Boone-Higman)
A group has type if it has a classifying space with finitely many cells in each dimension; type is finite presentation. The Boone-Higman conjecture asks for a finitely presented simple overgroup of every finitely generated group with solvable word problem. In the discussion following Question 5.6 of their survey 'Progress around the Boone-Higman conjecture', Belk, Bleak, Matucci and Zaremsky raise the higher-finiteness strengthening. Does every finitely generated group with solvable word problem embed in a simple group of type ?
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Geometric group theory; finiteness properties and simple groups
- Posed by
- James Belk, Collin Bleak, Francesco Matucci and Matthew Zaremsky (survey, arXiv:2306.16356, discussion after Question 5.6)
- Year posed
- 2025
- Years open
- 1y
- Solved
- 2026-09-23
- Model
- Unreleased internal OpenAI model
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Collection
- OpenAI math release (October 2026), version adc7f12
- Significance
- 25 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Theorem 1.1: every finitely generated group with decidable word problem embeds in a nontrivial simple group of type ; with the classical converse, these are exactly the finitely generated subgroups of simple groups of type . This implies the Boone-Higman conjecture. The classifying space may be infinite-dimensional; no torsion-freeness, finite cohomological dimension or type is claimed.
What the AI did
The release README says every result in openai/math was produced by an unreleased internal OpenAI model with a fixed procedure, on average about three hours of ChatGPT Pro thinking compute per result. This result is not one of the README's two exceptions (the Hodge conjecture for CM abelian varieties and the Re(s) > 11/12 zero-free region). The manuscript is authored 'OpenAI' and names no human author. It is the second of three Boone-Higman family manuscripts, all dated September 23, 2026.
Verification
No independent mathematician has checked this yet. Checked here: Theorem 1.1 was read against the survey's question; it gives an injective homomorphism of any finitely generated group with decidable word problem into a nontrivial simple group of type . Lean: lean/ComparatorChallenges/SimpleOvergroups.json exists with solution_module OAI.GroupTheory.SimpleOvergroups.Main, whose file exists at the pinned commit; this challenge is not in lean/formalization.yaml. The statement SimpleOvergroups.lean was read here: type is a Hausdorff connected CW complex of finite type with the group as fundamental group and a contractible covering space; the theorem gives a nontrivial simple group of that type with an injective homomorphism from G. This states the headline. Not rebuilt here. Permitted axioms: propext, Quot.sound, Classical.choice.
Sources
- PaperRelated in family: Finite algebraic envelopes and the Boone-Higman conjecture
- Lean proofLean proof (OAI.SimpleFInftyOvergroups.main)Comparator statement: SimpleOvergroups.lean
- CodeOpenAI math release: Simple F-infinity overgroups of groups with decidable word problem
- Problem recordBelk-Bleak-Matucci-Zaremsky, Progress around the Boone-Higman conjecture