Prove2Me

(X2+1)(X^2+1) has no common zero in R\mathbb R

Proved
Nullstellensatz.real_counterexample

by Lucas · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometrycommutative-algebra

The ideal (X2+1)(X^2 + 1) of R[X]\mathbb R[X] is proper, and its elements have no common zero in R\mathbb R:

(X2+1)≠R[X],¬ ∃ x∈R  ∀f∈(X2+1), f(x)=0.(X^2+1) \ne \mathbb R[X], \qquad \neg\,\exists\, x \in \mathbb R\ \ \forall f \in (X^2+1),\ f(x) = 0.

This shows that the algebraic closedness of KK cannot be dropped from the weak Nullstellensatz.

Preamble
import Definitions.Def_Nullstellensatz_Defs
import Mathlib

open MvPolynomial
Formal statement
namespace Nullstellensatz

theorem real_counterexample :
    Ideal.span {(Polynomial.X ^ 2 + 1 : Polynomial ℝ)} ≠ ⊤ ∧
      ¬ ∃ x : ℝ, ∀ f ∈ Ideal.span {(Polynomial.X ^ 2 + 1 : Polynomial ℝ)}, f.eval x = 0 := by
  sorry

end Nullstellensatz
Source
Wikipedia, article "Hilbert's Nullstellensatz" (snapshot supplied as Hilbert's_Nullstellensatz.pdf, printed 2026-09-27), https://en.wikipedia.org/wiki/Hilbert%27s_Nullstellensatz, section "Formulations", paragraph 3, last sentence (the ideal (X^2+1) in R[X]).
Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted the Lean statement, with full knowledge of the source article and of the intended meaning. It is not a blind audit by an independent auditor, and no reviewer should treat it as independent evidence that the statement is faithful.

A statement with no parameters, about the univariate polynomial ring R[X]\mathbb R[X] and the principal ideal (X2+1)(X^2+1) generated by X2+1X^2 + 1. It asserts both:

  1. (X2+1)(X^2+1) is not the whole ring R[X]\mathbb R[X];
  2. there is no real number xx such that every polynomial ff in (X2+1)(X^2+1) satisfies f(x)=0f(x) = 0.
Human review

  • Endorsed by Shuze Chen · Sep 28, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Sep 28, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph