Disproof of the Köthe conjecture (Krempa's matrix form)

Source: arxiv:2609.07996, url:https://github.com/tadamcz/koethe Authors: Tom Adamczewski Status: verified Main declarations: Koethe.KotherConjecture.variants.general_matrix.disproof Tags: ring-theory, nil-ideals, koethe-conjecture, counterexample, matrix-rings MSC: 16N40, 16S50

Mathematical overview

Köthe's conjecture (1930) asks whether the sum of two nil left ideals of a ring is nil. Krempa (1972) showed that it is equivalent to the statement that M_n(I) is a nil ideal of M_n(R) for every ring R and every nil two-sided ideal I, already for n = 2. This development refutes that matrix form: Koethe.KotherConjecture.variants.general_matrix.disproof is exactly the negation of the research-open statement KotherConjecture.variants.general_matrix of Google DeepMind's Formal Conjectures (copied verbatim, see LeanPool.Koethe.Disproof), and KoetheCounterexample.counterexample exhibits, in every universe, a ring with a nil two-sided ideal I and a non-nilpotent matrix in M_2(I).

The witness ring is the unitization of the non-unital algebra A generated by three weighted backward shifts (aᵢ u)(n) = vₙ(i) u(n + 1) on the sequence space over K = k(t), where k = \overline{𝔽₂} and vₙ ∈ k³ are nonzero weights; the nil ideal is A itself. The operator a₀ + t a₁ + t² a₂ fixes an explicit nonzero vector, which yields a companion matrix H ∈ M₂(R) with a nonzero eigenvalue, so H² ∈ M₂(A) is not nilpotent (LeanPool.Koethe.ShiftWitness). The bulk of the development shows that the weights can be chosen so that A is nil:

• LeanPool.Koethe.Linearization: every element of A is linearized into a one-row matrix pencil whose nilpotence implies nilpotence of the element (KoetheCounterexample.nil_of_all_pencils_nil);
• LeanPool.Koethe.MultiProjective: a multiprojective common-zero theorem, namely that at most 2N polynomials multihomogeneous of a common positive degree in N blocks of three variables have a common zero with no zero block, proved with the Segre cone, the Nullstellensatz and Krull's height theorem (KoetheMultiProjective.exists_common_zero);
• LeanPool.Koethe.Mortality: mask mortality, namely that a periodic mask with more than half of its residues free admits a compatible word of nonzero letters killing any given pencil, by determinantal rank reduction (KoetheCounterexample.maskMortality);
• LeanPool.Koethe.MaskSequence: a diagonal construction over the countably many pencils gives a universal mortal sequence (KoetheCounterexample.exists_universalMortalSequence).

The implication from Köthe's original formulation to the matrix form (each column ideal of M_n(I) is a nil left ideal) is standard and is not part of the formal development.

Provenance

Imported from https://github.com/tadamcz/koethe at commit a94a72aec957cb28d76aa30fb97a01d440990d7f (Apache-2.0). The Lean proof was written autonomously by a pre-release version of GPT-6 Astra (OpenAI) in Epoch AI's LeanOpenProblems evaluation harness, starting from the Formal Conjectures statement, and was packaged by Tom Adamczewski; an informal write-up is arXiv:2609.07996 (Adamczewski, Böhmler, Marczinzik). The port splits the single upstream file into modules along its original part boundaries, replaces the broad import Mathlib by minimal imports, removes the per-part set_option autoImplicit false lines, renames the pencil field constant to scalar, and repairs the Mathlib API drift from v4.28.0 to the pool's toolchain. No statement was weakened; three auxiliary lemmas were generalized from Fintype to Finite index types.