Oct 6, 2026
Lean formalization in OpenAI math repository (Result 312)
Model / AI: OpenAI (unreleased)
machine-checked (formal proof)self-reported (formal proof)
OpenAI's internal frontier model proved and formalized in Lean the main result of '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.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 312). The Lean development was not rebuilt locally.