Spaces as algebra?
An AI preprint claims Grothendieck’s homotopy hypothesis for every coherator in the Ara–Henry convention
Covers result 312 in OpenAI’s catalog: its one paper. See its connections to other results and the work it cites.
4:31. English captions available. The video loads from YouTube when you press play.
Chapters
The claim, in plain words
In 1983, in Pursuing Stacks, Grothendieck proposed that spaces, up to homotopy, are the same thing as purely algebraic ∞-groupoids: points, paths between points, homotopies between paths, and so on forever, with composition, inverses and every coherence law supplied by operations rather than by geometry. Maltsiniotis later made this precise with coherators, theories built stage by stage by freely adding fillers for parallel pairs of operations. Strict versions are too rigid: by the Eckmann–Hilton argument two compatible operations collapse into one commutative operation, which is why strict groupoids cannot model even the 2-sphere. In 2016 Henry reduced the hypothesis to one gluing step: attach a new cell parallel to an existing one, plus a cell joining them, and show that nothing changes up to homotopy. In 2022 Henry wrote that this sounds like it should be very easy, but is still open at this point. Only dimension 3 was known, for groupoids of one particular kind, through work of Lanari and of Henry and Lanari.
Result 312 is one OpenAI paper, 26 pages, dated September 24, 2026, and made public October 6. It claims that Henry’s gluing step is a weak equivalence for every coherator in the Ara–Henry convention, where each generating filler’s input has dimension at most its output. Through Henry’s 2016 theorem, this gives a left semi-model structure and a Quillen equivalence with spaces: the homotopy hypothesis for these groupoids.
What it doesn’t claim
Coherators without that dimension bound, strict groupoids, higher categories that are not groupoids, other models such as Batanin’s, or a full model structure. The step to spaces depends on Henry’s 98-page 2016 preprint, which, as far as we found, has not appeared in a journal.
Where it stands
- Posted as a preprint
- OpenAI, 26 pages, dated September 24, 2026
- Peer reviewed
- Not yet
- Formalized in Lean
- In part: the core gluing theorem, not the comparison with spaces (docs)
Last checked October 19, 2026. The paper has not been revised. In Lean, the core gluing theorem is formalized against a challenge statement whose definitions, in our reading, match the paper’s, with an import closure of 58 files and about 12,700 lines; our scan finds no unproved steps, and we did not build it. The semi-model structure and the comparison with spaces are not formalized; a third party’s claim to have formalized the rest has not been checked. OSVerify has not reviewed it, and we found no specialist assessment. One public doubt was raised: on the algebraic topology mailing list on October 9, Johnathon Taylor, whose own paper the release cites for context, wrote that “there is definitely not elementary expansions in the sense the paper lays out”. They gave no argument, and no one followed up on the mathematics.
How the proof goes
- From the top down. The proof tests weak equivalence by lifting problems with exact boundaries. It first cuts the models off above some dimension q, forcing unique fillers there, then runs a descending induction from q down to 0. At each step, the gluing results already proved in higher dimensions make certain tree and cylinder models contractible, and this lets the paper build a path-object-like construction that interprets every operation of the coherator. A retract argument finishes the step, and the cutoff is removed at the end, because each test only involves finitely many dimensions.
- What Lean checks. The core gluing theorem, not the semi-model structure or the comparison with spaces. One footnote misquotes Henry’s definition, without affecting the argument.
The numbers in the video
- Ours: pasting shapes of globes, counted by size, follow the Catalan numbers 1, 1, 2, 5, 14, 42.
- Ours: in a toy coherator, one-dimensional operations on two composable arrows number 49 when built from two generating fillers and 3,556 when built from three.
- Ours: linking numbers 1, 2, 3 and 6 for the Hopf map and three variants of it.
Read the source
- The Grothendieck Homotopy Hypothesis via Elementary Expansions (PDF), 26 pages.
- Henry’s 2016 reduction (arXiv).
- The Lean formalization notes.
- The collection’s catalog, where this is result 312.
The paper
OpenAI groups related papers into one result; this one has a single paper.
Transcript
Read the full script
0:00The question
In 1983, in Pursuing Stacks, Grothendieck proposed that spaces, up to homotopy, are the same thing as purely algebraic ∞-groupoids: points, paths between points, homotopies between paths, and so on forever, with composition, inverses and every coherence law supplied by operations rather than by geometry. Maltsiniotis later made this precise with coherators, theories built stage by stage by freely adding fillers for parallel pairs of operations. The operations act on pasting shapes made of globes, and our computer counts these shapes by size: they follow the Catalan numbers, 1, 1, 2, 5, 14, 42. The operations multiply fast. In a toy coherator, our count of one-dimensional operations on two composable arrows gives 49 built from two generating fillers and 3,556 built from three, and every parallel pair needs a filler at the next stage. Strict versions are too rigid: by the Eckmann–Hilton argument, which our computer checks by brute force on small sets, two compatible operations collapse into one commutative operation. That is why strict groupoids cannot model even the 2-sphere, whose Hopf map has linked circles as fibres; our computer measures linking numbers of 1, 2, 3 and 6 for the Hopf map and three variants of it. In 2016 Henry reduced the hypothesis to one gluing step: attach a new cell parallel to an existing one, plus a cell joining them, and show that nothing changes up to homotopy. In 2022 Henry wrote that this sounds like it should be very easy, but is still open at this point. Only dimension 3 was known, for groupoids of one particular kind, through work of Lanari and of Henry and Lanari.
1:50The claim
Result 312 is one OpenAI paper, 26 pages, dated September 24 and made public October 6, 2026. It claims that Henry’s gluing step is a weak equivalence for every coherator in the Ara–Henry convention, where each generating filler’s input has dimension at most its output. Through Henry’s 2016 theorem, this gives a left semi-model structure and a Quillen equivalence with spaces: the homotopy hypothesis for these groupoids. Not claimed: coherators without that dimension bound, strict groupoids, higher categories that are not groupoids, other models such as Batanin’s, or a full model structure. The step to spaces depends on Henry’s 98-page 2016 preprint, which, as far as we found, has not appeared in a journal.
2:42How the proof goes
The proof tests weak equivalence by lifting problems with exact boundaries. It first cuts the models off above some dimension q, forcing unique fillers there, then runs a descending induction from q down to 0. At each step, the gluing results already proved in higher dimensions make certain tree and cylinder models contractible, and this lets the paper build a path-object-like construction that interprets every operation of the coherator. A retract argument finishes the step, and the cutoff is removed at the end, because each test only involves finitely many dimensions. In Lean, the core gluing theorem is formalized against a challenge statement whose definitions, in our reading, match the paper’s, with an import closure of 58 files and about 12,700 lines; our scan finds no unproved steps, and we did not build it. The semi-model structure and the comparison with spaces are not formalized, and a third party’s claim to have formalized the rest has not been checked. One footnote misquotes Henry’s definition, without affecting the argument.
3:50Where it stands
The paper is unrefereed and unchanged since release, and in the first 12 days we found no specialist assessment. One public doubt was raised: on the algebraic topology mailing list on October 9, Johnathon Taylor, whose own paper the release cites for context, wrote that there are definitely not elementary expansions in the sense the paper lays out. They gave no argument, and no one followed up on the mathematics. If it holds, Grothendieck’s ∞-groupoids, for every coherator in this convention, recover the homotopy theory of spaces, 43 years after Pursuing Stacks.
Spot a mistake?
This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.