Grothendieck Homotopy Hypothesis: How the OpenAI Proof Reveals the Algebra of Spaces

Take a path, add a second path with the same endpoints, and join them by a homotopy. In a free algebra of paths, however, it creates new composites, inverses, and higher coherence cells as well. The September 24, 2026 OpenAI preprint proves that the entire extension leaves the homotopy type unchanged for cellular models of any Grothendieck coherator in the Ara–Henry convention. That result, Theorem 1.1, resolves Henry’s pushout conjecture. It also unlocks the Grothendieck homotopy hypothesis for these models: weak globular infinity-groupoids and spaces have equivalent homotopy theories.

1. Grothendieck Homotopy Hypothesis: What the OpenAI Proof Establishes

A space has points, paths between points, and homotopies between paths. Those homotopies can themselves be compared in higher dimensions. The hypothesis says that this hierarchy, equipped with the right algebraic operations and taken up to weak equivalence, captures the homotopy theory of spaces. The original preprint supplies the missing algebraic step and derives the comparison. The Poincaré conjecture offers a familiar example of homotopy information constraining a space under additional hypotheses. Here the aim is to compare entire homotopy theories. The preprint’s scope is every coherator satisfying Definition 2.1, which specifies how the operations are freely introduced and which pasting schemes can serve as their inputs.

Different choices of coherator can produce different categories of algebraic models. Both recover the same homotopy theory after weak equivalences are inverted.

2. Why Grothendieck’s Original Formulation Remained Difficult

Simplicial sets already model spaces through the classical realization and singular-complex equivalence. Grothendieck’s proposal asked for a different presentation, with paths and higher homotopies organized by their sources and targets. Maltsiniotis made that proposal precise using coherators. The specific question was whether the resulting weak globular models admit the required homotopy theory for each allowed coherator.

Under realization preserving homotopy groups, the simply connected types represented by strict globular infinity-groupoids are products of Eilenberg–Mac Lane spaces. Each such factor carries a single nonzero homotopy group. Requiring coherence laws to hold as exact identities restricts what the model can express. Weak composition allows different ways of composing to be related by higher cells, with further cells relating those comparisons. Earlier work established a corresponding comparison for suitable 3-groupoids. Lanari’s globular path construction supplied compositions, identities, and inverses, leaving compatibility with every higher operation open.

3. The Algebraic Framework: Globes, Coherators, and Higher Homotopies

A globular set has vertices in dimension zero, arrows in dimension one, and cells between parallel arrows in dimension two. Two positive-dimensional cells are parallel when they share their immediate source and target. All vertices count as parallel. The globular identities ensure that the two faces of a higher cell themselves share their lower faces. Thus a homotopy between arrows fixes their endpoints.

Write $d_j$ for the bare globe in dimension $j$, $D_j$ for its free algebraic model, and $\partial D_j$ for the free model on its boundary. Pasting schemes glue finitely many globes along matching faces. A coherator $C$ is a theory on these shapes. It is built in stages by freely adjoining fillers of specified parallel boundaries. In the Ara–Henry convention, a generator producing a $j$-cell takes a pasting scheme of height at most $j$, and every admissible parallel pair eventually has a filler. Composite operations can have larger input shapes. A model interprets these operations with their prescribed faces, while a cellular model is built from the empty model by boundary attachments, possibly through transfinitely many stages.

4. Henry’s Pushout Conjecture: The Missing Piece

The source inclusion $J_n\colon D_n\to D_{n+1}$ selects the source face of the next globe. An attaching map $a\colon D_n\to X$ chooses an existing cell. The pushout glues that face to the chosen cell inside the category of models of $C$.

Set $n=1$. Start with an arrow $a\colon x\to y$ in $X$. The pushout freely adds another arrow $a^\prime\colon x\to y$ and a 2-cell $\alpha\colon a\Rightarrow a^\prime$. The vertices stay fixed in this generating picture. The new arrow represents the same relative path class as the old one. But a new 2-cell can take part in higher operations, so equality of those two path classes says little by itself about all newly generated classes.

The inclusion has a retraction that sends the new arrow to $a$ and its comparison to the unit 2-cell on $a$. This gives a left inverse on homotopy groups. Surjectivity still needs proof: a class in the expanded model must come from a class in the original one. That distinction is the content of Henry’s pushout conjecture.

5. Theorem 1.1: Why Elementary Expansions Preserve Homotopy Groups

For every coherator in the stated convention, every cellular $X$, every $n\geq 0$, and every attaching cell $a\colon D_n\to X$, Theorem 1.1 says the canonical pushout map $i\colon X\to X^+$ induces a bijection on components $\pi_0$ and isomorphisms on all based homotopy groups $\pi_k$ for positive $k$. The selected cell can be any generator, composite, or coherence cell.

The proof uses Proposition 2.4 to test weak equivalence one boundary at a time. Given a boundary in the source and a target cell with its image boundary, find a source cell with exactly the prescribed boundary and a higher cell joining its image to the target cell. Dimension zero tests vertices up to paths. In higher dimensions, the criterion also recovers injectivity by applying it to joining cells. The division calculus behind the criterion undoes a composition up to homotopy while respecting specified faces. It lets the paper pass between based homotopy groups and relative classes of cells with arbitrary parallel boundaries.

6. Coskeletal Cutoffs and the Descending-Induction Strategy

The reflector $R_q$ leaves all cells and face maps through dimension $q$ intact. Above that level it puts exactly one filler over each boundary. Distinct parallel cells at the cutoff are still distinct. The dimension bound on generating operations lets their interpretations below and at the cutoff be copied from the original model. As a left adjoint, $R_q$ preserves the pushout and the cellular presentation.

Fix $q$ and work downward from $n=q$. At the top, lower cells are unchanged by the expansion. A target $q$-cell retracts to one with the prescribed boundary and has a unique joining cell to the image of that retracted cell. Higher tests use unique fillers directly. Once the higher expansion indices are settled, Lemma 3.6 shows that a weak equivalence built by boundary attachments strictly above $n$ splits when its source is cellular. It also stays a weak equivalence when pushed out to another cellular source.

7. From Globular Trees to Contractible Models

A free model on a pasting scheme is contractible in the sense that it is nonempty and every parallel pair of cells has a joining cell. The paper proves this using spines. For cells of dimension $n$, the spine keeps all cells through $n$ but has height at most $n+1$. A joining cell then meets the coherator’s arity bound, even if the original scheme was much taller. At depth $n$, the comparison diagrams have parallel $n$-cells as vertices and $n+1$-cells as edges. In Proposition 3.7, replace each oriented tree at that depth by a linear string on the same labeled vertices. The string belongs to a globular-sum shape, whose free model is contractible. The maps both ways keep the vertices and send an edge to a composite along the corresponding path, using inverses for backward steps.

Going from the tree to the string and back may replace an edge by a longer walk. Backtracking cancels up to higher homotopy, leaving the original edge class. The proof duplicates each edge with a joining cell, an expansion at index $n+1$, where the result is already known. Freeness turns those individual edge comparisons into maps on the entire model. Two-out-of-three makes the round trip a weak equivalence. Since it factors through the contractible string model, the tree model is contractible too. Adding a duplicate and a joining edge at each spine vertex makes a tree with extra leaves. Restoring the rest of the pasting scheme uses only the higher-index expansions and preserves contractibility.

8. Partial Cylinders: The Key to Controlling Higher Coherence

The object $P_j$ represents cylinders on $j$-cells. Mapping it into a model specifies a cylinder there. Below $n$, both endpoints are identical. At $n$, the cylinder is a single $n+1$-cell between parallel endpoints. In the path example, $P_1$ is $D_2$. Its map into the expanded model represents the move from $a$ to $a^\prime$ with both vertices fixed.

In higher dimensions the boundary already carries compatible cylinders. A one-sided prescribed-data object adds one endpoint disk to that boundary, and a two-sided object adds both. The two-sided object is the starting point for the higher cellular completion defining $P_j$. Proposition 4.2 proves that the higher one-sided objects and all completed cylinders are contractible. The gluing starts from a whiskered shape and attaches the already constructed lower-dimensional cylinders along shared faces in skeletal order. The upper-cell pushout lemma keeps each replacement a weak equivalence. The same procedure makes the cylinder object on a whole pasting scheme contractible, which is what the operation construction needs.

9. How the Proof Makes Every Higher Operation Compatible

The path functor $P$ has $j$-cells in $PY$ given by maps $P_j\to Y$ through the cutoff. Its two endpoint maps $p_0$ and $p_1$ read off the endpoint cells. The coherator’s generators must act on these cylinders in their original free stage order, since a prescribed face may use any operation already introduced. For each new generator, those earlier operations supply the boundary data, and the original operation on the model supplies both endpoint values. Contractibility of the cylinder object on its input shape lets the two-sided data extend across the representing cylinder. Choosing that extension once makes the operation natural in the target model.

Proposition 4.3 gives two different lifting properties. Each endpoint lifts every boundary inclusion, so it is a weak equivalence. Together the endpoints lift $J_n$. For the two-path example, prescribe one comparison at the source and two 2-cells leaving its endpoints. Those three arrows on four parallel paths form a tree. The missing comparison between the two target paths is an upper boundary attachment. The map from the tree model into the completed cylinder splits, giving the required extension into any target model.

10. The Retract Argument That Completes the Elementary-Expansion Proof

Cellularity of $X$ and the boundary lifts for $p_0$ give a section $h\colon X\to PX$. Reading its other endpoint defines $u=p_1h$, a weak equivalence by two-out-of-three. In the example, this yields compatible comparisons for paths throughout $X$, including $a$. Use the unit retraction $r\colon Y\to X$ of the expansion and the joint endpoint lift to extend the comparison over the disk introducing $a^\prime$. The joint lift $f\colon Y\to PY$ has the identity and $v=iur$ as endpoints.

Since each endpoint map is a weak equivalence, the section in this display is one, and so is $v$. The arrow $iu\colon X\to Y$ is a retract of $v$: use $i$ and $r$ on the domains and the identity on both codomains. Retract closure makes $iu$ a weak equivalence, and two-out-of-three with $u$ gives the result for $i$. To return to the original category, test a boundary in dimension $k$ and choose $q\geq\max\{n+1,k+1\}$. The lifted $k$-cell and its joining $k+1$-cell both lie in dimensions the reflector left intact. Those witnesses already exist in the original expansion.

11. From Henry’s Conjecture to a Quillen Equivalence With Spaces

Corollary 5.1 gives the canonical cofibrantly generated left semi-model structure. Boundary inclusions generate cofibrations, source inclusions detect fibrations by right lifting, and weak equivalences are still the maps detected by components and homotopy groups. Every object is fibrant, and cofibrant objects are retracts of cellular ones. The expansion theorem makes the source endpoint of each generating relative cylinder a weak equivalence, so the cylinder construction works on finitely cellular models.

Henry’s comparison identifies the completion of this finite cylinder category with models of the original coherator. The marked free vertex is homotopically terminal, giving the cylinder coherator used in that comparison. Corollary 5.2 identifies the adjunction: geometric realization goes from groupoids to spaces, and the fundamental infinity-groupoid functor goes back. The adjunction is a Quillen equivalence. Writing $\operatorname{Mod}(C)$ for the category of models, $W$ for its weak equivalences, and $\operatorname{Ho}(\mathrm{Spaces})$ for the homotopy category of spaces, the induced equivalence is

The localization on the left formally inverts weak equivalences. The Quillen comparison also identifies the derived maps between objects.

12. Lean Formalization, Mathematical Scope, and Remaining Limitations

OpenAI’s October release announcement describes the broader publication effort, which Binary Verse AI covers in its OpenAI mathematics release overview. The family 312 scope note and the Lean theorem statement identify the machine-checked result as the elementary-expansion theorem for arbitrary Ara–Henry coherators and boundary-cellular models. The semi-model structure and Quillen comparison are proved in the manuscript and fall outside the published formalization’s stated scope. Likewise, the result applies to the specified convention for coherators. Extending it to a theory with different admissibility rules would require checking the hypotheses again.

In this proof of the Grothendieck homotopy hypothesis, a parallel cell can be freely added together with its comparison cell without changing the homotopy type, even after the coherator generates new composites and coherences. Henry’s comparison turns that local invariance into an equivalence with spaces. Follow Binary Verse AI for more research explainers. For other uses of topology, see cell attachments in Wall’s D(2) problem, manifold symmetries in Hilbert–Smith, sphere boundaries in the Cannon conjecture, and the Nearby Lagrangian conjecture. For more on formal verification, see Fermat’s Last Theorem in Lean.