The Grothendieck homotopy hypothesis 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 Grothendieck homotopy hypothesis

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:	donuts, coffee cups	Levels:	1
Category:	Topology	Lean version:	YES! ✔
Rate this game! 4.5 out of 5 (4,670 votes)

>>> How to Play <<<

The Grothendieck homotopy hypothesis. Proves the Grothendieck homotopy hypothesis for ∞-groupoids associated with every Grothendieck coherator in the Ara–Henry convention: these algebraic objects recover the homotopy theory of spaces.

>>> Level Select <<<

LEVEL 1 The Grothendieck homotopy hypothesis via elementary expansions

released 2026-09-24 | 1 theorem · 10 lemmas · 22 proofs · 12,928 words | PLAY LEVEL 1 » (pdf)

We prove the Grothendieck homotopy hypothesis for every Grothendieck coherator in the Ara–Henry convention: its weak globular infinity-groupoids recover the homotopy theory of spaces. We also resolve Henry's pushout conjecture, showing that elementary expansions preserve components and all homotopy groups of cellular infinity-groupoids.

More Topology Games!
The Kervaire invariant problem at the prime three HOT!	Quillen's conjecture in rational homology	Chai's invariant-ideal conjecture	Finite generation for the $K(n)$-local sphere
The chromatic Smith fixed-point problem for finite $p$-groups	The four-dimensional Singer conjecture	Curtis’s conjecture	Thomason model structures in every strict higher dimension

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