VibeMathedMath problems solved with AI
Sign in

The Boone-Higman conjecture: groups with solvable word problem embed in finitely presented simple groups

Higman's embedding theorem (1961) characterizes finitely generated subgroups of finitely presented groups as the recursively presented groups. Boone and Higman (1974) proved that a finitely generated group has solvable word problem if and only if it embeds in a simple group that in turn embeds in a finitely presented group, and asked whether the simple overgroup itself can be chosen finitely presented. Thompson later obtained a finitely generated simple overgroup, and the conjecture was proved for hyperbolic groups, Baumslag-Solitar and free-by-cyclic groups, Out(Fn)\mathrm{Out}(F_n) and mapping class groups, among others. Does every finitely generated group with solvable word problem embed in a finitely presented simple group?

Result
Proved(see note)
Status
Candidate (review pending)
AI contribution
AI-discovered
Method
Argument
Field
Combinatorial group theory; word problem and embedding theorems
Posed by
William W. Boone and Graham Higman (J. Austral. Math. Soc. 18, 1974, p. 43)
Year posed
1974
Years open
52y
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
50 / 100
Disclosed cost
—
Wikipedia
No dedicated article

What was actually shown

Theorem 1.1: a finitely generated group has decidable word problem if and only if it embeds in a finitely presented simple group. The route is Theorem 1.2: every such group embeds in a finitely presented group with a faithful two-transitive action on a countable set with finitely generated point stabilizers, built as a mapping torus of an affine Steinberg group over finitely presented F2\mathbb F_2-algebras, which Zaremsky's criterion for twisted Brin-Thompson groups turns into a finitely presented simple overgroup. The higher-finiteness strengthening is the companion's separate entry; no explicit bound on the size of the presentation is given.

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. The family has three manuscripts dated September 23, 2026: this one, a companion proving the stronger type F∞F_\infty version, and a companion constructing a universal group of type F∞F_\infty.

Verification

No independent mathematician has checked this yet. Checked here: Theorem 1.1 was read against the Boone-Higman question; it states the equivalence of decidable word problem and embedding in a finitely presented simple group for every finitely generated group, with no finite-presentation assumption on the input. Lean: lean/ComparatorChallenges/BooneHigman.json exists with solution_module OAI.GroupTheory.BooneHigman.Main, whose file exists at the pinned commit; this challenge is not in lean/formalization.yaml. The statement BooneHigman.lean was read here: for a finitely generated group, having some finite generating family whose word-equals-identity predicate is ComputablePred is equivalent to an injective homomorphism into a finitely presented group satisfying IsSimpleGroup, in the same universe. This states the headline. Not rebuilt here. Permitted axioms: propext, Quot.sound, Classical.choice.

Sources

Changelog1 change

Discussion