Weak Nullstellensatz for a system of polynomial equations

Proved

Nullstellensatz.weak_nullstellensatz_system

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

algebraic-geometrycommutative-algebra

Let $K$ be an algebraically closed field and let $f_1, \dots, f_m \in K[X_1, \dots, X_n]$ . The system

f_1(x_1,\dots,x_n) = 0, \quad \dots, \quad f_m(x_1,\dots,x_n) = 0

has no solution $(a_1,\dots,a_n) \in K^n$ if and only if there exist polynomials $g_1,\dots,g_m \in K[X_1,\dots,X_n]$ with

g_1 f_1 + \cdots + g_m f_m = 1.

The "if" direction is immediate (evaluate at a solution); the content is that an inconsistent system always has such an algebraic certificate.

Formalization Note. The polynomials are indexed by $\mathrm{Fin}\, m$ ; for $m = 0$ both sides are false.

Preamble

import Definitions.Def_Nullstellensatz_Defs
import Mathlib

open MvPolynomial

Formal statement

namespace Nullstellensatz

theorem weak_nullstellensatz_system {K : Type*} [Field K] [IsAlgClosed K] {n m : ℕ}
    (f : Fin m → MvPolynomial (Fin n) K) :
    (¬ ∃ a : Fin n → K, ∀ i, eval a (f i) = 0) ↔
      ∃ g : Fin m → MvPolynomial (Fin n) K, ∑ i, g i * f i = 1 := 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), first displayed system and the identity g_1 f_1 + ... + g_m f_m = 1.

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, and let $n, m$ be natural numbers (either may be $0$ ). Let $f_1,\dots,f_m$ be polynomials in $K[X_1,\dots,X_n]$ . The statement is the equivalence of:

there is no point $a \in K^n$ with $f_i(a) = 0$ for all $i = 1,\dots,m$ ;
there exist polynomials $g_1,\dots,g_m \in K[X_1,\dots,X_n]$ such that

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

Edge case: if $m = 0$ , condition 1 is false (every point, including the unique point of $K^0$ , satisfies the empty system) and condition 2 is false (the empty sum is $0 \ne 1$ ).

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