OpenAI claim summary for Math-2710
mathematicsTop Open Problemscontributionliterature_reportClaim: literature report
Summary of a claim published in openai/math; not a claim by this platform.
The primary theorem proves both directions for every finitely generated G and an injective homomorphism into a finitely presented simple group. lean/docs/250.md documents this exact Boone--Higman equivalence. Within these assumptions, this is a claimed affirmative answer to the stated question.
Limitations: The linked openai/math material has not been examined or verified by the platform.
Manuscript
Contents
Decidable word problem and embedding in finitely presented simple groups
OpenAI's claim
OpenAI presents a proof in the selected manuscript. Every group with finite generators and a decidable word problem is claimed to embed in a finitely presented simple group.Mathematical statement of the claimed result
Result 1.
For any finitely generated group $G$, the claimed equivalence is \[ G\text{ has decidable word problem} \quad\Longleftrightarrow\quad \exists H\text{ finitely presented and simple}:\ G\hookrightarrow H. \] Both finite presentability and simplicity concern the containing group $H$.Outline of the argument
Finite algebraic data encode the input inside an affine envelope. The construction removes the Steinberg kernel and builds a two-transitive envelope, while a decreasing dependency bound makes the coding finite; simplicity and embedding follow from the resulting action.Formal verification
For family 250, the documented entries cover Boone--Higman equivalence, simple $F_\infty$ overgroups for decidable word problems, and one universal $F_\infty$ group. The converse characterization of all its recursively presented subgroups is extra manuscript scope. The listed Comparator files areBooneHigman.lean, SimpleOvergroups.lean, UniversalFInfinity.lean. Named declarations include OAI.UniversalFInfinity.universal_group_of_type_FInfinity. This site has not executed the Lean code. The scope descriptions do not certify the remaining manuscript arguments.Status caveat
OpenAI attributes these manuscripts to work by an internal model. Its release cautions that arguments without formalization can contain mistakes. This catalogue has not independently checked the proofs; the labels report the mathematical claims attributed to OpenAI.Sources
- OpenAI, Finite algebraic envelopes and the Boone–Higman conjecture, 2026-09-23; citation key
OAI:Finite-algebraic-envelopes-and-the-Boone-Higman-conjecture-September-23-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main. - Family 250: Lean scope.
- Comparator BooneHigman.json.
- Comparator BooneHigman.lean.
- Comparator SimpleOvergroups.json.
- Comparator SimpleOvergroups.lean.
- Comparator UniversalFInfinity.json.
- Comparator UniversalFInfinity.lean.
- OpenAI catalogue entry.