Lean formalization in OpenAI math repository (Result 199)
Model / AI: OpenAI (unreleased)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'An explicit counterexample to the Auslander-Reiten conjecture'. 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.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 199). The Lean development was not rebuilt locally.