Boone–Higman embeddings with higher finiteness

The explanation

Take the integers under addition, written with one generator a. A word is a string like a a a⁻¹ a⁻¹. It means "step forward twice, then back twice". To test if a word returns to the start, add the exponents. Here 1 + 1 − 1 − 1 = 0, so the word is the identity. The word a a a⁻¹ has sum 1, so it is not. This adding rule is an algorithm, so the integers have a decidable word problem. In general, the word problem is decidable when an algorithm answers it for every wordSource 1.

A group is simple when it is nontrivial and its only normal subgroups are the trivial one and the whole group. A normal subgroup is one that is unchanged when you conjugate it by any element. The integers are not simple: the even numbers form a normal subgroup. A finitely presented group is one described by finitely many generators and finitely many rules.

In 1974, Boone and Higman matched decidable word problem with a chain G ≤ H ≤ KSource 2. Here H is simple and K is finitely presented. Here ≤ means "sits inside as a subgroup". They asked whether the simple group H could itself be finitely presentedSource 3. The obstacle is that finite presentation does not in general pass to subgroupsSource 4. So the two good properties lived in different groups. Thompson later made H finitely generated, but not finitely presentedSource 5.

The first paper proves the conjecture. A finitely generated group has decidable word problem exactly when it embeds in a finitely presented simple groupSource 6. The easy direction is classical. A nontrivial finitely presented simple group has decidable word problemSource 7. The hard direction builds a finitely presented group with a faithful two-transitive action on an infinite setSource 8. Two-transitive means any ordered pair of distinct points can be moved to any other such pair. A construction of Belk and Zaremsky then turns that action into a simple group.

The second paper asks for more. A group has type F∞ when some space modelling it has finitely many cells in each dimensionSource 9. Type F₂ is the same as finite presentationSource 9. The paper proves every such group embeds in a nontrivial simple group of type F∞Source 10. The third paper builds one group H of type F∞ that contains every finitely presented groupSource 11. Its finitely generated subgroups are exactly the recursively presented groups, those with a program that lists their rulesSource 12.

How sure is this? A computer proof checker called Lean has formal proofs of the Boone–Higman equivalence, the simple F∞ overgroups, and the universal F∞ group. The Lean note leaves out the converse about recursively presented subgroups. No specialist review of the papers has been published.

What it doesn't show. This does not give a fast algorithm for any word problem, and the Lean scope note leaves out the converse about recursively presented subgroups.