Thomason model structures on strict higher categories
Thomason model structures on strict higher categories are the subject of a conjecture of Ara and Maltsiniotis: for every n ≥ 1 and for n = ω, the category of small strict globular n-categories should carry a model structure transferred from simplicial sets along Thomason's twice-subdivided adjunction with the Street nerve, and Quillen equivalent to simplicial sets. A manuscript in OpenAI's public mathematics collection (github.com/openai/math), dated 25 September 2026, claims the conjecture in every dimension. The collection includes a Lean formalization of the theorem. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
Background
- As recounted in the introduction of the manuscript:
- Thomason established the case n = 1 by transferring the model structure of simplicial sets to small categories along the twice-subdivided nerve adjunction, introducing Dwyer maps to compare pushouts of nerves with nerves of pushouts; Cisinski corrected the retract argument used for properness. Street's orientals extend the nerve to strict higher categories.
- Ara and Maltsiniotis developed an abstract transfer theorem, established the proper combinatorial model structure in dimension two, and obtained the Quillen equivalence using Chiche's comparison theorem; Worytkiewicz, Hess, Parent and Tonks had proposed the two-dimensional structure earlier, with a later corrigendum. For general n the transfer framework reduces the question to two sufficient conditions.
- Ara and Maltsiniotis proved the first condition, a unit comparison on nerves of posets, in all dimensions, and Gagna gave a direct simplicial proof and showed that the Street nerve induces an equivalence with homotopy types after localization. Ara's 2023 account records the remaining pushout condition and the general conjecture, and Guetta and Maltsiniotis state the ω-dimensional conjecture explicitly. Fiore and Paoli constructed a Thomason model structure on n-fold categories, a different setting.
The original result
- Claim. Theorem 1.1 of Thomason Model Structures in Every Strict Higher Dimension states that, for every n in {1, 2, 3, …} ∪ {∞}, the classes whose weak equivalences are detected by the Street nerve and whose fibrations are detected by its twice-extended nerve form a proper combinatorial model structure on small strict globular n-categories, cofibrantly generated by the images of the simplicial boundary and horn inclusions under the twice-subdivided categorification, and that this adjunction is a Quillen equivalence with simplicial sets in the Kan–Quillen model structure.
- Method, as described: the principal intermediate result states that a pushout of the categorified nerve of a downward-closed subposet, whose inclusion has a right adjoint retraction, is a Street weak equivalence; this is the pushout condition isolated by Ara and Maltsiniotis. Its proof constructs strict Gray cylinders from explicit directed prisms on Steiner's chain complexes that stay constant on the old part, so that they glue across any attachment, and handles general posets by covering arguments; Thomason's Dwyer-map geometry then gives the comparison for the subdivided boundary and horn attachments.
- Source. The manuscript Thomason Model Structures in Every Strict Higher Dimension at commit
1581d4c. - Formalization, as described by the repository. The scope note states that the formalization proves the higher-dimensional Thomason model-structure theorem for small strict globular n-categories in every positive finite dimension and in dimension ω, with the stated proper combinatorial model structure Quillen equivalent to simplicial sets through the twice-subdivided categorification and twice-extended Street nerve, and that the selected statements also identify the weak equivalences by the Street nerve in all these dimensions. The Comparator statement is
ThomasonModelStructures.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 20 October 2026) |
|---|---|---|---|---|
| 2026-10-07 | nLab, Thomason model structure (revision of 7 October 2026; content mirror) | Reading (encyclopedia entry) | The entry lists the OpenAI manuscript, with links to the paper and the Lean scope note, as a Lean-formalized proof of Thomason model structures for small strict globular n-categories in every positive dimension n and for n = ω. | Wiki entry. |
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026) |
Review (fidelity of the formal statements) | Rates this family "full": the Lean statement gives, for strict ω-categories and for every n ≥ 1, the model structure with the stated classes, generators, properness and Quillen-equivalence criterion, and identifies the weak equivalences by Street-nerve detection in every dimension. It notes that strict ω- and n-categories are defined by hand, with no Mathlib counterpart. It records a sandboxed Comparator pass for ThomasonModelStructures. |
MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-10 | cert-machine, openai/math lane K, run 38051470892 | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept the ThomasonModelStructures solution (897 s). The project reports two-kernel certification of 398 of 416 challenges of the collection. |
Repository. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (time-outs, memory, errors) does not list ThomasonModelStructures, so the challenge was accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-16 | J. Jardine, Lattice24, referee review in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995) | Review (AI-assisted audit) | Reports no gap and states that the reviewer read sections 1 to 7 in full and skimmed the presentability appendix without auditing it. Its one minor note is that the prism construction needs the naturality of the Steiner–Gray comparison for every morphism of strong Steiner complexes, including degeneracies, which the manuscript takes from Ara and Maltsiniotis rather than proving; the reviewer calls this input standard. | Part of an audit of the collection's manuscripts that the audit describes as complete. The reviews are published under CC BY 4.0. |
Notes
- The earlier results are due to the authors named in the Background section, as recounted by the manuscript.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.