Decidable word problem and embedding in finitely presented simple groups
Status OpenLLM status Open unverified
Top Open Problems unknownunknown Not reported cataloguedOpenOpenStatement
Definitions and mathematical statement
Statement recorded in the supplied source.
Is it true that a finitely generated group has a decidable word problem exactly when it admits an injective homomorphism into a finitely presented simple group?Short English statement
Is it true that a finitely generated group has a decidable word problem exactly when it admits an injective homomorphism into a finitely presented simple group?Sources
- S1 Original question source or mathematical context. https://www.math.utah.edu/~bestvina/eprints/questions-updated.pdf.
- S2 Original question source or mathematical context. https://doi.org/10.4171/owr/2023/55.
- S3 OpenAI, manuscript citation page. Source of the formulation motivating this local problem. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Finite-algebraic-envelopes-and-the-Boone-Higman-conjecture-September-23-2026/README.md.
Statement licence: CC-BY-4.0 · Source file
Contributions 1
OpenAI claim summary for Math-2710
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.
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.