Topology·OpenAI Math·Result 312·Lean formalisation listed
The Grothendieck homotopy hypothesis
One of the 372 results in OpenAI's public mathematics catalogue, filed under topology: 1 preprint, the latest dated 24 September 2026. This page quotes OpenAI's own summary of the claim, links the paper and abstract, and will embed the animation.
Latest paper
The Grothendieck homotopy hypothesis via elementary expansions
The animation for this result has not been released yet. Subscribe on YouTube to catch it.
What OpenAI claims
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. (Lean)
Paper
The Grothendieck homotopy hypothesis via elementary expansions
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.
Status
Preprint. The paper has not been independently reviewed. Treat the result as OpenAI's claim until other mathematicians have checked it. If a video exists, it illustrates the statement; it is not the proof.
