Lean disproof of Krempa's matrix form of the Koethe conjecture
A machine-checked Lean proof refutes the matrix formulation that Krempa showed equivalent to the Koethe conjecture, found by a pre-release model with no human steering of the proof search.
- Model
- GPT-6 Astra (pre-release)
- Field
- Mathematics
- Date
- 2026-09-03
- Human collaborators
- Tom Adamczewski
- Problem posed
- 1930 · open 96 yrs
Sources
Original work
Independent commentary
What was found
Koethe asked in 1930 whether every ring has a largest nil left ideal. Krempa showed in 1972 that this is equivalent to several other statements, among them a statement about matrix ideals, and it is that matrix form which is disproved here. The proof was produced in Epoch AI's LeanOpenProblems harness, in an evaluation run over the 222 research-open statements of the Wikipedia collection of Google DeepMind's Formal Conjectures, at a pinned benchmark commit. The benchmark file states the conjecture and its negation, both with sorry, and the model fills in exactly one. The construction builds a nil algebra from three weighted backward shifts over the algebraic closure of the two-element field. The compared theorem depends on no sorry and on no axioms beyond propext, Quot.sound and Classical.choice.
Novelty check
The Koethe conjecture has stood since 1930 and is stated as open in Google DeepMind's Formal Conjectures at the commit the harness pinned, which is what the model was given. Krempa's 1972 equivalences are the standard literature on the problem and are cited in the repository. No prior disproof of the matrix form, and no prior resolution of the conjecture in any of its equivalent forms, was found in the four registries or the surrounding literature. What is new is the counterexample and its Lean proof, not the equivalence, which is classical.
Caveats and known objections
The machine-checked statement is Krempa's matrix form, not Koethe's original question, and the step from one to the other is a 1972 equivalence in the literature rather than part of what was checked. Anyone citing this as a disproof of the Koethe conjecture is relying on that equivalence, and an algebraist should confirm it holds in the form used. The repository is prepared for submission to Palomar but no registration had landed at entry, and no expert in ring theory is on record as having read the construction. The verification grade rests on the mechanical check of the matrix-form statement, which vibemathed independently cloned and confirmed at 3,331 lines with no sorry outside the statement stub and no axiom declarations. Autonomy is graded autonomous on the repository's explicit record that the run was one attempt per statement with 'no human saw or steered the proof search', the only human input being the pre-existing benchmark statement; the repository also discloses that the whole repository was machine-written by AI assistants at Adamczewski's direction.
Also recorded at
Nothing mechanically. It is a parallel listing of the same result, carrying its own verification label rather than an independent check.
Nobody outside the lab has checked this yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Formally verified and Autonomous.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded formally verified for verification and autonomous for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Lean disproof of Krempa's matrix form of the Koethe conjecture. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-09-03-koethe-conjecture-matrix-formBibTeX
@misc{whataifound-openai-2026-form,
title = {Lean disproof of Krempa's matrix form of the Koethe conjecture},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by OpenAI / Epoch AI. Verification: Formally verified. Autonomy: Autonomous.},
url = {https://whataifound.org/finding/2026-09-03-koethe-conjecture-matrix-form}
}