VibeMathedMath problems solved with AI
Sign in

Köthe Conjecture

Köthe's conjecture asks whether the sum of two nil left ideals of a ring is always nil. Equivalently, by Krempa's 1972 formulation, if II is a nil two-sided ideal of a ring RR, then the matrix ideal Mn(I)M_n(I) should be nil for every finite nn, already for n=2n=2.

The conjecture is false: there exists a ring RR, a nil two-sided ideal I⊆RI\subseteq R, and a 2×22\times 2 matrix with entries in II that is not nilpotent.

Result
Disproved(see note)
Status
Candidate (review pending)
AI contribution
AI-discovered
Method
Construction
Field
Noncommutative ring theory
Posed by
Gottfried Köthe
Year posed
1930
Years open
96y
Solved
2026-09-03
Model
GPT-6 Astra (pre-release)
Vendor
OpenAI
Collaborators
Tom Adamczewski
Verification
Lean-verified
Publication
Announced
Significance
60 / 100
Disclosed cost
$432
Wikipedia
No dedicated article

What was actually shown

GPT-6 Astra constructs a unital algebra R=k⊕AR=k\oplus A over the countable fieldk=F2‾, k=\overline{\mathbb F_2}, with I=AI=A a nil two-sided ideal, together with a matrixW∈M2(I) W\in M_2(I) that is not nilpotent.

The algebra AA is generated by three weighted backward shifts. A diagonal construction chooses the weights so that every element of AA is nilpotent. At the same time, a suitable polynomial combination of the shifts fixes a nonzero vector; this yields a companion-type matrix with a nonzero eigenvalue, and hence a nonnilpotent matrix whose entries lie in II.

This formally disproves Krempa's matrix formulation of Köthe's conjecture.

What the AI did

A pre-release GPT-6 Astra autonomously attempted the open Formal Conjectures benchmark statement, with no human steering during the run, and constructed both the mathematical counterexample and its Lean proof. It builds a nil algebra from three weighted backward shifts over F2‾\overline{\mathbb F_2}, arranges a universal mortality property for all elements, and simultaneously constructs a 2×22\times2 matrix over the resulting nil ideal that has a nonzero eigenvalue and hence is not nilpotent. Claude was later used to generate repository documentation from the completed proof; it was not the mathematical solver.

Verification

Lean-verified on this site's ladder: kernel-checked, and the statement was written independently of the prover. Checked here on 5 September 2026 from a clone at b052755: 3,331 lines of Lean, zero `sorry` outside the Challenge.lean stub, zero `axiom` declarations, no `native_decide`, `unsafe` or `implemented_by` (two uses of `decide` on small numerals), mathlib pinned, Comparator in CI with the three standard axioms. The compared statement is byte-identical to Formal Conjectures' `KotherConjecture.variants.general_matrix` at 9cbe1d3c, and its one nontrivial ingredient, mathlib's `TwoSidedIdeal.matrix`, is the ideal of matrices whose every entry lies in I, so the statement is Krempa's matrix form as intended. What the kernel has certified is therefore: a ring with a nil ideal I and a non-nilpotent matrix in M_2(I). That Köthe's original statement implies the matrix form is an elementary argument (M_n(I) is a sum of n nil column left ideals) stated in the repository and not formalized; Formal Conjectures opened a PR on 4 September relating the formulations. Candidate because no ring theorist has read it yet, and the machine-generated proof account is unaudited.

Sources

Submitted by VibeGene on

Changelog2 changes

Discussion