# Boone–Higman embeddings with higher finiteness

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

- [Finite algebraic envelopes and the Boone–Higman conjecture](../../preprints/Finite-algebraic-envelopes-and-the-Boone-Higman-conjecture-September-23-2026/paper.pdf)
- [Simple $F_\infty$ overgroups of groups with decidable word problem](../../preprints/Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem-September-23-2026/paper.pdf)
- [A universal group of type $F_\infty$](../../preprints/A-universal-group-of-type-F-infinity-September-23-2026/paper.pdf)

## 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](../ComparatorChallenges/BooneHigman.lean) |
| Simple type $F_\infty$ overgroups of groups with decidable word problem | [SimpleOvergroups.lean](../ComparatorChallenges/SimpleOvergroups.lean) |
| Universal group of type $F_\infty$ | [UniversalFInfinity.lean](../ComparatorChallenges/UniversalFInfinity.lean) |