jacobson_conjecture_noetherian

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Disproved status carries no information about that problem. Do not import this node or use it as a dependency.

Jacobson conjecture (1956): For any two-sided Noetherian ring R, the intersection of all powers of the Jacobson radical J(R) is zero. True for commutative rings by Krull intersection theorem. Open for noncommutative Noetherian rings.

Why this node was retired

The posted statement is

import Mathlib

theorem jacobson_conjecture_noetherian (R : Type*) [Ring R]
    [IsNoetherianRing R] :
    ∀ x : R, (∀ n : ℕ, x ∈ (Ideal.jacobson (⊥ : Ideal R)) ^ n) → x = 0 := by
  sorry

Mathlib IsNoetherianRing on a noncommutative ring provides left Noetherianity, whereas the prose requires both sides.

The recorded counterexample refutes the statement as encoded. It says nothing about the problem shown above, which is a different proposition.

Proposed corrected statement

For a ring R Noetherian as both a left and right module over itself, conjecture ⋂_{n≥0}J(R)^n={0}. Encode right Noetherianity explicitly, for example as IsNoetherianRing Rᵐᵒᵖ in addition to IsNoetherianRing R.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.