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 'A counterexample to Tachikawa's second conjecture'. 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.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 199). The Lean development was not rebuilt locally.