Grothendieck's homotopy hypothesis for weak globular infinity-groupoids (Ara-Henry coherators)
In Pursuing Stacks (1983) Grothendieck defined weak globular -groupoids as models of a coherator, a globular theory obtained by freely adjoining coherence operations, and conjectured that they model homotopy types: their homotopy theory, with weak equivalences detected by components and homotopy groups, is equivalent to that of spaces. Maltsiniotis made the formulation precise; strict -groupoids are known to fail. Henry (2016) reduced the hypothesis to a pushout conjecture: attaching an -cell along the source face of an -cell of a cellular model is a weak equivalence. The case of 3-groupoids was settled by Henry and Lanari. Do Grothendieck -groupoids, for every coherator, recover the homotopy theory of spaces?
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Higher category theory; homotopy theory
- Posed by
- Alexander Grothendieck (Pursuing Stacks); precise formulation by Georges Maltsiniotis
- Year posed
- 1983
- Years open
- 43y
- Solved
- 2026-09-24
- Model
- Unreleased internal OpenAI model
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Unreviewed
- Publication
- Announced
- Collection
- OpenAI math release (October 2026), version adc7f12
- Significance
- 42 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Theorem 1.1 (Henry's pushout conjecture): for every Grothendieck coherator in the Ara-Henry convention, elementary expansions of cellular models are weak equivalences. Section 5 derives the canonical left semi-model structure and, through Henry's comparison, a Quillen equivalence with spaces, so the homotopy theory is independent of the coherator within that convention. It does not cover coherators outside the Ara-Henry convention, Grothendieck's weak -categories (the non-invertible case), or Taylor's generalized pushout conjecture for algebraic coherators.
What the AI did
The release README says the results were produced by an unreleased internal OpenAI model with a fixed procedure, on average about three hours of ChatGPT Pro thinking compute per result, and that some outputs build on earlier model results. This result is not among the README's exceptions (the Hodge conjecture for CM abelian varieties and the Re(s) > 11/12 zero-free region). The manuscript is authored 'OpenAI' and names no human author. The single manuscript (September 24, 2026) is the whole family.
Verification
No independent mathematician has checked this yet. Checked here: Theorem 1.1 and the abstract were read against the homotopy hypothesis as Maltsiniotis and Henry formulate it; the claim covers every Grothendieck coherator in the Ara-Henry convention, not every coherator in Maltsiniotis's broader sense. The proof was not refereed. lean/formalization.yaml lists GrothendieckElementaryExpansion (OAI.Grothendieck.elementary_expansion). Its comparator statement, read here, is Henry's pushout conjecture: for a coherator, a cellular model , an -cell and the pushout of the source inclusion along , the map is a weak equivalence (bijective on components and on all homotopy groups). The semi-model structure and the Quillen equivalence with spaces follow by Henry's published reduction and Section 5 and are not formalized. Not rebuilt here. Listed as Unreviewed rather than Lean-checked because its formal statement is Henry's pushout conjecture, and the step to the homotopy hypothesis is Henry's 2016 reduction.
Sources
- Lean proofLean proof of Henry's pushout conjecture (OAI.Grothendieck.elementary_expansion)Comparator statement: GrothendieckElementaryExpansion.lean
- CodeOpenAI math release: The Grothendieck homotopy hypothesis via elementary expansions
- Problem recordHenry, Algebraic models of homotopy types and the homotopy hypothesis (arXiv 1609.04622)