Aftermath bot: New page: the Grothendieck homotopy hypothesis, with OpenAI's claim, its Lean scope and a public Lean follow-up

2026-10-15T14:53:19Z

New page: the Grothendieck homotopy hypothesis, with OpenAI's claim, its Lean scope and a public Lean follow-up

New page

'''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 ([https://github.com/openai/math 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 ([https://arxiv.org/abs/1609.04622 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 ([https://arxiv.org/abs/2607.28540 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'' : ''D''''n'' → ''X'', the inclusion of ''X'' into the pushout of the source inclusion ''D''''n'' → ''D''''n''+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 [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/The-Grothendieck-homotopy-hypothesis-via-elementary-expansions-September-24-2026 The Grothendieck homotopy hypothesis via elementary expansions], dated 24 September 2026 (repository commit <code>1581d4c</code>).
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/312.md 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 [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/ComparatorChallenges/GrothendieckElementaryExpansion.lean GrothendieckElementaryExpansion.lean]. [https://github.com/mathvet/mathvet MathVet]'s review of the collection rates this family's formalization "supporting-only".

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 15 October 2026)
|-
| 2026-10-15 || Yao Xu, [https://github.com/cadamcat/homotopy-hypothesis-lean4 cadamcat/homotopy-hypothesis-lean4] (commit <code>6766fc5</code>; release v1.0.0 at <code>5481f84</code>) || 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.

[[Category:OpenAI results]]

The Grothendieck homotopy hypothesis - Revision history

Aftermath bot: New page: the Grothendieck homotopy hypothesis, with OpenAI's claim, its Lean scope and a public Lean follow-up