Boone–Higman embeddings with higher finiteness

3 papersLean

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.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 3

Finite algebraic envelopes and the Boone–Higman conjecture

OpenAI · 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.

Read PDF Download Source

Cite

@misc{OAI:Finite-algebraic-envelopes-and-the-Boone-Higman-conjecture-September-23-2026,
  author = {{OpenAI}},
  title = {{Finite algebraic envelopes and the Boone--Higman conjecture}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Finite-algebraic-envelopes-and-the-Boone-Higman-conjecture-September-23-2026/paper.pdf}{OAI:Finite-algebraic-envelopes-and-the-Boone-Higman-conjecture-September-23-2026}},
  year = {2026}
}

Simple F∞ overgroups of groups with decidable word problem

OpenAI · 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.

Read PDF Download Source

Cite

@misc{OAI:Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem-September-23-2026,
  author = {{OpenAI}},
  title = {{Simple $F_\infty$ overgroups of groups with decidable word problem}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem-September-23-2026/paper.pdf}{OAI:Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem-September-23-2026}},
  year = {2026}
}

A universal group of type F∞

OpenAI · 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.

Read PDF Download Source

Cite

@misc{OAI:A-universal-group-of-type-F-infinity-September-23-2026,
  author = {{OpenAI}},
  title = {{A universal group of type $F_\infty$}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-universal-group-of-type-F-infinity-September-23-2026/paper.pdf}{OAI:A-universal-group-of-type-F-infinity-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The Boone–Higman conjecture characterizes finitely generated groups with decidable word problem by embeddings into finitely presented simple groups. The formalization proves the equivalence in full: a finitely generated group has a computable word problem for a finite generating set exactly when it embeds by an injective homomorphism into a finitely presented simple group.

The formalization proves the higher-finiteness strengthening of the Boone–Higman conjecture: every finitely generated group with decidable word problem embeds by an injective homomorphism into a nontrivial simple group of type \(F_\infty\). Here type \(F_\infty\) means that the group has a classifying CW complex with finitely many cells in each dimension. No additional finiteness property of the original group is assumed.

The formalized result constructs one group \(H\) of type \(F_\infty\) containing every finitely presented group. Here type \(F_\infty\) means that \(H\) has a classifying space with finitely many cells in each dimension.

The group \(H\) is fixed before the groups embedded into it are chosen. No word-problem assumption is imposed, and the classifying space need not be finite-dimensional or have finitely many cells in total. The paper's converse about recursively presented subgroups is not included.

Comparator links

Result	Comparator statement
Boone–Higman equivalence	BooneHigman.lean
Simple type \(F_\infty\) overgroups of groups with decidable word problem	SimpleOvergroups.lean
Universal group of type \(F_\infty\)	UniversalFInfinity.lean

Scope note on GitHub →