# The Grothendieck homotopy hypothesis

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [The Grothendieck homotopy hypothesis via elementary expansions](../../preprints/The-Grothendieck-homotopy-hypothesis-via-elementary-expansions-September-24-2026/paper.pdf)

## Scope

The Grothendieck homotopy hypothesis asks whether algebraic $\infty$-groupoids recover the homotopy theory of spaces. The formalized result is the elementary-expansion theorem used in this approach: 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 full comparison with the homotopy theory of spaces are not included.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Elementary-expansion weak equivalence | [GrothendieckElementaryExpansion.lean](../ComparatorChallenges/GrothendieckElementaryExpansion.lean) |