The Grothendieck homotopy hypothesis
The Grothendieck homotopy hypothesis asks whether Grothendieck's weak globular ∞-groupoids model the homotopy theory of spaces. In Pursuing Stacks the higher operations are specified by freely adjoining coherence operations to globular pasting diagrams; a coherator records these choices, and Maltsiniotis gave a precise formulation in terms of coherators, their models, and realization and fundamental ∞-groupoid functors. A manuscript dated 24 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims the hypothesis for every coherator in the Ara–Henry convention. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
Background
- As recounted in the manuscript's introduction: Henry (arXiv:1609.04622) isolated a pushout conjecture (Conjecture 5.3.3). Take a cellular ∞-groupoid X, choose an n-cell a, and freely adjoin a parallel n-cell together with an (n+1)-cell from a to it. The conjecture asserts that the resulting extension is a weak equivalence. Henry showed that it suffices both for a canonical semi-model structure and for the comparison with spaces (Theorem 5.3.5 and Corollary 5.3.13).
- The introduction also recalls that strict globular ∞-groupoids realize, among simply connected homotopy types, only products of Eilenberg–Mac Lane spaces (Ara), and that partial constructions of path objects are due to Bourke and Lanari. J. Taylor (arXiv:2607.28540, July 2026) formulated a generalized pushout conjecture for globular models of other algebraic structures.
The original result
- Claim. Fix any Grothendieck coherator in the Ara–Henry convention. For every cellular ∞-groupoid X, every n ≥ 0 and every cell a : Dn → X, the inclusion of X into the pushout of the source inclusion Dn → Dn+1 along a is a weak equivalence (Theorem 1.1). Weak equivalences induce a bijection on components and isomorphisms on all based homotopy groups. This resolves Henry's pushout conjecture. The manuscript then derives the canonical semi-model structure and its equivalence with the homotopy theory of spaces (Section 5), that is, the homotopy hypothesis for these coherators.
- Source. The manuscript The Grothendieck homotopy hypothesis via elementary expansions, dated 24 September 2026 (repository commit
1581d4c). - Formalization, as described by the repository. The scope note lean/docs/312.md states that the formalized result is the elementary-expansion theorem: for every Grothendieck coherator in the Ara–Henry convention and every boundary-cellular model, attaching an (n+1)-disk along its source n-face induces a weak equivalence. The later semi-model structure and the full comparison with the homotopy theory of spaces are not included. The comparator statement is GrothendieckElementaryExpansion.lean. MathVet's review of the collection rates this family's formalization "supporting-only".
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 15 October 2026) |
|---|---|---|---|---|
| 2026-10-15 | Yao Xu, cadamcat/homotopy-hypothesis-lean4 (commit 6766fc5; release v1.0.0 at 5481f84) |
Extension (formalization) | A Lean 4 proof of the homotopy hypothesis for coherators in the form stated by Maltsiniotis and Ara: for every coherator a topological realization exists, and for every realization the fundamental ∞-groupoid functor sends weak homotopy equivalences to weak equivalences and exhibits the homotopy category of its ∞-groupoids as the localization of spaces at the weak homotopy equivalences. It vendors the collection's Lean library of globular theories and coherators, including the elementary-expansion theorem, and follows Henry's framework. The README states that it was developed with AI assistance. | GitHub repository. Its verification record reports a full build, a main theorem depending only on Lean's three standard axioms, a fresh kernel replay, and acceptance by the Comparator tool with the nanoda kernel enabled. The record notes that Comparator ran with a development stand-in rather than a Landrun sandbox. |
Notes
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.