Algebra · Result 199

Counterexamples to Auslander–Reiten, Tachikawa and related homological conjectures

2 papersLean

Constructs finite-dimensional algebras over a characteristic-two rational-function field that disprove the Auslander–Reiten and Gorenstein-projective conjectures, and Tachikawa's second conjecture. An associated endomorphism algebra also disproves the classical, generalized and strong Nakayama conjectures, the Auslander–Gorenstein conjecture, and the Wakamatsu tilting conjecture. The counterexamples persist under every extension of the base field.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 2

An explicit counterexample to the Auslander-Reiten conjecture

OpenAI · September 23, 2026

We disprove the Auslander–Reiten conjecture for Artin algebras. We construct a finite-dimensional algebra Λ over \(k=\mathbb F_2(q,H_1,H_2)\) and a finite-dimensional nonprojective left module Z such that \(\mathop{\mathrm{Ext}}\nolimits ^i_\Lambda(Z,Z)=\mathop{\mathrm{Ext}}\nolimits ^i_\Lambda(Z,\Lambda)=0\) for every i > 0. The module is Gorenstein-projective, so the same example also disproves the Gorenstein-projective conjecture. Both counterexamples persist after every extension of k.

Read PDF Download Source

Cite

@misc{OAI:An-explicit-counterexample-to-the-Auslander-Reiten-conjecture-September-23-2026,
  author = {{OpenAI}},
  title = {{An explicit counterexample to the Auslander--Reiten conjecture}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/An-explicit-counterexample-to-the-Auslander-Reiten-conjecture-September-23-2026/paper.pdf}{OAI:An-explicit-counterexample-to-the-Auslander-Reiten-conjecture-September-23-2026}},
  year = {2026}
}

A counterexample to Tachikawa's second conjecture

OpenAI · September 23, 2026

We disprove Tachikawa's second conjecture by constructing a finite-dimensional symmetric algebra over \(k=\mathbb F_2(q,H_1,H_2)\) with a finite-dimensional nonprojective module whose self-extension groups vanish in every positive degree. The associated endomorphism algebra also gives counterexamples to the classical, generalized, and strong Nakayama conjectures, the Auslander–Gorenstein conjecture, and the Wakamatsu tilting conjecture. These conclusions persist after every extension of k.

Read PDF Download Source

Cite

@misc{OAI:A-counterexample-to-Tachikawas-second-conjecture-September-23-2026,
  author = {{OpenAI}},
  title = {{A counterexample to Tachikawa's second conjecture}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-counterexample-to-Tachikawas-second-conjecture-September-23-2026/paper.pdf}{OAI:A-counterexample-to-Tachikawas-second-conjecture-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 Auslander–Reiten conjecture predicts that a finitely generated module \(M\) over an Artin algebra \(A\) is projective if \(\mathrm{Ext}^i_A(M,M\oplus A)=0\) for every \(i>0\). The formalized counterexample is a finite-dimensional algebra over \(k=\mathbb F_2(q,H_1,H_2)\) and a finite-dimensional nonprojective Gorenstein-projective module with this vanishing.

It also establishes \(A/\mathrm{rad}\,A\cong k^8\), \((\mathrm{rad}\,A)^4\ne0\), and preservation of the listed properties after every field extension. The Tachikawa companion is separate.

Tachikawa's second conjecture predicts that a finite-dimensional module over a finite-dimensional self-injective algebra is projective if all its positive-degree self-Ext groups vanish. The formalized counterexample gives a finite-dimensional symmetric algebra over \(\mathbb F_2(q,H_1,H_2)\) and a finite-dimensional nonprojective module \(M\) with \(\mathrm{Ext}^i(M,M)=0\) for every \(i>0\). Symmetric algebras are self-injective, so this contradicts the conjecture.

The later field-extension, endomorphism-algebra, and related homological consequences are not included.

Comparator links

Result	Comparator statement
Auslander–Reiten counterexample	AuslanderReiten.lean
Tachikawa counterexample	Tachikawa.lean

Scope note on GitHub →