Boone–Higman embeddings with higher finiteness

What OpenAI claims

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)

Papers (3)

1. Finite algebraic envelopes and the Boone–Higman conjecture

   23 September 2026 · Preprint, not peer reviewed · PDF

   OpenAI's abstract 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.

2. Simple F∞ overgroups of groups with decidable word problem

   23 September 2026 · Preprint, not peer reviewed · PDF

   OpenAI's abstract 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.

3. A universal group of type F∞

   23 September 2026 · Preprint, not peer reviewed · PDF

   OpenAI's abstract 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.

Status

Preprint. The papers have not been independently reviewed. Treat the result as OpenAI's claim until other mathematicians have checked it. If a video exists, it illustrates the statement; it is not the proof.