Disproof of the Köthe conjecture in Krempa's matrix form

Köthe's conjecture (1930) asks whether the sum of two nil left ideals of a ring is always nil, equivalently whether every ring has a largest nil left ideal. Krempa (1972) showed it equivalent to several other statements, among them that for every ring R and nil two-sided ideal I the matrix ideal M_n(I) is nil in M_n(R) (already for n = 2).

This file states that matrix form exactly as Google DeepMind's Formal Conjectures does and proves its negation from KoetheCounterexample.counterexample. The definitions Koethe.IsNil and Koethe.KotheRadical and the bracketed conjecture inside Koethe.KotherConjecture.variants.general_matrix.disproof are copied verbatim from FormalConjectures/Wikipedia/Koethe.lean in Formal Conjectures at commit 9cbe1d3c12998c786b7c2cd99ce28a21b6631f66 (Copyright 2025 The Formal Conjectures Authors, Apache-2.0), where KotherConjecture.variants.general_matrix is registered as a research-open statement.

Since M_n(I) is the sum of its n column left ideals, each of which is nil when I is, Köthe's original statement implies the matrix form; the counterexample therefore also refutes the conjecture as originally stated. That implication is a standard argument and is not part of this formal development.

def Koethe.IsNil {R : Type u_1} [Ring R] {S : Type u_2} [SetLike S R] (I : S) : Prop

Say a subset I of a ring R is nilpotent if all its elements are nilpotent.

Equations

• Koethe.IsNil I = ∀ i ∈ I, IsNilpotent i

def Koethe.KotheRadical (R : Type u_1) [Ring R] : TwoSidedIdeal R

The Kothe Radical of a ring R is the sum of all (two-sided) nil ideals of R. Tags: Kothe Radical, upper nilradical

Equations

• Koethe.KotheRadical R = sSup {I : TwoSidedIdeal R | Koethe.IsNil I}

theorem Koethe.KotherConjecture.variants.general_matrix.disproof : ¬∀ {R : Type u_2} [inst : Ring R] {I : TwoSidedIdeal R}, IsNil I → ∀ (n : Type u_3) [inst_1 : Fintype n], IsNil (TwoSidedIdeal.matrix n I)

Disproof of the Köthe conjecture in Krempa's matrix form (the KotherConjecture.variants.general_matrix statement of Formal Conjectures): it is not the case that for every ring R, every nil two-sided ideal I and every finite index type n, the matrix ideal M_n(I) is nil.