Browse › Topology › 312 The Grothendieck homotopy hypothesis
The Grothendieck homotopy hypothesis via elementary expansions
Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion
Edit NOTES.md · Existing issues · Source on GitHub
Abstract
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.
If the PDF does not display here, open it directly: Open PDF.
Notes
No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.
Automatically collected notes (unreviewed)
work in progress
Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.
Formalization
- OpenAI math release, Lean scope notes for family 312 (lean/docs/312.md) (release Lean development, 2026-10-06). According to these notes, the Lean development formalizes the elementary-expansion weak-equivalence theorem (Theorem 1.1, Henry's pushout conjecture) for every Ara–Henry coherator and boundary-cellular model; the semi-model structure and the comparison with spaces are not included.
- Yao Xu (cadamcat), homotopy-hypothesis-lean4 (GitHub repository, Apache-2.0, 2026). An independent Lean 4/Mathlib project that vendors the release's elementary-expansion development and states a main theorem presenting Ho(∞-Gpd_C) as a localization of Top; the README cites this paper as its mathematical basis and says it was developed with AI assistance.
Possibly relevant literature (found by the agent, not checked)
- Johnathon Taylor, A Tale of Two Paths (arXiv:2609.20860, 2026-09-08). Gives a new presentation of a cylinder object for co-globular ∞-groupoids and proves it isomorphic to Lanari's cylinder construction, which may bear on the partial-cylinder and path construction of Section 3 (the paper cites Lanari 2020 but not this preprint).
- Johnathon Taylor, An Inductive Strategy Towards a Solution to the Generalized Homotopy Hypothesis (arXiv:2604.09867, 2026-04-10). Constructs an inductive coherator and gives a necessary and sufficient condition for transferring model structures from n-groupoids to (n+1)-groupoids, an alternative route to the semi-model structure and homotopy-hypothesis consequences in Sections 4–5.
- Johnathon Taylor, The Inductive Coherator For Grothendieck Infinity Groupoids (arXiv:2510.22326, 2025-10-25). Constructs an (∞,0)-coherator via distributive series of monads; relevant to the question of which coherators fall under the paper's Ara–Henry convention.
Digests and expositions
- Latent Seminar, The homotopy hypothesis: elementary expansions and partial cylinders (2026-10-07). This family-specific exposition explains finite cutoffs, tree comparisons and partial cylinders, and states that it does not independently verify the complete proof or audit the Lean development. [family-level]
News and blogs
- TheNextGenTechInsider, OpenAI Math Repository Shows Mismatch Between Headlines and Lean Proofs (Tech Pulse, 2026-10-12). The article discusses this paper's elementary-expansion formalization and the exclusion of the semi-model structure and comparison with spaces from its documented Lean scope. [AI-generated per source]
Elsewhere
- VibeMathed: Problem record
- Emergent Mind: family 312
Independent sites; their content is not reviewed here.
Cite
@misc{OAI:The-Grothendieck-homotopy-hypothesis-via-elementary-expansions-September-24-2026,
author = {{OpenAI}},
title = {{The Grothendieck homotopy hypothesis via elementary expansions}},
howpublished = {OpenAI Math Release preprint
\href{https://github.com/openai/math/blob/main/preprints/The-Grothendieck-homotopy-hypothesis-via-elementary-expansions-September-24-2026/paper.pdf}{OAI:The-Grothendieck-homotopy-hypothesis-via-elementary-expansions-September-24-2026}},
year = {2026}
}Lean formalization
OpenAI provides Lean files for this family: lean/docs/312.md. The Lean statements have not been checked by people against the paper's claims.
Family 312: The Grothendieck homotopy hypothesis
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.
This is the only paper in this family.