Every dimension?
An AI preprint, with a Lean proof, claims Thomason model structures on strict n-categories in every dimension
Covers result 317 in OpenAI’s catalog: its one paper. See its connections to other results and the work it cites.
4:18. English captions available. The video loads from YouTube when you press play.
Chapters
The claim, in plain words
Every small category has a nerve, a space built from its chains of arrows. In 1980 Thomason showed that small categories, with weak equivalences measured on their nerves, form a model category with the same homotopy theory as spaces. Even posets are enough. Our computer takes the 14 faces of a tetrahedron’s surface, ordered by inclusion, and finds that the nerve of this poset is a 2-sphere. Turn every arrow into an isomorphism, though, and the same category collapses to a point.
That contrast matters. Episode 312 was about weak ∞-groupoids, where every arrow is invertible up to higher arrows, because strict groupoids cannot model all spaces. Strict categories, without inverses, measured through their nerves, can. Their higher versions, strict n-categories, have a nerve too, due to Street, built from shapes called orientals. Our computer lists the cells of the third oriental: 4 objects, 11 arrows counting composites, 8 two-cells and 1 three-cell.
In 2014 Ara and Maltsiniotis built the Thomason model structure for strict 2-categories, and reduced every higher dimension to two conditions, one of them about gluing. In 2015 they proved the other one, and conjectured the result for every dimension up to ∞. In 2018 Gagna, building on their work, showed that strict n-categories have the right homotopy category; the model structure itself stayed open, and in 2023 Ara wrote that their two-dimensional strategy had not yet been adapted, even for n = 3.
Result 317 is one OpenAI paper, 35 pages, dated September 25 and made public October 6, 2026. It claims the Ara–Maltsiniotis conjecture is true: for every n from 1 to ∞, small strict n-categories carry a proper, combinatorial model structure, with weak equivalences and fibrations detected by the twice-extended Street nerve, and Quillen equivalent to simplicial sets.
What is new, and what isn’t claimed
The cases n = 1 and 2 were known, and so was the homotopy category; the new part is the model structure in every higher dimension. Not claimed: anything about strict ∞-groupoids, weak higher categories, or other model structures on strict categories.
Where it stands
- Posted as a preprint
- OpenAI, 35 pages, dated September 25, 2026
- Peer reviewed
- Not yet
- Formalized in Lean
- The whole main theorem, every dimension (docs)
Last checked October 19, 2026. The paper is unrefereed and unchanged since release. Unusually, the whole main theorem, in every dimension, has a Lean proof: about 65,000 lines in 85 files, with no unproved steps and only Lean’s standard axioms, against a statement that, in our reading, says what the paper says. Two independent outside re-runs report that the checker accepts it; we did not build it ourselves. In the first 12 days we found no specialist assessment, only a citation on the nLab wiki, no reported error and no competing claim. OSVerify has not reviewed it.
How the proof goes
- Glue anything, change nothing. The missing step is Ara and Maltsiniotis’s gluing condition: attaching a piece built from a poset along a special kind of subposet, a sieve with a retraction, never changes the homotopy type of the nerve, whatever you attach it to. The paper builds explicit directed cylinders from a one-line chain formula, arranged to stay still on the old part, so that they survive any gluing. Our computer checks that formula on small posets: it holds in all 985 cases that meet its hypotheses, and fails in 769 of the rest, so the hypothesis is doing real work.
- Then Thomason’s argument. The new part is then contracted by induction, removing maximal elements, the local answers are glued with nerve covers, and the rest follows Thomason’s 1980 argument, with subdivided boundaries and horns. Our computer checks the poset facts that argument uses for every boundary and horn up to dimension 3, and all 13 pass.
The numbers in the video
- Ours: the 14 faces of a tetrahedron’s surface, ordered by inclusion, have a nerve that is a 2-sphere; inverting every arrow collapses the category to a point.
- Ours: the third oriental has 4 objects, 11 arrows counting composites, 8 two-cells and 1 three-cell.
- Ours: the paper’s chain formula holds in all 985 small cases that meet its hypotheses, and fails in 769 of 1,684 without them.
- Ours: the poset facts of Thomason’s argument hold for all 13 boundaries and horns up to dimension 3.
Read the source
- Thomason Model Structures in Every Strict Higher Dimension (PDF), 35 pages.
- The Lean formalization notes.
- The collection’s catalog, where this is result 317.
The paper
OpenAI groups related papers into one result; this one has a single paper.
Transcript
Read the full script
0:00The question
Every small category has a nerve, a space built from its chains of arrows. In 1980 Thomason showed that small categories, with weak equivalences measured on their nerves, form a model category with the same homotopy theory as spaces. Even posets are enough. Our computer takes the 14 faces of a tetrahedron’s surface, ordered by inclusion, and finds that the nerve of this poset is a 2-sphere. Turn every arrow into an isomorphism, though, and the same category collapses to a point. That contrast matters. Episode 312 was about weak ∞-groupoids, where every arrow is invertible up to higher arrows, because strict groupoids cannot model all spaces. Strict categories, without inverses, measured through their nerves, can. Their higher versions, strict n-categories, have a nerve too, due to Street, built from shapes called orientals. Our computer lists the cells of the third oriental: 4 objects, 11 arrows counting composites, 8 two-cells and 1 three-cell. In 2014 Ara and Maltsiniotis built the Thomason model structure for strict 2-categories, and reduced every higher dimension to two conditions, one of them about gluing. In 2015 they proved the other one, and conjectured the result for every dimension up to ∞. In 2018 Gagna, building on their work, showed that strict n-categories have the right homotopy category; the model structure itself stayed open, and in 2023 Ara wrote that their two-dimensional strategy had not yet been adapted, even for n = 3.
1:41The claim
Result 317 is one OpenAI paper, 35 pages, dated September 25 and made public October 6, 2026. It claims the Ara–Maltsiniotis conjecture is true: for every n from 1 to ∞, small strict n-categories carry a proper, combinatorial model structure, with weak equivalences and fibrations detected by the twice-extended Street nerve, and Quillen equivalent to simplicial sets. The cases n = 1 and 2 were known, and so was the homotopy category; the new part is the model structure in every higher dimension. Not claimed: anything about strict ∞-groupoids, weak higher categories, or other model structures on strict categories.
2:27How the proof goes
The missing step is Ara and Maltsiniotis’s gluing condition: attaching a piece built from a poset along a special kind of subposet, a sieve with a retraction, never changes the homotopy type of the nerve, whatever you attach it to. The paper builds explicit directed cylinders from a one-line chain formula, arranged to stay still on the old part, so that they survive any gluing. Our computer checks that formula on small posets: it holds in all 985 cases that meet its hypotheses, and fails in 769 of the rest, so the hypothesis is doing real work. The new part is then contracted by induction, removing maximal elements, the local answers are glued with nerve covers, and the rest follows Thomason’s 1980 argument, with subdivided boundaries and horns. Our computer checks the poset facts that argument uses for every boundary and horn up to dimension 3, and all 13 pass.
3:28Where it stands
The paper is unrefereed and unchanged since release. Unusually, the whole main theorem, in every dimension, has a Lean proof: about 65,000 lines in 85 files, with no unproved steps and only Lean’s standard axioms, against a statement that, in our reading, says what the paper says. Two independent outside re-runs report that the checker accepts it; we did not build it ourselves. In the first 12 days we found no specialist assessment, only a citation on the nLab wiki, no reported error and no competing claim. If it holds, strict higher categories, in every dimension up to ∞, carry a full model of the homotopy theory of spaces, just as Thomason found for ordinary categories.
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.