A universal group of type F-infinity containing every finitely presented group (F-infinity Higman embedding)
Higman's embedding theorem puts every finitely generated recursively presented group into a finitely presented group, and there is a universal finitely presented group containing all finitely presented ones. Fournier-Facio and Zaremsky asked for higher-dimensional versions (Question 1.3 of 'Finiteness properties and Higman's rope trick', 2026): can finitely generated recursively presented groups be embedded into groups of type , in particular type , and they showed that their rope-trick groups fail for this. Is there a single group of type into which every finitely presented group embeds?
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Construction
- Field
- Geometric group theory; finiteness properties and embedding theorems
- Posed by
- Francesco Fournier-Facio and Matthew C. B. Zaremsky (Question 1.3, arXiv:2607.21727)
- Year posed
- 2026
- Years open
- 0y
- 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
- 20 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Theorem 1.1 constructs one group of type containing every finitely presented group; by Higman's theorem its finitely generated subgroups are exactly the finitely generated recursively presented groups (Corollary 1.2). No word-problem hypothesis is imposed. The classifying space need not be finite-dimensional, so type is not claimed, and is not claimed simple.
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 third of three Boone-Higman family manuscripts, all dated September 23, 2026.
Verification
No independent mathematician has checked this yet. Checked here: Theorem 1.1 and Corollary 1.2 were read against Fournier-Facio-Zaremsky Question 1.3 as the manuscript quotes it; the form is answered positively. Lean: lean/formalization.yaml lists comparator UniversalFInfinity with declaration OAI.UniversalFInfinity.universal_group_of_type_FInfinity. The statement UniversalFInfinity.lean was read here: there is a group H of type (a Hausdorff connected CW complex with finitely many cells in each dimension, fundamental group H and a contractible covering space) such that every finitely presented group in the same universe embeds injectively in H. This states Theorem 1.1; the converse about recursively presented subgroups is not included. Not rebuilt here. Permitted axioms: propext, Quot.sound, Classical.choice.