OpenAI claim summary for Math-3019

Elementary expansion for Grothendieck infinity-groupoids

OpenAI's claim

For every coherator under the Ara--Henry convention, weak globular infinity-groupoids are claimed to model spaces; elementary cellular expansions preserve components and all homotopy groups, resolving Henry's pushout question. The cited manuscript argues for that result; its relation to this problem is specified below.

Mathematical statement of the claimed result

Mathematical claim 1.

Fix any Grothendieck coherator $\mathcal C$ in the convention whose generating filler of dimension $j$ has pasting-scheme arity of dimension at most $j$. Let $D_n$ be the free model on an $n$-globe, with source inclusion $s_n:D_n\to D_{n+1}$. For any cellular $\mathcal C$-infinity-groupoid $X$ and any cell $a:D_n\to X$, $n\ge0$, OpenAI claims \[ X\longrightarrow X\amalg_{D_n}D_{n+1} \] is a weak equivalence, inducing a bijection of components and isomorphisms of all based homotopy groups. Cellular means built from the initial model by possibly transfinite boundary attachments. The statement is an elementary-expansion theorem for every coherator, used in the homotopy-hypothesis argument.

Outline of the argument

Manuscript 1 (family 312, 2026-09-24): Reflection preserves low-dimensional cells while making higher fillers unique. Descending induction on expansion dimension, combined with partial cylinders fixed on lower boundaries, controls newly generated composites and coherence cells. Stagewise interpretation of free operations gives endpoint lifts and a retract argument proving expansion invariance; the resulting semi-model structure then invokes the comparison with spaces.

Formal verification

For family 312, the scope page documents the following selections. Only the elementary disk-attachment weak equivalence for the specified coherator convention and boundary-cellular models is selected. The full semi-model construction and comparison with spaces are outside that declaration. The documented statement covers the main claim of manuscript 1. Its selected declaration also covers the clause used for this problem. Comparator files: GrothendieckElementaryExpansion.lean. Declarations: OAI.Grothendieck.elementary_expansion.

This site has not executed the Lean files or checked their dependencies. These descriptions report the scope of the linked declarations, rather than a new verification of the proofs.

Status caveat

OpenAI attributes these results to an internal model. Its release notice cautions that results lacking full formalization can contain mistakes. This site has not independently assessed the proofs; a solved label records the scope of the reported claim.

Sources

• OpenAI, The Grothendieck homotopy hypothesis via elementary expansions, 2026-09-24; citation key OAI:The-Grothendieck-homotopy-hypothesis-via-elementary-expansions-September-24-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main.
• Family 312: Lean scope.
• Comparator GrothendieckElementaryExpansion.json.
• Comparator GrothendieckElementaryExpansion.lean.
• OpenAI catalogue entry.