Lean statement

Elementary-expansion weak equivalence

Lean is a language for mathematical statements and proofs that a computer can verify. This page shows one statement file from OpenAI’s release, possible paper matches and independent reports. The code-like names below identify the definitions or theorems selected by the proof-verification settings.

Theorem selected for verification: OAI.Grothendieck.elementary_expansion

Lean statement file: GrothendieckElementaryExpansion.leanShow on the mapFamily 312. OpenAI lists this as a main result in its Lean catalogue.

See the candidate theorem Who ran the proof-verification program Report a comparison with the paper (GitHub issue)

The Lean statement

The lines of the Lean statement that state the theorem, then the definitions in the file that it uses.

theorem elementary_expansion (C : GlobularTheory.{v}) (hC : C.IsCoherator)    (X : C.Model) (hX : X.IsCellular) (n : ℕ)    (a : GlobularTheory.Model.disk C n ⟶ X)    (Y : C.Model) (i : X ⟶ Y)    (b : GlobularTheory.Model.disk C (n + 1) ⟶ Y)    (square : IsPushout a (GlobularTheory.Model.J C n) i b) :    GlobularTheory.Model.WeakEquivalence hC i := by  sorry

A Lean statement states the theorem and leaves its proof as sorry on purpose. OpenAI’s proof is in a separate solution module, and a program called Comparator checks that proof against this statement.

Definitions needed to read it

Local definitions the statement names, followed through the definitions they name in turn. The match is by name in the source text, so a name reached only through notation can be missed; the full file is below.

structure OAI.Grothendieck.GlobularSet line 9

structure GlobularSet where  Cell : ℕ → Type u  source : ∀ n, Cell (n + 1) → Cell n  target : ∀ n, Cell (n + 1) → Cell n  source_source : ∀ n x, source n (source (n + 1) x) = source n (target (n + 1) x)  target_source : ∀ n x, target n (source (n + 1) x) = target n (target (n + 1) x)

structure OAI.Grothendieck.GlobularSet.Hom line 19

structure Hom (X Y : GlobularSet.{u}) where  app : ∀ n, X.Cell n → Y.Cell n  source_app : ∀ n x, app n (X.source n x) = Y.source n (app (n + 1) x)  target_app : ∀ n x, app n (X.target n x) = Y.target n (app (n + 1) x)

definition OAI.Grothendieck.GlobularSet.Parallel line 24

def Parallel (X : GlobularSet.{u}) : ∀ n, X.Cell n → X.Cell n → Prop  | 0, _, _ => True  | n + 1, x, y => X.source n x = X.source n y ∧ X.target n x = X.target n y

definition OAI.Grothendieck.GlobularSet.Joined line 28

def Joined (X : GlobularSet.{u}) (n : ℕ) (x y : X.Cell n) : Prop :=  ∃ h : X.Cell (n + 1), X.source n h = x ∧ X.target n h = y

structure OAI.Grothendieck.Globe line 56
```
structure Globe where  dim : ℕ
```

inductive type OAI.Grothendieck.Globe.Face line 61

inductive Face : ℕ → ℕ → Type  | id (n : ℕ) : Face n n  | face {m n : ℕ} (lt : m < n) (side : Bool) : Face m n

definition OAI.Grothendieck.Globe.Face.comp line 67

def comp {m n k : ℕ} : Face m n → Face n k → Face m k  | .id _, g => g  | .face h b, .id _ => .face h b  | .face h b, .face h' _ => .face (h.trans h') b

definition OAI.Grothendieck.Globe.face line 84

def face {m n : ℕ} (h : m < n) (side : Bool) : Globe.mk m ⟶ Globe.mk n :=  Face.face h side

definition OAI.Grothendieck.Globe.source line 87

def source (n : ℕ) : Globe.mk n ⟶ Globe.mk (n + 1) := face (Nat.lt_succ_self n) false

definition OAI.Grothendieck.Globe.target line 89

def target (n : ℕ) : Globe.mk n ⟶ Globe.mk (n + 1) := face (Nat.lt_succ_self n) true

abbreviation OAI.Grothendieck.GlobularPresheaf line 93

abbrev GlobularPresheaf := Globeᵒᵖ ⥤ Type u

definition OAI.Grothendieck.GlobularPresheaf.underlying line 97

def underlying (X : GlobularPresheaf.{u}) : GlobularSet.{u} where  Cell n := X.obj (op (Globe.mk n))  source n := X.map (Globe.source n).op  target n := X.map (Globe.target n).op  source_source n x := by    have h := congrArg (fun f => X.map f) (congrArg Quiver.Hom.op (show Globe.source n ≫ Globe.source (n + 1) = Globe.source n ≫ Globe.target (n + 1) from rfl))    simpa only [op_comp, X.map_comp, types_comp_apply] using ConcreteCategory.congr_hom h x  target_source n x := by    have h := congrArg (fun f => X.map f) (congrArg Quiver.Hom.op (show Globe.target n ≫ Globe.source (n + 1) = Globe.target n ≫ Globe.target (n + 1) from rfl))    simpa only [op_comp, X.map_comp, types_comp_apply] using ConcreteCategory.congr_hom h x

definition OAI.Grothendieck.GlobularPresheaf.underlyingMap line 108

def underlyingMap {X Y : GlobularPresheaf.{u}} (f : X ⟶ Y) : X.underlying.Hom Y.underlying where  app n := f.app (op (Globe.mk n))  source_app n x := by    exact ConcreteCategory.congr_hom (f.naturality (Globe.source n).op) x  target_app n x := by    exact ConcreteCategory.congr_hom (f.naturality (Globe.target n).op) x

definition OAI.Grothendieck.GlobularPresheaf.disk line 115

def disk (n : ℕ) : GlobularPresheaf.{u} := uliftYoneda.{u}.obj (Globe.mk n)

inductive type OAI.Grothendieck.Table line 122

inductive Table : ℕ → Type  | globe (n : ℕ) : Table n  | attach {last : ℕ} (T : Table last) (b h : ℕ) (left : b < last) (right : b < h) : Table h

definition OAI.Grothendieck.Table.height line 128

def height : {n : ℕ} → Table n → ℕ  | _, .globe n => n  | _, .attach T _ h _ _ => max T.height h

definition OAI.Grothendieck.Table.realizeWithLast line 132

noncomputable def realizeWithLast : {n : ℕ} → Table n →    (Σ X : GlobularPresheaf.{0}, GlobularPresheaf.disk n ⟶ X)  | _, .globe n => ⟨GlobularPresheaf.disk n, 𝟙 _⟩  | _, .attach T _ h hl hr =>    let prev := T.realizeWithLast    let f := GlobularPresheaf.face hl true ≫ prev.2    let g := GlobularPresheaf.face hr false    ⟨pushout f g, pushout.inr f g⟩

definition OAI.Grothendieck.Table.realize line 141

noncomputable def realize {n} (T : Table n) : GlobularPresheaf.{0} := T.realizeWithLast.1

definition OAI.Grothendieck.Table.lastInclusion line 143

noncomputable def lastInclusion {n} (T : Table n) : GlobularPresheaf.disk n ⟶ T.realize :=  T.realizeWithLast.2

abbreviation OAI.Grothendieck.Shape line 148
```
abbrev Shape := Σ n, Table n
```

definition OAI.Grothendieck.Shape.globe line 156

def globe (n : ℕ) : Shape := ⟨n, Table.globe n⟩

definition OAI.Grothendieck.Shape.attach line 173

def attach (S : Shape) (b h : ℕ) (hl : b < S.1) (hr : b < h) : Shape :=  ⟨h, Table.attach S.2 b h hl hr⟩

definition OAI.Grothendieck.Shape.seam line 176

noncomputable def seam (S : Shape) {b : ℕ} (hl : b < S.1) : globe b ⟶ S :=  show GlobularPresheaf.disk b ⟶ S.realize from    GlobularPresheaf.face hl true ≫ S.2.lastInclusion

definition OAI.Grothendieck.Shape.inl line 180

noncomputable def inl (S : Shape) (b h : ℕ) (hl : b < S.1) (hr : b < h) :    S ⟶ S.attach b h hl hr :=  pushout.inl (GlobularPresheaf.face hl true ≫ S.2.lastInclusion)    (GlobularPresheaf.face hr false)

28 more definitions are reached the same way; the full file lists them.

Possible paper match, with no recorded review

Atlas selected this possible match by comparing words in the Lean statement with every statement in the family. No review of whether the statements mean the same thing is recorded.

Words of the Lean statement, its names split into words, that also appear in the theorem: pushout, source, square, inclusion, map, cellular, coherator, cell and two more. Found in the paper’s title, which its main theorem states: expansions, elementary and homotopy. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: grothendieck.

Theorem 1.1 of The Grothendieck homotopy hypothesis via elementary expansions

Theorem

Fix any Grothendieck coherator \mathcal C. Let X be a cellular \mathcal C-infinity-groupoid, let n\ge0, and let a:D_n\to X be any cell. In the pushout square

A diagram here is drawn in the paper: see it at the passage.

where s_n is the source inclusion, the map i:X\to X^+ is a weak equivalence.

Section 1, Introduction Read it in the paper TeX source, line 50

Show the TeX

Fix any Grothendieck coherator \(\mathcal C\).
Let \(X\) be a cellular \(\mathcal C\)-infinity-groupoid, let \(n\ge0\),
and let \(a:D_n\to X\) be any cell.  In the pushout square
\[
\begin{tikzpicture}[baseline=(current bounding box.center),
                   node distance=1.25cm and 2.2cm,>=Stealth]
\node (a) {\(D_n\)};
\node (b) [right=of a] {\(D_{n+1}\)};
\node (c) [below=of a] {\(X\)};
\node (d) at (b |- c) {\(X^+\)};
\draw[->] (a) -- node[above] {\(s_n\)} (b);
\draw[->] (a) -- node[left] {\(a\)} (c);
\draw[->] (b) -- (d);
\draw[->] (c) -- node[below] {\(i\)} (d);
\end{tikzpicture}
\]
where \(s_n\) is the source inclusion, the map \(i:X\to X^+\)
is a weak equivalence.

Other possible paper matches, closest wording first

Proposition 2.4 of The Grothendieck homotopy hypothesis via elementary expansions. Words of the Lean statement, its names split into words, that also appear in the theorem: parallel, pair, boundary, components, map, homotopy and four more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: induces.
Proposition 4.3 of The Grothendieck homotopy hypothesis via elementary expansions. Words of the Lean statement, its names split into words, that also appear in the theorem: functor, natural, morphisms, boundary, inclusions, map and two more.
Proposition 3.4 of The Grothendieck homotopy hypothesis via elementary expansions. Words of the Lean statement, its names split into words, that also appear in the theorem: shape, nonempty, globular, free and models.
Corollary 5.1 of The Grothendieck homotopy hypothesis via elementary expansions. Words of the Lean statement, its names split into words, that also appear in the theorem: trivial, groups, category, components, cellular, coherator and four more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: grothendieck.
Proposition 4.2 of The Grothendieck homotopy hypothesis via elementary expansions. Words of the Lean statement, its names split into words, that also appear in the theorem: height, cellular, weak, equivalence and model.
Corollary 5.2 of The Grothendieck homotopy hypothesis via elementary expansions. Words of the Lean statement, its names split into words, that also appear in the theorem: realization, category, coherator, homotopy, equivalence and model. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: grothendieck.

How Atlas selects possible matches: it compares words in the Lean statement with every statement in the family. It also splits Lean names into words. The release’s label and note receive less weight; a main theorem wins a close match. If the Lean wording yields no clear match, Atlas uses the catalogue description. This selects passages to compare; it does not establish that they mean the same thing.

Reported Comparator runs

two independent groups report that Comparator accepted runs for this Lean statement file: Carlos Toledo’s cert-machine; MathVet. Each group reports its own Comparator run for this statement file. Atlas has not repeated the runs.

For a configured theorem, Comparator tests whether OpenAI’s proof proves the exact Lean statement. Some files instead configure definitions for comparison by name and type. Acceptance does not establish that the statement means the same thing as the paper’s theorem.

Carlos Toledo’s cert-machine

How they ran it, in their words

Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule; every family’s challenge statements read against OpenAI’s headline, clause by clause. Decider: Comparator (leanprover/comparator d03acab1 = tag v4.34.0, built with the release’s toolchain v4.34.1), lean4export 076e8e57, landrun 811cfff5, nanoda_lib 3a240721 — on GitHub’s Linux runners (.github/workflows/openai-math-kernel.yml), one j…

Accepted Their term: “CERTIFIED”.
Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.
Reported 10 October 2026, at the release version shown here. Original verification report

MathVet

How they ran it, in their words

An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge. Its protocol describes a planned error-rate study; this import does not establish that the study has been completed.

Accepted Their term: “comparator-sandboxed-pass”.
Re-run through Comparator in a sandboxed virtual machine: accepted.
Reported 8 October 2026, at the release version shown here. Original verification report

What an accepted Comparator run would establish

If Comparator is run under this configuration and accepts, the solution proves the configured theorem using only the allowed axioms, and the Lean kernel accepts every step.

This configuration lists no definition holes, so every definition the statement uses is compared as it is written in this file.

Allowed axioms: propext, Quot.sound, Classical.choice

Acceptance leaves open whether the Lean statement means the same thing as the paper’s theorem, whether the paper’s other claims are correct, and whether the result is new. Those questions require comparing the definitions and statements, reviewing the paper’s arguments, and reading the earlier literature.

Do family 312’s Lean statements express the advertised result?

These assessments compare all the family’s Lean statements with the whole result OpenAI describes in its catalogue. They do not assess this statement alone. Each group uses its own published rules.

Neither group finds that the Lean statements express or imply the whole advertised result. They describe what the statements express in different terms.

MathVet
Finds a supporting or a different result stated Their term: “supporting-only”.
The challenge statements state a lemma or auxiliary result, not the headline. Their record
Their note: Only elementary_expansion: for a coherator C (Ara-Henry convention, encoded by hand), a cellular model X and a pushout of J n : disk n → disk (n+1) along any disk n → X, the inclusion X → Y is a WeakEquivalence (bijection on π₀ and on every π_n at every basepoint). The homotopy hypothesis itself (comparison of these ∞-groupoid models with spaces) is not stated; docs: 'the later semi-model structure and full comparison with the homotopy theory of spaces are not included'.
Definitions the group asks readers to compare with the paper: GlobularTheory, CellularPresentation, IsCoherator C := Nonempty C.CellularPresentation ∧ ∀ p : AdmissiblePair, ∃ z, Fills (Morphism.id C) p z and Model are hand-built encodings of Grothendieck coherators and their models ; noncomputable def unit C hC n := Classical.choose (hC.2 (C.unitPair n)): the degenerate-cell operation used to define baseCell, Loops, HomotopyGroup and hence WeakEquivalence is chosen by Classical.choose (any choice is valid, but the notion is not canonical)
Carlos Toledo’s cert-machine
Finds part of it stated, or a narrower or weaker statement Their term: “NARROWER — DECLARED”.
The challenge statements state less than the headline, and OpenAI’s Lean note says so. Their record
Their note: The Grothendieck homotopy hypothesis (the comparison of the homotopy theory of coherator ∞-groupoids with spaces) is not stated; only the elementary-expansion theorem (Henry's pushout conjecture) is.

Read the complete assessments on the family page.

OpenAI’s own note on what this Lean statement covers

“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.”
Quoted from OpenAI’s Lean note for this family

An AI agent drafted an interpretation of that note, classifying this statement as “states a paper’s theorem as the paper does”. No human review of the draft is recorded.

Supporting material

The complete Lean statement file

476 lines, copied from release version fd4aeeb. A name defined in this file links to its line; pointing at the name shows its definition.

Declared in this fileOpenAI’s library at fd4aeebOther linked names open the current documentation for Mathlib, Lean’s mathematical library.

Links in the file: 229 to its own declarations, 99 to Mathlib’s documentation. 73 declared names also link to the same declaration in OpenAI’s library. 3 identifiers stay plain because they resolve to no single declaration: variables Lean binds automatically, notation, or names the scan of the pinned sources did not find. OpenAI uses Mathlib version d13f23b. The linked documentation describes the current version, so names that have since changed may be missing there.

import Mathlibnamespace OAIuniverse u v wnamespace Grothendieckstructure GlobularSet where  Cell : ℕ → Type u  source : ∀ n, Cell (n + 1) → Cell n  target : ∀ n, Cell (n + 1) → Cell n  source_source : ∀ n x, source n (source (n + 1) x) = source n (target (n + 1) x)  target_source : ∀ n x, target n (source (n + 1) x) = target n (target (n + 1) x)namespace GlobularSet@[ext]structure Hom (X Y : GlobularSet.{u}) where  app : ∀ n, X.Cell n → Y.Cell n  source_app : ∀ n x, app n (X.source n x) = Y.source n (app (n + 1) x)  target_app : ∀ n x, app n (X.target n x) = Y.target n (app (n + 1) x)def Parallel (X : GlobularSet.{u}) : ∀ n, X.Cell n → X.Cell n → Prop  | 0, _, _ => True  | n + 1, x, y => X.source n x = X.source n y ∧ X.target n x = X.target n ydef Joined (X : GlobularSet.{u}) (n : ℕ) (x y : X.Cell n) : Prop :=  ∃ h : X.Cell (n + 1), X.source n h = x ∧ X.target n h = ydef Boundary (X : GlobularSet.{u}) : ℕ → Type u  | 0 => PUnit  | n + 1 => { p : X.Cell n × X.Cell n // X.Parallel n p.1 p.2 }def boundary (X : GlobularSet.{u}) : ∀ n, X.Cell n → X.Boundary n  | 0, _ => PUnit.unit  | n + 1, x => ⟨(X.source n x, X.target n x), by      cases n with      | zero => trivial      | succ n => exact ⟨X.source_source n x, X.target_source n x⟩⟩def Hom.boundaryMap {X Y : GlobularSet.{u}} (f : Hom X Y) : ∀ n, X.Boundary n → Y.Boundary n  | 0, _ => PUnit.unit  | n + 1, b => ⟨(f.app n b.1.1, f.app n b.1.2), by      cases n with      | zero => trivial      | succ n =>        exact ⟨by rw [← f.source_app, ← f.source_app, b.2.1],          by rw [← f.target_app, ← f.target_app, b.2.2]⟩⟩end GlobularSetopen CategoryTheory CategoryTheory.Limits Opposite@[ext]structure Globe where  dim : ℕnamespace Globeinductive Face : ℕ → ℕ → Type  | id (n : ℕ) : Face n n  | face {m n : ℕ} (lt : m < n) (side : Bool) : Face m nnamespace Facedef comp {m n k : ℕ} : Face m n → Face n k → Face m k  | .id _, g => g  | .face h b, .id _ => .face h b  | .face h b, .face h' _ => .face (h.trans h') bend Faceinstance : Category Globe where  Hom m n := Face m.dim n.dim  id m := .id m.dim  comp := Face.comp  id_comp _ := rfl  comp_id {X Y} f := by cases X; cases Y; cases f <;> rfl  assoc {W X Y Z} f g h := by    cases W; cases X; cases Y; cases Z    cases f <;> cases g <;> cases h <;> rfldef face {m n : ℕ} (h : m < n) (side : Bool) : Globe.mk m ⟶ Globe.mk n :=  Face.face h sidedef source (n : ℕ) : Globe.mk n ⟶ Globe.mk (n + 1) := face (Nat.lt_succ_self n) falsedef target (n : ℕ) : Globe.mk n ⟶ Globe.mk (n + 1) := face (Nat.lt_succ_self n) trueend Globeabbrev GlobularPresheaf := Globeᵒᵖ ⥤ Type unamespace GlobularPresheafdef underlying (X : GlobularPresheaf.{u}) : GlobularSet.{u} where  Cell n := X.obj (op (Globe.mk n))  source n := X.map (Globe.source n).op  target n := X.map (Globe.target n).op  source_source n x := by    have h := congrArg (fun f => X.map f) (congrArg Quiver.Hom.op (show Globe.source n ≫ Globe.source (n + 1) = Globe.source n ≫ Globe.target (n + 1) from rfl))    simpa only [op_comp, X.map_comp, types_comp_apply] using ConcreteCategory.congr_hom h x  target_source n x := by    have h := congrArg (fun f => X.map f) (congrArg Quiver.Hom.op (show Globe.target n ≫ Globe.source (n + 1) = Globe.target n ≫ Globe.target (n + 1) from rfl))    simpa only [op_comp, X.map_comp, types_comp_apply] using ConcreteCategory.congr_hom h xdef underlyingMap {X Y : GlobularPresheaf.{u}} (f : X ⟶ Y) : X.underlying.Hom Y.underlying where  app n := f.app (op (Globe.mk n))  source_app n x := by    exact ConcreteCategory.congr_hom (f.naturality (Globe.source n).op) x  target_app n x := by    exact ConcreteCategory.congr_hom (f.naturality (Globe.target n).op) xdef disk (n : ℕ) : GlobularPresheaf.{u} := uliftYoneda.{u}.obj (Globe.mk n)def face {m n : ℕ} (h : m < n) (side : Bool) : disk.{u} m ⟶ disk.{u} n :=  uliftYoneda.{u}.map (Globe.face h side)end GlobularPresheafinductive Table : ℕ → Type  | globe (n : ℕ) : Table n  | attach {last : ℕ} (T : Table last) (b h : ℕ) (left : b < last) (right : b < h) : Table hnamespace Tabledef height : {n : ℕ} → Table n → ℕ  | _, .globe n => n  | _, .attach T _ h _ _ => max T.height hnoncomputable def realizeWithLast : {n : ℕ} → Table n →    (Σ X : GlobularPresheaf.{0}, GlobularPresheaf.disk n ⟶ X)  | _, .globe n => ⟨GlobularPresheaf.disk n, 𝟙 _⟩  | _, .attach T _ h hl hr =>    let prev := T.realizeWithLast    let f := GlobularPresheaf.face hl true ≫ prev.2    let g := GlobularPresheaf.face hr false    ⟨pushout f g, pushout.inr f g⟩noncomputable def realize {n} (T : Table n) : GlobularPresheaf.{0} := T.realizeWithLast.1noncomputable def lastInclusion {n} (T : Table n) : GlobularPresheaf.disk n ⟶ T.realize :=  T.realizeWithLast.2end Tableabbrev Shape := Σ n, Table nnamespace Shapenoncomputable def realize (S : Shape) : GlobularPresheaf.{0} := S.2.realizedef height (S : Shape) : ℕ := S.2.heightdef globe (n : ℕ) : Shape := ⟨n, Table.globe n⟩noncomputable instance : Category Shape where  Hom S T := S.realize ⟶ T.realize  id S := 𝟙 S.realize  comp f g := f ≫ g  id_comp := Category.id_comp  comp_id := Category.comp_id  assoc := Category.assocnoncomputable def face {m n : ℕ} (h : m < n) (side : Bool) : globe m ⟶ globe n :=  GlobularPresheaf.face h sidenoncomputable def source (n : ℕ) : globe n ⟶ globe (n + 1) := face (Nat.lt_succ_self n) falsenoncomputable def target (n : ℕ) : globe n ⟶ globe (n + 1) := face (Nat.lt_succ_self n) truedef attach (S : Shape) (b h : ℕ) (hl : b < S.1) (hr : b < h) : Shape :=  ⟨h, Table.attach S.2 b h hl hr⟩noncomputable def seam (S : Shape) {b : ℕ} (hl : b < S.1) : globe b ⟶ S :=  show GlobularPresheaf.disk b ⟶ S.realize from    GlobularPresheaf.face hl true ≫ S.2.lastInclusionnoncomputable def inl (S : Shape) (b h : ℕ) (hl : b < S.1) (hr : b < h) :    S ⟶ S.attach b h hl hr :=  pushout.inl (GlobularPresheaf.face hl true ≫ S.2.lastInclusion)    (GlobularPresheaf.face hr false)noncomputable def inr (S : Shape) (b h : ℕ) (hl : b < S.1) (hr : b < h) :    globe h ⟶ S.attach b h hl hr :=  pushout.inr (GlobularPresheaf.face hl true ≫ S.2.lastInclusion)    (GlobularPresheaf.face hr false)end Shapestructure TheoryData where  Hom : Shape → Shape → Type v  id : ∀ S, Hom S S  comp : ∀ {S T U}, Hom S T → Hom T U → Hom S U  id_comp : ∀ {S T} (f : Hom S T), comp (id S) f = f  comp_id : ∀ {S T} (f : Hom S T), comp f (id T) = f  assoc : ∀ {R S T U} (f : Hom R S) (g : Hom S T) (h : Hom T U),    comp (comp f g) h = comp f (comp g h)  base : ∀ {S T}, (S ⟶ T) → Hom S T  base_id : ∀ S, base (𝟙 S) = id S  base_comp : ∀ {R S T} (f : R ⟶ S) (g : S ⟶ T), base (f ≫ g) = comp (base f) (base g)namespace TheoryDatastructure Obj (C : TheoryData.{v}) where  shape : Shapeinstance (C : TheoryData.{v}) : Category C.Obj where  Hom S T := C.Hom S.shape T.shape  id S := C.id S.shape  comp f g := C.comp f g  id_comp := C.id_comp  comp_id := C.comp_id  assoc := C.assocnoncomputable def arity (C : TheoryData.{v}) : Shape ⥤ C.Obj where  obj S := ⟨S⟩  map f := C.base f  map_id := C.base_id  map_comp := C.base_compdef PreservesGlobularSums (C : TheoryData.{v}) : Prop :=  ∀ (S : Shape) (b h : ℕ) (hl : b < S.1) (hr : b < h),    IsPushout (C.arity.map (S.seam hl)) (C.arity.map (Shape.face hr false))      (C.arity.map (S.inl b h hl hr)) (C.arity.map (S.inr b h hl hr))end TheoryDatastructure GlobularTheory extends TheoryData.{v} where  sums : toTheoryData.PreservesGlobularSumsnamespace GlobularTheoryabbrev Obj (C : GlobularTheory.{v}) := C.toTheoryData.Obj@[ext]structure Morphism (C D : GlobularTheory.{v}) where  map : ∀ {S T}, C.Hom S T → D.Hom S T  map_id : ∀ S, map (C.id S) = D.id S  map_comp : ∀ {R S T} (f : C.Hom R S) (g : C.Hom S T),    map (C.comp f g) = D.comp (map f) (map g)  map_base : ∀ {S T} (f : S ⟶ T), map (C.base f) = D.base fnamespace Morphismdef id (C : GlobularTheory.{v}) : Morphism C C where  map f := f  map_id _ := rfl  map_comp _ _ := rfl  map_base _ := rfldef comp {C D E : GlobularTheory.{v}} (f : Morphism C D) (g : Morphism D E) : Morphism C E where  map a := g.map (f.map a)  map_id S := by rw [f.map_id, g.map_id]  map_comp a b := by rw [f.map_comp, g.map_comp]  map_base a := by rw [f.map_base, g.map_base]end Morphismdef Parallel (C : GlobularTheory.{v}) {S : Shape} :    ∀ n, C.Hom (Shape.globe n) S → C.Hom (Shape.globe n) S → Prop  | 0, _, _ => True  | n + 1, f, g =>    C.comp (C.base (Shape.source n)) f = C.comp (C.base (Shape.source n)) g ∧    C.comp (C.base (Shape.target n)) f = C.comp (C.base (Shape.target n)) gstructure AdmissiblePair (C : GlobularTheory.{v}) where  n : ℕ  arity : Shape  height : arity.height ≤ n + 1  source : C.Hom (Shape.globe n) arity  target : C.Hom (Shape.globe n) arity  parallel : C.Parallel n source targetdef Fills {C D : GlobularTheory.{v}} (f : Morphism C D) (p : C.AdmissiblePair)    (z : D.Hom (Shape.globe (p.n + 1)) p.arity) : Prop :=  D.comp (D.base (Shape.source p.n)) z = f.map p.source ∧  D.comp (D.base (Shape.target p.n)) z = f.map p.targetdef IsFreeExtension {C D : GlobularTheory.{v}} (f : Morphism C D)    (G : Type v) (pair : G → C.AdmissiblePair)    (filler : ∀ g, D.Hom (Shape.globe ((pair g).n + 1)) (pair g).arity) : Prop :=  (∀ g, Fills f (pair g) (filler g)) ∧  ∀ (E : GlobularTheory.{v}) (a : Morphism C E)    (chosen : ∀ g, E.Hom (Shape.globe ((pair g).n + 1)) (pair g).arity),    (∀ g, Fills a (pair g) (chosen g)) →    ∃! b : Morphism D E, f.comp b = a ∧ ∀ g, b.map (filler g) = chosen gstructure CellularPresentation (C : GlobularTheory.{v}) where  stage : ℕ → GlobularTheory.{v}  initial : ∀ D : GlobularTheory.{v}, Nonempty (Unique (Morphism (stage 0) D))  step : ∀ r, Morphism (stage r) (stage (r + 1))  generators : ℕ → Type v  pair : ∀ r, generators r → (stage r).AdmissiblePair  filler : ∀ r g, (stage (r + 1)).Hom (Shape.globe ((pair r g).n + 1)) (pair r g).arity  free : ∀ r, IsFreeExtension (step r) (generators r) (pair r) (filler r)  inclusion : ∀ r, Morphism (stage r) C  compatible : ∀ r, (step r).comp (inclusion (r + 1)) = inclusion r  colimit : ∀ (D : GlobularTheory.{v}) (a : ∀ r, Morphism (stage r) D),    (∀ r, (step r).comp (a (r + 1)) = a r) →    ∃! b : Morphism C D, ∀ r, (inclusion r).comp b = a rdef IsCoherator (C : GlobularTheory.{v}) : Prop :=  Nonempty C.CellularPresentation ∧  ∀ p : C.AdmissiblePair, ∃ z, Fills (Morphism.id C) p znoncomputable def shapeGlobes : Globe ⥤ Shape where  obj n := Shape.globe n.dim  map f := uliftYoneda.map f  map_id n := by exact uliftYoneda.map_id n  map_comp f g := by exact uliftYoneda.map_comp f gnoncomputable def globes (C : GlobularTheory.{v}) : Globe ⥤ C.Obj :=  shapeGlobes ⋙ C.toTheoryData.aritystructure Model (C : GlobularTheory.{v}) where  presheaf : C.Objᵒᵖ ⥤ Type v  sums : ∀ (S : Shape) (b h : ℕ) (hl : b < S.1) (hr : b < h),    IsPullback      (presheaf.map (C.toTheoryData.arity.map (S.inl b h hl hr)).op)      (presheaf.map (C.toTheoryData.arity.map (S.inr b h hl hr)).op)      (presheaf.map (C.toTheoryData.arity.map (S.seam hl)).op)      (presheaf.map (C.toTheoryData.arity.map (Shape.face hr false)).op)namespace Modelinstance (C : GlobularTheory.{v}) : Category C.Model where  Hom X Y := X.presheaf ⟶ Y.presheaf  id X := 𝟙 X.presheaf  comp f g := f ≫ g  id_comp := Category.id_comp  comp_id := Category.comp_id  assoc := Category.assocnoncomputable def underlying {C : GlobularTheory.{v}} (X : C.Model) : GlobularSet.{v} :=  GlobularPresheaf.underlying (C.globes.op ⋙ X.presheaf)noncomputable def underlyingMap {C : GlobularTheory.{v}} {X Y : C.Model} (f : X ⟶ Y) :    X.underlying.Hom Y.underlying :=  GlobularPresheaf.underlyingMap (Functor.whiskerLeft C.globes.op f)noncomputable def freeShape (C : GlobularTheory.{v}) (S : Shape) : C.Model where  presheaf := yoneda.obj ⟨S⟩  sums T b h hl hr := ((C.sums T b h hl hr).op.map (yoneda.obj ⟨S⟩)).flipnoncomputable def disk (C : GlobularTheory.{v}) (n : ℕ) : C.Model :=  freeShape C (Shape.globe n)noncomputable def J (C : GlobularTheory.{v}) (n : ℕ) : disk C n ⟶ disk C (n + 1) :=  show (disk C n).presheaf ⟶ (disk C (n + 1)).presheaf from    yoneda.map (C.toTheoryData.arity.map (Shape.source n))structure BoundaryAttachment {C : GlobularTheory.{v}} {X Y : C.Model} (f : X ⟶ Y) where  index : Type v  dimension : index → ℕ  boundary : ∀ k, X.underlying.Boundary (dimension k)  cell : ∀ k, Y.underlying.Cell (dimension k)  cell_boundary : ∀ k, Y.underlying.boundary _ (cell k) =    (underlyingMap f).boundaryMap _ (boundary k)  universal : ∀ (Z : C.Model) (g : X ⟶ Z)    (z : ∀ k, Z.underlying.Cell (dimension k)),    (∀ k, Z.underlying.boundary _ (z k) = (underlyingMap g).boundaryMap _ (boundary k)) →    ∃! h : Y ⟶ Z, f ≫ h = g ∧ ∀ k, (underlyingMap h).app _ (cell k) = z kstructure CellularPresentation {C : GlobularTheory.{v}} (X : C.Model) where  order : Type v  linearOrder : LinearOrder order  orderBot : OrderBot order  succOrder : SuccOrder order  wellFoundedLT : WellFoundedLT order  initial : C.Model  isInitial : IsInitial initial  start : initial ⟶ X  chain : @TransfiniteCompositionOfShape _ _ order linearOrder orderBot    _ _ start succOrder wellFoundedLT  attachment : ∀ j, ¬ IsMax j → BoundaryAttachment    (chain.F.map (homOfLE (Order.le_succ j)))def IsCellular {C : GlobularTheory.{v}} (X : C.Model) : Prop := Nonempty X.CellularPresentationend Modeldef unitPair (C : GlobularTheory.{v}) (n : ℕ) : C.AdmissiblePair where  n := n  arity := Shape.globe n  height := Nat.le_succ n  source := C.id (Shape.globe n)  target := C.id (Shape.globe n)  parallel := by cases n <;> simp [Parallel]noncomputable def unit (C : GlobularTheory.{v}) (hC : C.IsCoherator) (n : ℕ) :    C.Hom (Shape.globe (n + 1)) (Shape.globe n) := Classical.choose (hC.2 (C.unitPair n))def Model.eval {C : GlobularTheory.{v}} (X : C.Model) {S T : Shape} (f : C.Hom S T) :    X.presheaf.obj (op (⟨T⟩ : C.Obj)) → X.presheaf.obj (op (⟨S⟩ : C.Obj)) :=  X.presheaf.map (show (⟨S⟩ : C.Obj) ⟶ ⟨T⟩ from f).opnoncomputable def Model.unitCell {C : GlobularTheory.{v}} (X : C.Model) (hC : C.IsCoherator)    (n : ℕ) (x : X.underlying.Cell n) : X.underlying.Cell (n + 1) :=  X.eval (C.unit hC n) xnoncomputable def Model.baseCell {C : GlobularTheory.{v}} (X : C.Model) (hC : C.IsCoherator)    (x : X.underlying.Cell 0) : ∀ n, X.underlying.Cell n  | 0 => x  | n + 1 => X.unitCell hC n (X.baseCell hC x n)def Model.Loops {C : GlobularTheory.{v}} (X : C.Model) (hC : C.IsCoherator)    (x : X.underlying.Cell 0) (n : ℕ) : Type v :=  { z : X.underlying.Cell (n + 1) // X.underlying.source n z = X.baseCell hC x n ∧      X.underlying.target n z = X.baseCell hC x n }def Model.Components {C : GlobularTheory.{v}} (X : C.Model) : Type v :=  Quot (X.underlying.Joined 0)def Model.HomotopyGroup {C : GlobularTheory.{v}} (X : C.Model) (hC : C.IsCoherator)    (x : X.underlying.Cell 0) (n : ℕ) : Type v :=  Quot (fun a b : X.Loops hC x n => X.underlying.Joined (n + 1) a.1 b.1)noncomputable def Model.loopsMap {C : GlobularTheory.{v}} {X Y : C.Model} (f : X ⟶ Y)    (hC : C.IsCoherator) (x : X.underlying.Cell 0) (n : ℕ) :    X.Loops hC x n → Y.Loops hC ((underlyingMap f).app 0 x) n := by  have hb : ∀ k, (underlyingMap f).app k (X.baseCell hC x k) =      Y.baseCell hC ((underlyingMap f).app 0 x) k := by    intro k    induction k with    | zero => rfl    | succ k ih =>      have h := ConcreteCategory.congr_hom (f.naturality        (show (op (⟨Shape.globe k⟩ : C.Obj)) ⟶ op ⟨Shape.globe (k+1)⟩ from          Quiver.Hom.op (C.unit hC k))) (X.baseCell hC x k)      change (underlyingMap f).app (k+1) (X.unitCell hC k (X.baseCell hC x k)) =        Y.unitCell hC k ((underlyingMap f).app k (X.baseCell hC x k)) at h      simpa only [baseCell, ih] using h  exact fun z => ⟨(underlyingMap f).app (n + 1) z.1,    by rw [← (underlyingMap f).source_app, z.2.1, hb],    by rw [← (underlyingMap f).target_app, z.2.2, hb]⟩noncomputable def Model.componentsMap {C : GlobularTheory.{v}} {X Y : C.Model} (f : X ⟶ Y) :    X.Components → Y.Components :=  Quot.map ((underlyingMap f).app 0) (by    rintro _ _ ⟨h, hs, ht⟩    exact ⟨(underlyingMap f).app _ h,      by rw [← (underlyingMap f).source_app, hs],      by rw [← (underlyingMap f).target_app, ht]⟩)noncomputable def Model.homotopyMap {C : GlobularTheory.{v}} {X Y : C.Model} (f : X ⟶ Y)    (hC : C.IsCoherator) (x : X.underlying.Cell 0) (n : ℕ) :    X.HomotopyGroup hC x n → Y.HomotopyGroup hC ((underlyingMap f).app 0 x) n :=  Quot.map (loopsMap f hC x n) (by    rintro _ _ ⟨h, hs, ht⟩    exact ⟨(underlyingMap f).app _ h,      by rw [← (underlyingMap f).source_app, hs]; rfl,      by rw [← (underlyingMap f).target_app, ht]; rfl⟩)def Model.WeakEquivalence {C : GlobularTheory.{v}} (hC : C.IsCoherator) {X Y : C.Model}    (f : X ⟶ Y) : Prop :=  Function.Bijective (componentsMap f) ∧    ∀ (x : X.underlying.Cell 0) (n : ℕ), Function.Bijective (homotopyMap f hC x n)end GlobularTheoryopen CategoryTheory CategoryTheory.Limitstheorem elementary_expansion (C : GlobularTheory.{v}) (hC : C.IsCoherator)    (X : C.Model) (hX : X.IsCellular) (n : ℕ)    (a : GlobularTheory.Model.disk C n ⟶ X)    (Y : C.Model) (i : X ⟶ Y)    (b : GlobularTheory.Model.disk C (n + 1) ⟶ Y)    (square : IsPushout a (GlobularTheory.Model.J C n) i b) :    GlobularTheory.Model.WeakEquivalence hC i := by  sorryend Grothendieckend OAI

Every extracted statement of the accompanying papers

The statements the atlas extracted automatically from each accompanying paper’s TeX source, with links to the full sources.

The Grothendieck homotopy hypothesis via elementary expansions

Theorem

Fix any Grothendieck coherator \mathcal C. Let X be a cellular \mathcal C-infinity-groupoid, let n\ge0, and let a:D_n\to X be any cell. In the pushout square

A diagram here is drawn in the paper: see it at the passage.

where s_n is the source inclusion, the map i:X\to X^+ is a weak equivalence.

Section 1, Introduction Read it in the paper TeX source, line 50

Show the TeX

Fix any Grothendieck coherator \(\mathcal C\).
Let \(X\) be a cellular \(\mathcal C\)-infinity-groupoid, let \(n\ge0\),
and let \(a:D_n\to X\) be any cell.  In the pushout square
\[
\begin{tikzpicture}[baseline=(current bounding box.center),
                   node distance=1.25cm and 2.2cm,>=Stealth]
\node (a) {\(D_n\)};
\node (b) [right=of a] {\(D_{n+1}\)};
\node (c) [below=of a] {\(X\)};
\node (d) at (b |- c) {\(X^+\)};
\draw[->] (a) -- node[above] {\(s_n\)} (b);
\draw[->] (a) -- node[left] {\(a\)} (c);
\draw[->] (b) -- (d);
\draw[->] (c) -- node[below] {\(i\)} (d);
\end{tikzpicture}
\]
where \(s_n\) is the source inclusion, the map \(i:X\to X^+\)
is a weak equivalence.

Configuration and file facts

File: lean/ComparatorChallenges/GrothendieckElementaryExpansion.lean
OpenAI’s Lean catalogue: OpenAI lists this as a main result in its Lean catalogue.
Solution module: OAI/CategoryTheory/Globular/ElementaryExpansion.lean
Allowed axioms: propext, Quot.sound, Classical.choiceThe axioms this configuration allows a proof to use. A replay shows which of them a proof uses.
Imports: Mathlib
Imports from outside Mathlib: None
Local vocabulary: 76 local vocabulary declarations
Lines of Lean, without comments or blank lines: 344
Second proof-verification program (nanoda): Off in OpenAI's configuration.

A shareable summary of this page: the proposed paper match, what the Lean statement expresses, and which reviews are recorded.

Plectis Atlas