# Counterexamples to Auslander–Reiten, Tachikawa and related homological conjectures

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

- [An explicit counterexample to the Auslander-Reiten conjecture](../../preprints/An-explicit-counterexample-to-the-Auslander-Reiten-conjecture-September-23-2026/paper.pdf)
- [A counterexample to Tachikawa's second conjecture](../../preprints/A-counterexample-to-Tachikawas-second-conjecture-September-23-2026/paper.pdf)

## 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](../ComparatorChallenges/AuslanderReiten.lean) |
| Tachikawa counterexample | [Tachikawa.lean](../ComparatorChallenges/Tachikawa.lean) |