Category Theory

Motivation

Newtonian gravitation can be written in two ways. In Newtonian gravitation (NG), spacetime has a flat derivative operator $\nabla$ and a scalar potential $\varphi$ obeying Poisson's equation, and bodies are pushed off the straight lines of $\nabla$ by the force $-\nabla^a\varphi$. In geometrized Newtonian gravitation (GNG), also called Newton–Cartan theory, the potential is absorbed into a curved derivative operator $\tilde\nabla$ whose geodesics are the trajectories of freely falling bodies. This is the same geometrization that general relativity performs. Trautman (1965) proved that the two pictures pass into each other.

Weatherall (2016) asks whether NG and GNG are the same theory. He represents each theory by a category of models and calls two theories equivalent when there is an equivalence of categories that preserves empirical content. The answer depends on the arrows chosen for NG:

• NG₁ treats the potential as physical. Its arrows are diffeomorphisms preserving $t_a$, $h^{ab}$, $\nabla$ and $\varphi$, and NG₁ is not equivalent to GNG.
• NG₂ treats the potential as a gauge quantity, as Newton's Corollary VI suggests. Its arrows are pairs $(f,\psi)$ with $\nabla^a\nabla^b\psi = 0$, and NG₂ is equivalent to GNG (Prop. 6.1).

This is the gravitational twin of the electromagnetic question "potentials vs. field strengths" treated in the companion missions on Weatherall's Understanding Gauge. The other side of the Newton–Cartan story, the classical limit of general relativity, is described under Significance.

Setting

Following Weatherall (p. 3), spacetime is $\mathbb R^4$, here in one global chart E = Fin 4 → ℝ with index 0 for time. The classical metrics are $t_a = dx^0$ (tt) and $h^{ab} = \mathrm{diag}(0,1,1,1)$ (hh). Their $t = \text{const}$ slices are complete copies of $\mathbb R^3$, as Weatherall requires.

A derivative operator is a smooth field of Christoffel symbols Γ x a b c $=\Gamma^a{}_{bc}(x)$, symmetric in $b,c$, acting by

$$\nabla_b\xi^a = \partial_b\xi^a + \Gamma^a{}_{bn}\xi^n .$$

It is compatible when $\nabla_a t_b = 0$ and $\nabla_a h^{bc} = 0$. Curvature uses Malament's sign convention:

$$\xi^bR^a{}_{bcd} = -2\nabla_{[c}\nabla_{d]}\xi^a, \qquad R_{bc} = R^n{}_{bcn}.$$

Other notation:

• Geometrization: $\tilde\nabla = (\nabla, -t_bt_c\nabla^a\varphi)$, that is $\tilde\Gamma^a{}_{bc} = \Gamma^a{}_{bc} + t_bt_c\,h^{an}\partial_n\varphi$ (geomΓ).
• Gauge transformation: $(\nabla, t_bt_c\nabla^a\psi)$ (gaugeΓ).
• Curves: a massive body has unit timelike tangent, $t_a\xi^a = 1$. Curves are smooth on an open interval.

The objects of the categories are:

• NG (IsNG Γ φ): compatible, flat $\nabla$ and a smooth potential $\varphi$. The mass density is $\rho = \nabla^a\nabla_a\varphi/4\pi$.
• GNG (IsGNG Γ): compatible $\tilde\nabla$ satisfying, for some smooth $\rho$,

$$(1)\ R_{ab} = 4\pi\rho\,t_at_b,\qquad (2)\ R^a{}_b{}^c{}_d = R^c{}_d{}^a{}_b,\qquad (3)\ R^{ab}{}_{cd} = 0 .$$

The arrows are diffeomorphisms $f$ of $\mathbb R^4$ that preserve $t_a$ and $h^{ab}$ and carry one derivative operator to the other through the transformation law

$$\partial_b\partial_c f^a + \Gamma'^a{}_{de}(f(x))\,\partial_bf^d\,\partial_cf^e = \partial_nf^a\,\Gamma^n{}_{bc}(x)$$

(IsGNGArrow). NG₁ arrows also preserve $\varphi$ (IsNG1Arrow). NG₂ arrows are pairs $(f,\psi)$ with $\nabla^a\nabla^b\psi = 0$, where $f$ carries the gauge-transformed pair $\big((\nabla,t_bt_c\nabla^a\psi),\ \varphi+\psi\big)$ to $(\nabla',\varphi')$ (IsNG2Arrow).

Formalization targets

Goal: NG₂ ≃ GNG (ng2_equiv_gng, Weatherall Prop. 6.1)

Geometrization $E(\nabla,\varphi) = \tilde\nabla$, $E(f,\psi) = f$ has these properties:

1. It sends NG₂ objects to GNG objects with the same allowed trajectories, and NG₂ arrows to GNG arrows.
2. It is full and faithful: every GNG arrow $f : E(A)\to E(A')$ is $E(f,\psi)$ for a unique $\psi$.
3. It is essentially surjective: every GNG object is isomorphic to a geometrization.

This is exactly the "full, faithful, essentially surjective" route of Weatherall's proof in App. A. These three properties together are equivalent to an equivalence of categories.

Milestones (source order)

1. geometrization, Prop. 2.1 (Trautman). For flat compatible $\nabla$ and Poisson's equation, $\tilde\nabla$ has these properties:
   • it is a classical spacetime;
   • its timelike geodesics are exactly the curves with $\xi^n\nabla_n\xi^a = -\nabla^a\varphi$;
   • it is the unique derivative operator with that property;
   • it satisfies (1)–(3).
2. recovery, Prop. 2.2 (Trautman). Every classical spacetime satisfying (1)–(3) comes from some flat $\nabla$ and potential $\varphi$ obeying Poisson's equation.
3. gauge_iff, the non-uniqueness remark after Prop. 2.2. A second pair $(\varphi',\nabla')$ works iff $\nabla^a\nabla^b(\varphi'-\varphi)=0$ and $\nabla' = (\nabla, t_bt_c\nabla^a(\varphi'-\varphi))$. Weatherall states the "if" direction and his proof of Prop. 6.1 uses the "only if" direction. The iff is Malament's Prop. 4.2.5. Note that $\psi = g(x^0)\,x^1$ is allowed: the gauge includes time-dependent uniform accelerations (Corollary VI).
4. geom_naturality, the key computation in App. A. A metric-preserving diffeomorphism carrying $\varphi$ to $\varphi'$ carries $\nabla$ to $\nabla'$ iff it carries $\tilde\nabla$ to $\tilde\nabla'$.
5. ng1_not_equiv_gng, the NG₁ row of Table 1 (§6, p. 18). No object map NG₁ → GNG preserves empirical content while inducing bijections of hom-sets. Weatherall states this in prose without a proof. The intended argument is that two NG₁ models related by a nonzero gauge share a geometrization but have no NG₁ arrow between them.

Significance

• Philosophy of physics. This is the standard worked example for categorical criteria of theoretical equivalence: Glymour's criterion versus equivalence of categories. It also shows how "excess structure" (here the potential) is detected by fullness.
• Physics. Newton–Cartan geometry is the non-relativistic limit of general relativity. Fletcher, Manchak, Schneider and Weatherall (2018), Thm 8 restates Malament's (1986) theorem in Künzle's (1976) framework. If a family $g_{ab}(\lambda)$ of Lorentzian metrics has $g_{ab}\to t_at_b$ and $\lambda g^{ab}\to -h^{ab}$, and its Einstein tensors converge, then the limit derivative operator satisfies (1) and (2), but not necessarily (3). GR limits therefore land in a slightly larger class than GNG, and condition (3) is exactly what the recovery theorem needs. This makes the present mission the Newtonian half of a planned GR-limit mission.
• Lean. This is a reusable coordinate model of Galilean/Newton–Cartan structures, Christoffel transformation laws and curvature, none of which exist in Mathlib.

Difficulty

• Milestones 1, 3 and 4 are long but elementary tensor computations. The uniqueness clause in 1 needs local existence of solutions of the trajectory ODE (Mathlib's Picard–Lindelöf).
• Milestone 2 is the heart. Compatibility forces $\tilde\Gamma$ to be a rotation field $\omega_{ij}$ plus an acceleration field $g_i$. Condition (3) forces $\omega$ to be spatially constant, and condition (2) makes $g$, minus the inertial terms of a rotating frame, a closed form on each slice. The Poincaré lemma, smoothly in the time parameter, then produces $\varphi$. The degree-1 Poincaré lemma on convex sets is in Mathlib, and the companion mission Weatherall 2016: Potentials vs. Field Strengths (continuum) develops the homotopy operator.
• The goal then assembles 2, 3 and 4.

Formalization scope

• Single global chart. Weatherall's spacetime is $\mathbb R^4$ with arbitrary $t_a, h^{ab}$. Here $t_a$ and $h^{ab}$ are fixed to their standard form in one global chart, a choice of Galilean coordinates; the derivative operators remain arbitrary. Arrows are genuine diffeomorphisms of $\mathbb R^4$.
• Normalized curves. Massive bodies have unit tangent $t_a\xi^a = 1$, as in Malament (Ch. 4). Without this normalization the geodesic and force laws are not equivalent.
• No category instances. Categories are encoded by their hom-predicates, and "equivalence of categories" by the full / faithful / essentially-surjective data of App. A. Composition laws are not required by any item.
• Out of scope: Weatherall's footnote 32 (spatially compact matter), Glymour's criterion, and the GR limit (planned as a separate mission).

Selected references

• J. O. Weatherall, Are Newtonian Gravitation and Geometrized Newtonian Gravitation Theoretically Equivalent?, Erkenntnis 81 (2016) 1073–1091. Primary source: Props. 2.1, 2.2, 6.1, Table 1, App. A.
• D. B. Malament, Topics in the Foundations of General Relativity and Newtonian Gravitation Theory, University of Chicago Press (2012), Ch. 4 (Props. 4.2.1, 4.2.5). Conventions.
• D. B. Malament, Classical General Relativity, in Handbook of the Philosophy of Physics (2007).
• A. Trautman, Foundations and current problems of general relativity, in Brandeis Summer Institute 1964, Prentice-Hall (1965).
• S. C. Fletcher, J. B. Manchak, M. D. Schneider, J. O. Weatherall, Would Two Dimensions be World Enough for Spacetime?, Stud. Hist. Philos. Mod. Phys. 63 (2018) 100–113. Thm 8 is the Newtonian limit.
• H. P. Künzle, Covariant Newtonian limit of Lorentz space-times, Gen. Rel. Grav. 7 (1976) 445–457.

Motivation

Mirror symmetry was discovered in string theory as a duality between families of Calabi–Yau manifolds, and it entered mathematics as a prediction: the generating function counting rational curves on one manifold equals a period integral of a mirror manifold. In his 1994 ICM address, Homological algebra of mirror symmetry (alg-geom/9411018), M. Kontsevich proposed that these numerical coincidences are shadows of an equivalence of categories: the symplectic geometry of $V$ should be encoded by Fukaya's $A_\infty$-category $F(V)$, whose objects are Lagrangian submanifolds and whose products count pseudo-holomorphic discs, and the complex geometry of the mirror $W$ by the derived category $D^b(\mathrm{Coh}\,W)$ of coherent sheaves. His Homological Mirror Conjecture asserts that the derived category built from $F(V)$ embeds as a full triangulated subcategory of $D^b(\mathrm{Coh}\,W)$.

Kontsevich states the conjecture "in slightly vague form", because Fukaya's construction was not, and still is not, available in the generality the statement needs. He therefore closes the paper with the one instance he can compute by hand, in the section Two-dimensional tori: a return: for the flat torus $\Sigma = \mathbb{R}^2/\mathbb{Z}^2$, the objects are closed geodesics with unitary local systems, the products $m_2$ are sums over triangles in the universal cover weighted by $\exp(-\text{area})$, and their structure constants are values of the classical theta-function. He predicts an equivalence with $D^b(\mathrm{Coh}\,E)$ for an elliptic curve $E$. This instance was proved by A. Polishchuk and E. Zaslow, Categorical mirror symmetry: the elliptic curve (math/9801119). Later instances include the four-torus (Abouzaid–Smith, arXiv:0903.3065) and Calabi–Yau hypersurfaces (Sheridan, arXiv:1111.0632). None of this has been formalized.

Setting

Fix a real number $\mathrm{area} > 0$, and let $\Sigma$ be the torus $\mathbb{R}^2/\mathbb{Z}^2$ carrying the translation-invariant symplectic form of total area $\mathrm{area}$; a region of Euclidean area $a$ in coordinates has symplectic area $\mathrm{area}\cdot a$.

A brane $b$ consists of: a primitive vector $v \in \mathbb{Z}^2$ and a point $c \in \mathbb{R}^2$, which together determine the closed geodesic $L_b = \{\,c + tv \bmod \mathbb{Z}^2\,\}$; a grading $\alpha \in \mathbb{R}$, a real lift of the direction angle normalized so that $(\cos \pi\alpha, \sin \pi\alpha)$ is parallel to $v$; and a real constant $\theta$ describing a flat unitary line bundle on $L_b$, whose parallel transport along a path of parameter length $s$ is $\exp(2\pi i\,\theta s)$. Two branes are transverse when $\det(v_1, v_2) \neq 0$; their geodesics then meet in the finite set $L_{b_1} \cap L_{b_2}$, which indexes a basis of the Floer space $\mathrm{Hom}(b_1, b_2)$. All of this space sits in a single degree, the Maslov index

$$\mu(b_1, b_2) \;=\; \lceil \alpha_2 - \alpha_1 \rceil .$$

For three pairwise transverse branes and intersection points $p \in L_1 \cap L_2$, $q \in L_2 \cap L_3$, $r \in L_1 \cap L_3$, a triangle is a triple of lifts $(P, Q, R) \in (\mathbb{R}^2)^3$ of $(p,q,r)$ with $Q - P$ parallel to $v_2$, $R - Q$ parallel to $v_3$, $P - R$ parallel to $v_1$, and positively oriented. Kontsevich's structure constant is

$$c(p,q,r) \;=\; \sum_{\text{triangles}} \exp\bigl(-\text{symplectic area}\bigr)\cdot \bigl(\text{holonomies along the three sides}\bigr),$$

the coefficient of $r$ in $m_2(p, q)$. On the complex side, $D^b_{\mathrm{coh}}(E)$ denotes the complexes of $\mathcal{O}_E$-modules with bounded, coherent cohomology.

Formalization targets

Goal — homological mirror symmetry for the two-torus

For every $\mathrm{area} > 0$ there exist a smooth proper curve $E$ over $\mathbb{C}$, an assignment $b \mapsto \Phi(b)$ of an object of $D^b_{\mathrm{coh}}(E)$ to each brane, and isomorphisms

$$\mathbb{C}^{\,L_{b_1} \cap L_{b_2}} \;\xrightarrow{\ \sim\ }\; \mathrm{Hom}\bigl(\Phi(b_1),\, \Phi(b_2)[\mu(b_1,b_2)]\bigr) \qquad (b_1 \pitchfork b_2),$$

with $\mathrm{Hom}(\Phi(b_1), \Phi(b_2)[d]) = 0$ for $d \neq \mu(b_1,b_2)$, carrying the products $c(p,q,r)$ to composition in $D^b_{\mathrm{coh}}(E)$ whenever $\mu(b_1,b_2) + \mu(b_2,b_3) = \mu(b_1,b_3)$.

Milestones

Existence of the Fukaya $A_\infty$-category of the torus; finiteness of $L_{b_1} \cap L_{b_2}$ with $|\det(v_1,v_2)|$ points; the Maslov relation $\mu(b_1,b_2) + \mu(b_2,b_1) = 1$; $m_1^2 = 0$ together with associativity of $m_2$ up to coboundary; the degeneration of an $A_\infty$-category with $m_{\geq 3} = 0$ to a differential graded category; the theta-function shape of the structure constants; and their associativity equation.

Significance

The conjecture reorganizes mirror symmetry: the numerical predictions compare two elements of an uncountable set of power series, whereas the homological statement compares two objects in a countable set of triangulated categories, and the numerical statements are meant to follow from it. The torus case is the smallest instance in which every ingredient — Lagrangian branes, Maslov grading, disc counts, theta functions, and coherent sheaves on an elliptic curve — is present and computable, so it is the natural first target.

What this mission adds beyond the literature is machine-checked mathematics where none exists. Mathlib currently has no symplectic manifolds, no Lagrangian Floer theory, no Fukaya categories, and no $A_\infty$-categories; it does have schemes, sheaves of modules, and derived categories of abelian categories. The mission supplies the missing $A_\infty$ layer and the torus model, and asks for the comparison theorem. The $A_\infty$ definitions, the derived category with coherent cohomology, and the theta-function estimates are reusable outside this mission.

Difficulty

The obvious route — "transport the Polishchuk–Zaslow proof" — stalls at the point where the two sides are compared. Establishing that the triangle sums converge and equal theta-function values is analysis that Mathlib supports; producing an elliptic curve as a scheme with prescribed parameter, computing $\mathrm{Ext}$-groups between the mirror sheaves, and matching all products simultaneously is not currently supported by any library. A second difficulty is bookkeeping: gradings, Maslov indices and shifts must line up, since the product of two morphisms is nonzero only when $\mu(b_1,b_2)+\mu(b_2,b_3) = \mu(b_1,b_3)$, and the same numerical condition controls which triples of branes bound triangles at all.

Formalization scope

Conventions committed to in Lean. An $A_\infty$-category is encoded as a single graded module $A$ with morphism components $\hom(X,Y)$ and products given by a map on lists, $m[f_1,\dots,f_n] = m_n(f_1 \otimes \cdots \otimes f_n)$ of degree $2-n$, with $m_0 = 0$, and Stasheff signs $(-1)^{r+st}$ in the bar-construction normalization; $m_2(f,g)$ is "$f$ then $g$". Triangles are normalized by requiring the first vertex to lie in $[0,1)^2$, which picks exactly one representative in each $\mathbb{Z}^2$-orbit; only positively oriented triangles are counted; sums are tsums, so convergence is part of the work. The hom-space isomorphisms in the goal are required to be additive, not a priori $\mathbb{C}$-linear, because the derived category of $\mathcal{O}_E$-modules is not equipped with a $\mathbb{C}$-linear structure in Mathlib; the required compatibility with the structure constants pins down the algebra anyway. The goal asks only for the existence of a smooth proper curve $E$ over $\mathbb{C}$; the paper's further prediction that $E$ has parameter $\exp(-\mathrm{area})$ is deliberately left out of the statement.

The goal is not trivially satisfiable: the intersection set of two transverse branes is nonempty, so the required isomorphisms force the corresponding $\mathrm{Hom}$-groups to be nonzero of the right size, in the right degree, with the prescribed products.

The general conjecture, for an arbitrary symplectic manifold with $c_1 = 0$, is not stated here, and deliberately so: without symplectic manifolds and Floer theory in Mathlib, any general statement would have to take the Fukaya category as an unconstrained parameter, which would make it either vacuous or false. Building that infrastructure — symplectic manifolds, graded Lagrangian branes, Floer cohomology, twisted complexes over an $A_\infty$-category and their triangulated structure — is the natural way to extend this mission, and such contributions are welcome.

Selected references

• M. Kontsevich, Homological algebra of mirror symmetry, Proceedings of the International Congress of Mathematicians (Zürich, 1994), alg-geom/9411018.
• A. Polishchuk and E. Zaslow, Categorical mirror symmetry: the elliptic curve, Adv. Theor. Math. Phys. 2 (1998), math/9801119.
• M. Abouzaid and I. Smith, Homological mirror symmetry for the 4-torus, Duke Math. J. 152 (2010), arXiv:0903.3065.
• N. Sheridan, Homological mirror symmetry for Calabi–Yau hypersurfaces in projective space, Invent. Math. 199 (2015), arXiv:1111.0632.

Motivation

A model structure on a category specifies weak equivalences, fibrations and cofibrations so that the category carries a homotopy theory. Thomason showed that the category $\mathbf{Cat}$ of small categories carries a model structure Quillen equivalent to simplicial sets, so that ordinary categories model all homotopy types of spaces (Thomason 1980). Its weak equivalences are the functors whose nerves are weak homotopy equivalences.

Strict higher categories have a nerve too: Street's orientals $\mathcal O_m$ give the Street nerve $N_n$ of a strict $n$-category (Street 1987). The higher-dimensional Thomason model-structure conjecture of Ara and Maltsiniotis asks for the analogue of Thomason's theorem for strict globular $n$-categories for every $1\le n\le\infty$ (Ara–Maltsiniotis 2014; Ara 2023, §§9.2.5–9.2.6; Guetta–Maltsiniotis 2024). Strict higher categories are already known to describe the homotopy category of spaces after localization (Gagna, below); the conjecture asks for the full model structure, with lifting and factorization on all strict $n$-categories.

This mission asks for a machine-checked proof of Theorem 1.1 of an OpenAI preprint dated September 25, 2026 (source), which claims the conjecture in every dimension. The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Timeline

• 1980 — Thomason constructs the model structure on $\mathbf{Cat}$ by transfer along $c\,\mathrm{Sd}^2\dashv\mathrm{Ex}^2N$, introducing Dwyer maps (Cahiers 1980).
• 1987 — Street defines orientals and the nerve of strict $\omega$-categories (JPAA 1987).
• 1999 — Cisinski corrects the retract argument in Thomason's properness proof (Cahiers 1999).
• 2007/2016 — Worytkiewicz, Hess, Parent and Tonks propose the 2-dimensional structure (JPAA 2007), with a later corrigendum (JPAA 2016).
• 2010 — Fiore and Paoli construct a Thomason structure on $n$-fold categories (AGT 2010).
• 2014 — Ara and Maltsiniotis develop the transfer theorem, settle dimension 2, and isolate sufficient conditions for all $n$ (Adv. Math. 2014).
• 2018 — Gagna shows that strict $n$-categories model homotopy types after localizing at nerve weak equivalences (Adv. Math. 2018).
• 2023–2024 — Ara's habilitation records the remaining pushout condition and the conjecture; Guetta and Maltsiniotis state the $\omega$-dimensional conjecture.
• 2026 — The OpenAI preprint claims the conjecture for every $1\le n\le\infty$ (Theorem 1.1, p. 2).

Setting

A strict globular $\omega$-category has a set of cells, source and target operations $s_k,t_k$ in each dimension, and associative, unital compositions $\ast_k$ along $k$-dimensional boundaries satisfying the interchange law; every cell has finite dimension. A strict $n$-category is one whose cells above dimension $n$ are identities; $n\mathbf{Cat}$ denotes the category of small strict $n$-categories and strict functors ($n=\infty$ means $\omega\mathbf{Cat}$). No invertibility is assumed.

The Street nerve $N_n:n\mathbf{Cat}\to\mathbf{sSet}$ has $(N_nX)_m=\mathrm{Hom}(\mathcal O_m,X)$, with left adjoint $c_n$. With barycentric subdivision $\mathrm{Sd}\dashv\mathrm{Ex}$ set

$$L_n=c_n\mathrm{Sd}^2,\qquad R_n=\mathrm{Ex}^2N_n .$$

Let $W_{KQ}$ and $\mathrm{Fib}_{KQ}$ be the weak homotopy equivalences and Kan fibrations, $I=\{\partial\Delta[m]\hookrightarrow\Delta[m]\}_{m\ge0}$ and $J=\{\Lambda^k[m]\hookrightarrow\Delta[m]\}_{m\ge1}$. Define

$$W_n=R_n^{-1}(W_{KQ}),\qquad F_n=R_n^{-1}(\mathrm{Fib}_{KQ}),\qquad C_n={}^{\perp}(F_n\cap W_n).$$

Formalization targets

Milestone: Equation (7.1), p. 24 — nerve detection

$W_n=N_n^{-1}(W_{KQ})=R_n^{-1}(W_{KQ})$: a functor of strict $n$-categories is a weak equivalence exactly when its Street nerve is a weak homotopy equivalence. This follows from $\mathrm{id}\to\mathrm{Ex}$ being a natural weak equivalence.

Goal: Theorem 1.1 (p. 2)

For every $n\in\{1,2,3,\dots\}\cup\{\infty\}$, $(C_n,W_n,F_n)$ is a proper combinatorial model structure on $n\mathbf{Cat}$, cofibrantly generated by $(L_nI,L_nJ)$, and

$$L_n:\mathbf{sSet}_{KQ}\rightleftarrows(n\mathbf{Cat},C_n,W_n,F_n):R_n$$

is a Quillen equivalence.

Significance

The result itself. The theorem says that strict higher categories, in every dimension, model the homotopy theory of spaces through a genuine model structure, not only after localization. It provides functorial factorizations and lifting on arbitrary strict $n$-categories, including those that are not freely generated, which is what the small-object argument needs. The key new input is a couniversality theorem: pushouts of $c_nN(A)\to c_nN(E)$ along sieves with a right adjoint retraction are Street weak equivalences (Theorem 5.2, p. 18), which is the remaining sufficient condition of Ara–Maltsiniotis.

Formalizing it. Mathlib has simplicial sets and model-category foundations but no strict $\omega$-categories, orientals or Street nerve. A complete development adds these, Steiner's directed complexes, Gray cylinders and local presentability of $n\mathbf{Cat}$, all reusable in higher category theory.

Difficulty

The transfer theorem reduces the model structure to a pushout condition, and that is the hard part: categorical pushouts of strict $n$-categories can create many new composites, so the nerve of a pushout is not the pushout of nerves. Thomason controlled this in dimension 1 with Dwyer maps, but that method does not extend directly. The preprint builds explicit stationary directed prisms (Lemma 3.1, p. 10) that are constant on the old part, so contractions glue across any attachment, and then reduces general posets to finite ones via sieve covers (Corollary 4.5, p. 16; Lemma 4.6, p. 17). Properness (Proposition 7.3, p. 26) and the unit comparison after two subdivisions (Proposition 7.4, p. 27) are separate arguments.

Formalization scope

• OmegaCategory is a structure with a type of cells, source/target maps indexed by ℕ, partial compositions, the globular, unit, associativity and interchange laws, and finite dimension of each cell. Finite $n$ uses a full subcategory NCategory n.
• FullMain asserts: the Kan–Quillen model structure on SSet exists with the standard classes; and, for $\omega$ and every finite $n\ge1$, an ExactModelEndpoint for $L_n\dashv R_n$: a ModelCategory whose weak equivalences, fibrations and cofibrations are exactly $W_n,F_n,C_n$; $(L_nI)^{\pitchfork}=F_n\cap W_n$ and $(L_nJ)^{\pitchfork}=F_n$; both weak factorization systems; completeness, cocompleteness and local presentability; left and right properness; $L_n$ left Quillen; and the Quillen-equivalence criterion at fibrant targets.
• The classes are fixed by equations, so the goal cannot be met by an unrelated model structure.
• The milestone quantifies over every n : ℕ, including $n=0$, which the source does not consider; the identity holds there by the same argument.

Selected references

• OpenAI, Thomason Model Structures in Every Strict Higher Dimension, OpenAI Math Release preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Thomason-Model-Structures-in-Every-Strict-Higher-Dimension-September-25-2026/paper.pdf
• R. W. Thomason, Cat as a closed model category, Cahiers Topologie Géom. Différentielle 21 (1980). https://www.numdam.org/item/CTGDC_1980__21_3_305_0/
• R. Street, The algebra of oriented simplexes, J. Pure Appl. Algebra (1987). https://doi.org/10.1016/0022-4049(87)90137-X
• D.-C. Cisinski, La classe des morphismes de Dwyer n'est pas stable par rétractes, Cahiers (1999). https://www.numdam.org/item/CTGDC_1999__40_3_227_0/
• D. Ara, G. Maltsiniotis, Vers une structure de catégorie de modèles à la Thomason sur la catégorie des n-catégories strictes, Adv. Math. (2014). https://doi.org/10.1016/j.aim.2014.03.013
• A. Gagna, Strict n-categories and augmented directed complexes model homotopy types, Adv. Math. (2018). https://doi.org/10.1016/j.aim.2018.04.010
• D. Ara, Théorie de l'homotopie des ∞-catégories strictes, habilitation (2023). https://www.normalesup.org/~ara/files/hdr.pdf
• L. Guetta, G. Maltsiniotis, Homologie polygraphique des systèmes locaux, Adv. Math. (2024). https://doi.org/10.1016/j.aim.2024.109719
• T. M. Fiore, S. Paoli, A Thomason model structure on the category of small n-fold categories, Algebr. Geom. Topol. 10 (2010). https://doi.org/10.2140/agt.2010.10.1933
• P. G. Goerss, J. F. Jardine, Simplicial Homotopy Theory, Birkhäuser (1999). https://doi.org/10.1007/978-3-0348-8707-6

Motivation

Every module over a ring has a projective resolution, and its length, the projective dimension, measures how far the module is from being projective. Over a finite-dimensional algebra, some modules have infinite projective dimension; the finitistic dimension conjectures ask whether, among the modules whose projective dimension is finite, these finite values are bounded. The questions were publicized by Bass in 1960 and became central problems in the representation theory of finite-dimensional algebras, tied to many other homological conjectures (Nakayama, Gorenstein symmetry, Auslander–Reiten), each of which would follow from finiteness of the finitistic dimension.

Timeline

• 1960. Bass publicizes the finitistic-dimension questions (doi:10.1090/S0002-9947-1960-0157984-8).
• 1991. Green, Kirkman and Kuzmanovich prove little finitistic finiteness for finite-dimensional monomial algebras (doi:10.1016/0021-8693(91)90062-D); Green and Huisgen-Zimmermann treat Artin algebras with radical cube zero.
• 1992. Huisgen-Zimmermann constructs monomial algebras whose little and big finitistic dimensions differ ($n$ versus $n+1$), so the two invariants are not equal in general (doi:10.1007/BF02100610).
• 1995. Huisgen-Zimmermann's survey "a tale of 3.5 decades" describes the state of the problems (doi:10.1007/978-94-011-0443-2_41).
• 2005. Igusa and Todorov introduce syzygy invariants and prove finiteness for Artin algebras of representation dimension at most three.
• 2019. Rickard shows that if injective modules generate the unbounded derived category, then the big finitistic dimension is finite (doi:10.1016/j.aim.2019.106735).
• 2024. Cummings proves that universal little finitistic finiteness is equivalent to its left–right symmetry (doi:10.1112/blms.12954).

The source of this mission is an OpenAI preprint dated September 23, 2026, which constructs a counterexample to the little finitistic-dimension conjecture over $\mathbb C$. A companion OpenAI preprint independently gives a characteristic-two example.

Setting

Let $A$ be a finite-dimensional unital algebra over $\mathbb C$. For a left $A$-module $N$, $\operatorname{pd}_AN\in\{0,1,2,\dots\}\cup\{\infty\}$ is the minimal length of a projective resolution. The little finitistic dimension is

$$\operatorname{findim}A=\sup\{\operatorname{pd}_AN:\ N\ \text{finitely generated left } A\text{-module},\ \operatorname{pd}_AN<\infty\},$$

and the big finitistic dimension $\operatorname{Findim}A$ is the same supremum over all left modules. Over a finite-dimensional algebra, finitely generated and finite-dimensional modules coincide. The little finitistic-dimension conjecture asserts $\operatorname{findim}A<\infty$ for every such $A$.

Injective left modules generate if the smallest triangulated subcategory of the unbounded derived category of left modules that contains them and is closed under arbitrary coproducts is the whole category.

Formalization targets

Goal: Theorem 1.1

$$\exists\ A\ \text{finite-dimensional over } \mathbb C:\quad \forall m\ge1\ \exists N_m\ \text{finitely generated with}\ 2m-2\le\operatorname{pd}_AN_m<\infty;\ \text{hence}\ \operatorname{findim}A=\infty.$$

The Lean statement OAI.LittleFinitistic.Main.exists_counterexample is open on the platform.

Milestone: Corollary 1.2

$$\exists\ \Lambda:\ \operatorname{findim}\Lambda=\operatorname{Findim}\Lambda=\infty,\quad \operatorname{findim}\Lambda^{\rm op}=\operatorname{Findim}\Lambda^{\rm op}=0,$$

injective left $\Lambda$-modules do not generate, and injective right $\Lambda$-modules do.

Significance

Theorem 1.1 refutes the little finitistic-dimension conjecture: a single finite-dimensional algebra has finitely generated modules with terminating projective resolutions of unbounded length. Since $\operatorname{findim}\le\operatorname{Findim}$, it also refutes the big version for Artin algebras, and by Rickard's theorem gives an algebra for which injectives do not generate the derived category. Corollary 1.2 shows that finiteness can fail on one side and hold on the other in the most extreme way, in contrast with Cummings' equivalence of universal finiteness and left–right symmetry.

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. Because many homological conjectures were known to follow from the finitistic-dimension conjecture, an independent check of a counterexample is of direct interest.

Difficulty

Positive results cover large classes (monomial, radical cube zero, representation dimension at most three), so a counterexample must escape all of them. The finitistic dimension of one fixed algebra must be unbounded, which requires encoding an unbounded family of terminating processes into fixed finite data. The paper realizes a "selection process" from an infinite finitely presented group algebra by a single bounded bimodule complex over a finite-dimensional algebra; making this realization uniform in the input module, and turning it into ordinary projective resolutions over a trivial extension, are the main obstacles.

Formalization scope

• Algebras are A : Type with [Ring A] [Algebra ℂ A] and FiniteDimensional ℂ A; modules are objects of ModuleCat.{0} A, finiteness is Module.Finite A N.
• projectiveDimension is Mathlib's CategoryTheory.projectiveDimension, valued in WithBot ℕ∞, equal to ⊤ for infinite dimension; littleFinitisticDimension and bigFinitisticDimension are suprema over modules of finite projective dimension.
• Right modules are left modules over Aᵐᵒᵖ.
• InjectivesGenerate uses HasDerivedCategory.standard and quantifies over isomorphism-closed triangulated properties closed under coproducts indexed by Type u and containing all injectives in degree 0.

A complete development needs derived tensor products of bimodule complexes, trivial extension algebras $D\ltimes X$ and their bar resolutions, finite presentations of group algebras and their finite-dimensional representations, and (for the milestone) Rickard's theorem and Cummings' triangular algebra. Contributions formalizing Proposition 2.1 (selection), Theorem 4.1 (tensor realization) and Proposition 6.1 (bar splitting) are welcome.

Selected references

• OpenAI, An algebra of infinite little finitistic dimension, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/An-algebra-of-infinite-little-finitistic-dimension-September-23-2026/paper.pdf
• H. Bass, Finitistic dimension and a homological generalization of semi-primary rings, Trans. Amer. Math. Soc., 1960. https://doi.org/10.1090/S0002-9947-1960-0157984-8
• B. Zimmermann Huisgen, Homological domino effects and the first Finitistic Dimension Conjecture, Invent. Math., 1992. https://doi.org/10.1007/BF02100610
• B. Zimmermann Huisgen, The finitistic dimension conjectures — a tale of 3.5 decades, in Abelian Groups and Modules, 1995. https://doi.org/10.1007/978-94-011-0443-2_41
• E. L. Green, E. E. Kirkman, J. Kuzmanovich, Finitistic dimensions of finite dimensional monomial algebras, J. Algebra, 1991. https://doi.org/10.1016/0021-8693(91)90062-D
• K. Igusa, G. Todorov, On the finitistic global dimension conjecture for Artin algebras, in Representations of Algebras and Related Topics, 2005.
• J. Rickard, Unbounded derived categories and the finitistic dimension conjecture, Adv. Math., 2019. https://doi.org/10.1016/j.aim.2019.106735
• C. Cummings, Left–right symmetry of finite finitistic dimension, Bull. London Math. Soc., 2024. https://doi.org/10.1112/blms.12954