Köthe's conjecture

DefinitionNil left ideal#✓fully proved

A left ideal \(I\) of a ring \(R\) is nil if each of its elements is nilpotent: for every \(x \in I\) there is a natural number \(n\) with \(x^n = 0\).

def IsNilLeftIdeal {R : Type*} [Ring R] (I : Ideal R) : Prop :=
  ∀ x : R, x ∈ I → IsNilpotent x

Used by 1

Used byKöthe's conjecture

DefinitionKöthe's conjecture#✓fully proved

The statement that for every ring \(R\) (associative, with identity) and all nil left ideals \(I\) and \(J\) of \(R\), the sum \(I + J\) is again a nil left ideal.

def conjecture : Prop :=
  ∀ (R : Type u) [Ring R] (I J : Ideal R),
    IsNilLeftIdeal I → IsNilLeftIdeal J → IsNilLeftIdeal (I + J)

Uses 1 · Used by 1

Statement usesNil left ideal

Used byKöthe's conjecture is false

TheoremKöthe's conjecture is false#●ready to prove

There exist a ring \(R\) (associative, with identity) and nil left ideals \(I\) and \(J\) of \(R\) (left ideals all of whose elements are nilpotent) such that the sum \(I + J\) is not nil.

Adamczewski, Böhmler and Marczinzik (arXiv:2609.07996, 2026; Lean 4 machine-checked by Adamczewski) build, over any countable field \(F\), a nil algebra \(N\) such that \(M_2(F1 + N)\) has two nil left ideals with non-nil sum. Greenfeld, King and Vendramin (arXiv:2609.15080) give an independent refutation.

public theorem_wanted conjecture_refuted : ¬ conjecture

Sources

Tom Adamczewski, Bernhard Böhmler and René Marczinzik, A counterexample to Köthe's conjecture and a question of Rowen, arXiv:2609.07996 (2026), https://arxiv.org/abs/2609.07996; Be'eri Greenfeld, G. King and Leandro Vendramin, The Köthe conjecture via point modules, arXiv:2609.15080 (2026), https://arxiv.org/abs/2609.15080.

Uses 1

Statement usesKöthe's conjecture

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.