The Boone–Higman conjecture and higher finiteness at CoolmAIth Games - math proofs, math puzzles and fun for AIs of all ages

A
D
V
E
R
T

I
S
E
M
E
N
T

The Boone–Higman conjecture and higher finiteness

at CoolmAIth Games - math proofs, math puzzles and fun for AIs of all ages

thinking... about 3 hours remaining

If this game doesn't work on your computer, go here for help. (Lean version available!)

expertly designed by an internal OpenAI model

Difficulty:	🧠🧠🧠🧠🧠	Ages:	13 - ∞
Skills:	symmetry	Levels:	3
Category:	Group theory	Lean version:	YES! ✔
Rate this game! 4.1 out of 5 (2,553 votes)

>>> How to Play <<<

Boone–Higman embeddings with higher finiteness. 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.

>>> Level Select <<<

LEVEL 1 Finite algebraic envelopes and the Boone–Higman conjecture

released 2026-09-23 | 6 theorems · 16 lemmas · 21 proofs · 15,718 words | PLAY LEVEL 1 » (pdf)

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.

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

released 2026-09-23 | 6 theorems · 18 lemmas · 21 proofs · 13,826 words | PLAY LEVEL 2 » (pdf)

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.

LEVEL 3 A universal group of type F∞

released 2026-09-23 | 2 theorems · 6 lemmas · 11 proofs · 8,321 words | PLAY LEVEL 3 » (pdf)

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.

More Group theory Games!
Thompson's group $F$ is nonamenable HOT!	A finitely generated counterexample to Eilenberg–Ganea	Amenability, unitarizability, and Ulam stability	A non-residually-finite torsion-free hyperbolic group
An infinite finitely presented simple amenable group	Classifying spaces and geometric obstructions for Artin groups	Quasi-isometric rigidity of virtually polycyclic groups	Howie's conjecture on equations over groups

COOLMAITH GAMES SPONSORS: (not real)
Big Al's USED GPUs	Epsilon & Delta LLP attorneys at limit	QED Bail Bonds	Hilbert's Hotel always a vacancy!

Cool Links: openai/math Lean Mathlib arXiv the real Coolmath Games

You are visitor number 000719

Thanks for visiting CoolmAIth Games
© 1997-2026 CoolmAIth Games. A parody. Not affiliated with Coolmath.com LLC or OpenAI.
Every proof here was written by an internal OpenAI model and lives at github.com/openai/math.
Best viewed in Netscape Navigator 4.0 at 800x600