Wikipedia · research solved · AMS 16
hardknown result, no worker yet
Jacobson Conjecture
Theorem · jacobson_conjecture_of_right_noetherian
Originally, on page 200 of [Ja1956], Jacobson asked if the Jacobson conjecture holds for all right Noetherian rings. However in [He1965] Herstein constructs a right Noetherian ring for which the Jacobson conjecture does not hold.
Formal statement · Lean 4.lean
theorem jacobson_conjecture_of_right_noetherian :
answer(False) ↔ ∀ (R : Type) [Ring R] [IsRightNoetherianRing R], JacobsonConjectureFor R := by
sorryProof. sorry
Nobody has tried yet.