Simple overgroups of type F infinity for decidable word problems
Status OpenLLM status Open unverified
Top Open Problems unknownunknown Not reported cataloguedOpenOpenStatement
Definitions and mathematical statement
Statement recorded in the supplied source.
Does every finitely generated group with decidable word problem embed in a nontrivial simple group H admitting a classifying CW complex with finitely many cells in each dimension?Short English statement
Does every finitely generated group with decidable word problem embed in a nontrivial simple group H admitting a classifying CW complex with finitely many cells in each dimension?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/Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem-September-23-2026/README.md.
Statement licence: CC-BY-4.0 · Source file
Contributions 1
OpenAI claim summary for Math-2711
Decidability of the word problem for a finite generating set is the input hypothesis. The claimed simple overgroup has a classifying complex with only finitely many cells in each dimension; this is the requested $F_\infty$ strengthening. This is presented as a claimed affirmative answer.
Simple overgroups of type F infinity for decidable word problems
OpenAI's claim
OpenAI presents a proof in the selected manuscript. A group with finitely many generators and a decidable identity-word test is claimed to embed into a nontrivial simple group of type $F_\infty$.Mathematical statement of the claimed result
Result 1.
Consider a group $G$ generated by finitely many elements, with an algorithm deciding its word problem. The assertion supplies a nontrivial simple group $H$ of type $F_\infty$ and an embedding \[ \iota:G\hookrightarrow H. \] Type $F_\infty$ requires finite skeleta of a classifying space in all dimensions. The decidability condition on $G$ is part of this theorem.Outline of the argument
Encoded finite diagrams carry faithful actions with controlled stabilizers. A homological device for ascending tori provides fillings in every dimension, and stabilizers of finite type in a highly transitive action assemble the simple overgroup while retaining higher finiteness.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, Simple F_$\infty$ overgroups of groups with decidable word problem, 2026-09-23; citation key
OAI:Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem-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.