What was already known
Tachikawa’s second conjecture predicted every finite-dimensional self-orthogonal module over a finite-dimensional self-injective algebra is projective. Earlier skew-field or partial-vanishing examples did not settle this field-algebra statement.
AI involvement
OpenAI credits an internal model with the symmetric-algebra manuscript and Lean proof. Its companion Auslander–Reiten construction supplies an input.
The manuscript is credited to OpenAI and the release attributes production of its results and proof artifacts to an internal model; individual autonomy is not shown.
- Supporting source (github.com) — How the results were produced; versions and verification scope
- Supporting source (github.com) — Tachikawa Comparator entry
Importance
The claimed symmetric-algebra witness refutes the longstanding second Tachikawa conjecture.
Limitations
The cited Lean theorem covers the symmetric-algebra witness and self-Ext vanishing. Consequences for Nakayama and other homological conjectures require separate attribution and review.
Technical verification
The cited Lean file's main theorem constructs a finite symmetric algebra and nonprojective finite module over the specified characteristic-two function field with all positive self-Ext groups zero. The catalogue names this declaration as the Tachikawa Comparator target. This is a source-reported machine proof, not a replay in this review.
Formal checking
Lean proof of OAI.Tachikawa.main_theorem against the Tachikawa Comparator statement
- Checker
- Lean 4 kernel, as reported by the OpenAI math release
- Scope
- Existence of the finite-dimensional symmetric algebra and nonprojective self-orthogonal module over F_2(q,H_1,H_2)
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
No named human explanation of the central complete-resolution and symmetric-transfer construction is documented. Few is the evidence default, not a finding that mathematicians cannot understand it.
Correction and publication history
The claimed symmetric-algebra witness refutes the longstanding second Tachikawa conjecture.
Read this published revision