The Ara-Maltsiniotis conjecture: Thomason model structures on strict n-categories for every n
Thomason (1980) put a model structure on small categories, transferred from simplicial sets along , that is Quillen equivalent to simplicial sets. For strict globular -categories, , with the Street nerve built from orientals, Ara and Maltsiniotis (2014) proved the case , reduced the general case to two conditions, and conjectured the general statement; Ara (2023) and Guetta-Maltsiniotis (2024) restate it. Is there, for every including , a model structure on small strict -categories whose weak equivalences and fibrations are those maps sent by to weak equivalences and Kan fibrations, and is a Quillen equivalence with simplicial sets?
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Homotopy theory; strict higher categories and model structures
- Posed by
- D. Ara and G. Maltsiniotis, Vers une structure de categorie de modeles a la Thomason sur la categorie des n-categories strictes, Adv. Math. 259 (2014)
- Year posed
- 2014
- Years open
- 12y
- Solved
- 2026-09-25
- Model
- Unreleased internal OpenAI model
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Collection
- OpenAI math release (October 2026), version adc7f12
- Significance
- 20 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Theorem 1.1: for every , the classes , and form a proper combinatorial model structure on small strict -categories, cofibrantly generated by the images of boundary and horn inclusions under , and is a Quillen equivalence with Kan-Quillen simplicial sets. The key step proves the Ara-Maltsiniotis pushout condition (Scholie 5.14 (d')). It concerns strict globular categories only, not weak higher categories or n-fold categories.
What the AI did
The release README says every result in openai/math was produced by an unreleased internal OpenAI model with a fixed procedure, on average about three hours of ChatGPT Pro thinking compute per result. This result is not one of the README's two exceptions (the Hodge conjecture for CM abelian varieties and the Re(s) > 11/12 zero-free region). The manuscript is authored 'OpenAI' and names no human author.
Verification
No independent mathematician has checked this yet. Checked here: Theorem 1.1 was read against the Ara-Maltsiniotis conjecture as recorded by Ara (2023) and Guetta-Maltsiniotis (2024). The Lean challenge lean/ComparatorChallenges/ThomasonModelStructures.json (declarations OAI.Thomason.main and OAI.Thomason.nerveDetection_allDimensions; solution module OAI/CategoryTheory/Thomason/RankedFaithfulness.lean present at the pinned commit) is not in the formalization catalogue. Its top-level statement was read here: for strict omega-categories and for each finite n at least 1 there is a model category whose weak equivalences and fibrations are created by Ex^2 of the Street nerve, with the induced cofibrations, generating sets from boundary and horn images, left and right properness, local presentability and a Quillen equivalence condition; a second statement identifies weak equivalences through the Street nerve. That is the headline. The challenge file is about 136 KB because it defines strict omega-categories and orientals itself; those definitions were not audited. Not rebuilt here.