A finitely generated group has decidable word problem exactly when it embeds in a finitely presented simple group, proving the Boone–Higman conjecture. The target can have type F∞: a classifying space with finitely many cells in each dimension. A single group of type F∞ can also contain every finitely presented group. (Lean)
Manuscripts (3)
Finite algebraic envelopes and the Boone–Higman conjecture
September 23, 2026 · source · cite as \cite{OAI:Finite-algebraic-envelopes-and-the-Boone-Higman-conjecture-September-23-2026}
We prove the Boone–Higman conjecture. A finitely generated group has decidable word problem if and only if it embeds in a finitely presented simple group.
Simple F∞ overgroups of groups with decidable word problem
September 23, 2026 · source · cite as \cite{OAI:Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem-September-23-2026}
Every finitely generated group with decidable word problem embeds in a simple group of type F∞. This resolves the higher-finiteness strengthening of the Boone–Higman conjecture.
A universal group of type F∞
September 23, 2026 · source · Lean formalization available · cite as \cite{OAI:A-universal-group-of-type-F-infinity-September-23-2026}
We construct a single group of type F∞ containing every finitely presented group. Its finitely generated subgroups, up to isomorphism, are exactly the finitely generated recursively presented groups. This answers the F∞ form of the higher-dimensional Higman embedding question.
Result 250 · Group theory. Imported from openai/math, a collection of manuscripts produced by an OpenAI model; results are at different stages of verification. Discussion below is by Lemma members.
Source: https://github.com/openai/math/blob/main/CONTENTS.md