Full Nullstellensatz for a system of polynomial equations

Proved

Nullstellensatz.strong_nullstellensatz_system

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

algebraic-geometrycommutative-algebra

Let $K$ be an algebraically closed field, let $f_1,\dots,f_m \in K[X_1,\dots,X_n]$ and let $f \in K[X_1,\dots,X_n]$ . Every solution $a \in K^n$ of the system $f_1 = \cdots = f_m = 0$ is also a solution of $f = 0$ if and only if there exist a natural number $r$ and polynomials $g_1,\dots,g_m$ such that

f^r = g_1 f_1 + \cdots + g_m f_m.

This refines the weak form, which is the case $f = 1$ .

Formalization Note. The target polynomial is called $p$ in Lean; $r = 0$ is allowed (then $f^0 = 1$ ).

Preamble

import Definitions.Def_Nullstellensatz_Defs
import Mathlib

open MvPolynomial

Formal statement

namespace Nullstellensatz

theorem strong_nullstellensatz_system {K : Type*} [Field K] [IsAlgClosed K] {n m : ℕ}
    (f : Fin m → MvPolynomial (Fin n) K) (p : MvPolynomial (Fin n) K) :
    (∀ a : Fin n → K, (∀ i, eval a (f i) = 0) → eval a p = 0) ↔
      ∃ r : ℕ, ∃ g : Fin m → MvPolynomial (Fin n) K, p ^ r = ∑ i, g i * f i := 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, introduction (lead section), last displayed identity f^r = g_1 f_1 + ... + g_m f_m.

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.

Let $K$ be an algebraically closed field, $n, m$ natural numbers, $f_1,\dots,f_m \in K[X_1,\dots,X_n]$ , and $p \in K[X_1,\dots,X_n]$ . The statement is the equivalence of:

for every $a \in K^n$ : if $f_i(a) = 0$ for all $i = 1,\dots,m$ , then $p(a) = 0$ ;
there exist a natural number $r \ge 0$ and polynomials $g_1,\dots,g_m$ with

p^r = \sum_{i=1}^m g_i f_i.

The exponent $r = 0$ is permitted, in which case the right side must equal $1$ . For $m = 0$ : condition 1 says $p$ vanishes on all of $K^n$ , condition 2 says $p^r = 0$ for some $r$ .

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