∑math20

Algebra · Result 198

A counterexample to finitistic-dimension finiteness

1 paperLean

Constructs a finite-dimensional complex algebra whose finite-dimensional modules have unbounded finite projective dimensions. This disproves the little finitistic-dimension conjecture.

Watch

1

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation
2

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation
▶The proposed solutionin preparation

Papers 1

First page of An algebra of infinite little finitistic dimension

An algebra of infinite little finitistic dimension

OpenAI · September 23, 2026

We construct a finite-dimensional complex algebra whose finite-dimensional modules have unbounded finite projective dimensions. This disproves the little finitistic-dimension conjecture.

Read PDF Download Source

Cite
@misc{OAI:An-algebra-of-infinite-little-finitistic-dimension-September-23-2026,
  author = {{OpenAI}},
  title = {{An algebra of infinite little finitistic dimension}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/An-algebra-of-infinite-little-finitistic-dimension-September-23-2026/paper.pdf}{OAI:An-algebra-of-infinite-little-finitistic-dimension-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The little finitistic-dimension conjecture predicts that finitely generated modules of finite projective dimension over a fixed finite-dimensional algebra have bounded projective dimensions. The formalized counterexample is a finite-dimensional complex algebra with a finitely generated module of projective dimension at least \(2m-2\) and still finite for every \(m\ge1\).

A separate formalized result gives a finite-dimensional complex algebra whose little and big finitistic dimensions are infinite on the left and zero on the right. Injectives fail to generate its unbounded derived category on the left and generate it on the right.

Comparator links

ResultComparator statement
Infinite little finitistic dimensionLittleFinitistic.lean
Left/right finitistic-dimension asymmetryFinitisticAsymmetry.lean

Scope note on GitHub →