Source authenticated

Köthe Conjecture

GPT-6 Astra constructs a unital algebra $R=k\oplus A$ over the countable field $k=\overline{\mathbb F_2},$ with $I=A$ a nil two-sided ideal, together with a matrix $W\in M_2(I)$ that is not nilpotent. The algebra $A$ is generated by three weighted backward shifts. A diagonal construction chooses the weights so that every element of $A$ 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 $I$ . This formally disproves Krempa's matrix formulation of Köthe's conjecture.

Exact FrontierDelta

Prior state unknown→disproved

Scope and record

Occurred: Sep 3, 2026

Delta type: SOURCE CLAIM

Assumptions: VibeMathed verification: lean-verified. Publication: announcement. AI contribution: ai-discovered. VibeMathed editorial classifications, scores, notes, relations, and dataset structure are CC BY 4.0. Source statements and linked content retain their own rights.

Canonical aliases: Köthe Conjecture

Confidence: Not scored

Registry verification: lean verified · announcement · candidate

Open the source record ↗

Attribution

VibeMathed
registry · event recorded by

GPT-6 Astra (pre-release)
model · ai model contributor · OpenAI

Tom Adamczewski
human · human collaborator

Evidence vector

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review

Named evidence

VibeMathed record: Köthe Conjecture

specialist registry · passed

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.

Source ↗

Solution.lean and the Lean development

lean artifact · passed

lean-proof link supplied by the VibeMathed registry.

Source ↗

X Announcement

witness · pending

discussion link supplied by the VibeMathed registry.

Source ↗

Formal Conjectures source statement (Google DeepMind)

formal registration · pending

lean-statement link supplied by the VibeMathed registry.