Category Theory

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

The homotopy hypothesis relates algebraic higher groupoids to spaces. Elementary expansions provide a concrete test of whether adjoining a higher cell preserves homotopy information. The pinned manuscript supplies the research context.

Setting

C is a globular coherator in the encoded convention, X is a cellular model, and Y is a pushout that attaches an (n+1)-disk along the source-face inclusion of an n-disk.

Formalization target

The selected goal is OAI.Grothendieck.elementary_expansion. Its central assertion is

$$X\longrightarrow X\amalg_{D_n}D_{n+1}\quad\text{is a weak equivalence}.$$

The theorem states that, for a coherator C (a globular theory, meaning a category of shapes built from globes by iterated gluing, with morphisms preserving the globular pushouts, which has a cellular presentation as a countable-stage colimit of free extensions along admissible pairs of parallel cells and in which every admissible pair is filled by some morphism), the following holds for models of C, i.e. presheaves on C sending globular pushouts to pullbacks. Let X be a cellular model, meaning that it is built from an initial model by a well-ordered transfinite composition in which each successor step attaches cells freely along boundaries of cells of the previous stage. Let n be a natural number, let a be a map from the free model disk(n) on the n-globe to X, and let J_n : disk(n) → disk(n+1) be the map induced by the source-face inclusion of the n-globe into the (n+1)-globe. If Y, together with i : X → Y and b : disk(n+1) → Y, forms a pushout square of a and J_n, then i is a weak equivalence. Here weak equivalence means that i induces a bijection on sets of components (0-cells modulo being joined by a 1-cell) and, for every 0-cell x of X and every n, a bijection on homotopy groups, which are classes of n-loops based at the degenerate cells above x, identified when joined by an (n+1)-cell.

Significance and status

The selected goal is the elementary-expansion theorem. It does not itself assert the complete equivalence between the homotopy theory of spaces and all coherator models. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

The conclusion requires preservation of components and every based homotopy group, for cellular models built through transfinite attachments.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.

Selected references

• OpenAI, The Grothendieck homotopy hypothesis via elementary expansions, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

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