qedbot

Wikipedia·wikipedia:Koethe

Köthe conjecture

conjecture formal record: mixed F2 declared

No independent check recorded yet. A formal artifact, declaration or published object is attached, but no rebuild of it is recorded here.

Fidelity F2: The correspondence is declared through an alignment table and written divergences.

Source

AI activity

How grades work

No AI contribution recorded against this statement.

Fidelity

How fidelity is graded

F2 declared. The correspondence is declared through an alignment table and written divergences.

declares divergences from its source

Declared by the projects

1

As each project's formalization.yaml states it.

Köthe conjecture: disproof (Krempa's matrix form)tadamcz/koethe · joined by anchor · no independent check

Read formalization.yaml

method
autonomous — GPT-6 Astra (pre-release version, OpenAI)
review
other — mechanically verified (comparator: lean kernel replay, standard axioms only) in the harness and again in this repository's ci; no human mathematical review yet (none)
sorry
0 unproved goals declared
sources
Köthe conjecture: disproof (Krempa's matrix form) — other; Köthe conjecture (Wikipedia) — background; Die Struktur der Ringe, deren Restklassenring nach dem Radikal vollständig reduzibel ist — background; Logical connections between some open problems concerning nil rings — background
related
google-deepmind/formal-conjectures/blob/9cbe1d3c12998c786b7c2cd99ce28a21b6631f66/FormalConjectures/Wikipedia/Koethe.lean — builds-on; epoch-research/LeanOpenProblems/blob/0ef96d7b12cfa96a93761b4bba1c635f4546c5ca/apn/data/wikipedia/Isolated/Koethe.KotherConjecture.variants.general_matrix.lean — builds-on
divergences
The compared theorem is exactly the negation of the Formal Conjectures statement `general_matrix`, restated explicitly: for all `R : Type u_1` with `[Ring R]`, all two-sided ideals `I` with `IsNil I` (every element nilpotent), and all finite index types `n : Type u_2`, `IsNil (TwoSidedIdeal.matrix n I)`. `TwoSidedIdeal.matrix n I` is Mathlib's entrywise matrix ideal `M_n(I)` and requires a `DecidableEq n` instance, supplied classically (`open scoped Classical in`) exactly as in the Formal Conjectures file. The definition `Koethe.IsNil` is copied verbatim from that file. The statement is universe-polymorphic in `R` and `n`; the witness is built in every universe (`AlgebraicClosure (ULift (ZMod 2))`, index type `ULift (Fin 2)`). The relation to Köthe's original formulation (sums of nil left ideals) is a standard argument stated in the README but not formalized.
checked by
nobody independent of its authors yet

Follow and discuss

All discussion

Discussion and bounties for this problem load here.

Something wrong or missing here? Request a correction or add a claim, with its sources.

Formal material

Formal statements · 1
Cited proofs · 0

No proof artifact cited by the formal record.

Also known as · 2
  • https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Wikipedia/Koethe.lean
  • FormalConjectures/Wikipedia/Koethe.lean

Cite this record

qed.bot, “Köthe conjecture”, https://qed.bot/s/wikipedia-koethe, as of 30 Sep 2026.

This record as plain text, with each claim, its grades and its sources.