Motivation

Hilbert's Nullstellensatz ("theorem of zeros") is the basic link between algebra and geometry. It was proved by David Hilbert in his second major paper on invariant theory in 1893, after his 1890 paper that proved the basis theorem, and it is a foundational result of algebraic geometry. It gives an algebraic criterion for when a system of polynomial equations over an algebraically closed field has a solution, and an algebraic criterion for when one polynomial vanishes wherever a given family does. Every dictionary between affine varieties and ideals — points and maximal ideals, algebraic sets and radical ideals, irreducible sets and prime ideals — is a consequence.

This mission follows the Wikipedia article Hilbert's Nullstellensatz (snapshot of 27 September 2026): its introduction, its section Formulations, the statement of Zariski's lemma from Proofs, and the first theorem of Generalizations (finitely generated algebras over Jacobson rings).

Setting

Let $k$ be a field and $K$ an algebraically closed field extension of $k$ (every non-constant polynomial over $K$ has a root in $K$). Write $k[X_1,\dots,X_n]$ for the polynomial ring in $n$ variables. A point is an $n$-tuple $a = (a_1,\dots,a_n) \in K^n$, and $f(a)$ is the value of a polynomial $f$ at $a$.

• For an ideal $J$, the algebraic set (zero locus) is $\mathrm V(J) = \{a \in K^n : f(a) = 0 \text{ for all } f \in J\}$.
• For $U \subseteq K^n$, the vanishing ideal is $\mathrm I(U) = \{p : p(a) = 0 \text{ for all } a \in U\}$.
• The radical of $J$ is $\sqrt J = \{p : p^r \in J \text{ for some } r \in \mathbb N\}$.
• For $a \in K^n$, $\mathfrak m_a = (X_1 - a_1, \dots, X_n - a_n)$ is the ideal of the point.
• A subset $W \subseteq K^n$ is irreducible (Zariski topology) if it is nonempty and is not covered by two algebraic sets without lying in one of them.
• A commutative ring is Jacobson if every radical ideal is an intersection of maximal ideals.

Formalization targets

Goal: the Nullstellensatz

If $p \in k[X_1,\dots,X_n]$ vanishes on $\mathrm V(J) \subseteq K^n$, then

$$\exists\, r \in \mathbb N,\qquad p^r \in J.$$

This is the statement of the article's section Formulations, with the coefficient field $k$ and the algebraically closed field $K$ allowed to differ.

Milestones

1. Systems of equations. Over algebraically closed $K$: a system $f_1 = \dots = f_m = 0$ has no solution in $K^n$ iff $g_1 f_1 + \dots + g_m f_m = 1$ for some $g_i$; and $f$ vanishes on all solutions iff $f^r = g_1 f_1 + \dots + g_m f_m$ for some $r$ and $g_i$.
2. Geometric form. $\mathrm I(\mathrm V(J)) = \sqrt J$.
3. Weak Nullstellensatz. A proper ideal of $k[X_1,\dots,X_n]$ has a common zero in $K^n$; algebraic closedness is needed, as $(X^2+1) \subseteq \mathbb R[X]$ shows; for $K = \mathbb C$, $n = 1$ this is the fundamental theorem of algebra: $P$ has a complex root iff $\deg P \ne 0$.
4. Correspondences. $\mathrm V$ is an order-reversing bijection from radical ideals onto algebraic sets, with inverse $\mathrm I$; $\mathrm I(\{a\}) = \mathfrak m_a$ is maximal; every maximal ideal of $K[X_1,\dots,X_n]$ is some $\mathfrak m_a$; an algebraic set $W$ is irreducible iff $\mathrm I(W)$ is prime.
5. Intersections. $\sqrt J = \bigcap_{\mathfrak m \supseteq J} \mathfrak m = \bigcap_{a \in \mathrm V(J)} \mathfrak m_a$.
6. Zariski's lemma. A field finitely generated as an algebra over a field $K$ is a finite extension of $K$.
7. Jacobson rings. A finitely generated algebra $S$ over a Jacobson ring $R$ is Jacobson, and for a maximal ideal $\mathfrak n \subseteq S$, $\mathfrak n \cap R$ is maximal and $S/\mathfrak n$ is finite over $R/(\mathfrak n \cap R)$.

Significance

The Nullstellensatz makes the zero sets of polynomial systems accessible through ideals: solvability of a system becomes the ideal-membership question $1 \in J$, and the geometry of algebraic sets becomes the algebra of radical ideals. Consequences include the identification of the points of $K^n$ with the maximal ideals of $K[X_1,\dots,X_n]$, the description of irreducible algebraic sets by prime ideals, and the reduction of the fundamental theorem of algebra to the case $n=1$. The Jacobson-ring version extends the first equality of the intersection formula to every finitely generated algebra over a field.

All statements here are classical and proved. Mathlib already contains versions of several of them in its own vocabulary (Jacobson rings, Zariski's lemma, and a Nullstellensatz over an algebraically closed coefficient field). What this mission adds is a single set of statements matching the article's formulations: the version with separate fields $k \subseteq K$, the explicit systems-of-equations form, the point-ideal and irreducibility correspondences over $K^n$, and the intersection formula — and, for solvers, the bridges from these concrete statements to Mathlib's abstract ones.

Difficulty

The inclusion $\sqrt J \subseteq \mathrm I(\mathrm V(J))$ is immediate; the content is the reverse inclusion, which requires producing a point of $K^n$ from purely algebraic data. When $k \ne K$ the ideal $J$ lives over $k$ while the points live over $K$, so a result stated only for $K[X_1,\dots,X_n]$ does not apply directly: an ideal of $k[X]$ must be related to the ideal it generates in $K[X]$ without losing membership information. For the correspondences, the explicit ideals $\mathfrak m_a$ and the closed-set definition of irreducibility must be matched with the abstract notions (maximal spectrum, irreducible closed subsets) used in the library.

Formalization scope

• Points of $K^n$ are functions $\mathrm{Fin}\,n \to K$; polynomials are MvPolynomial (Fin n) k. When $k \ne K$, $K$ is a $k$-algebra and evaluation of a polynomial over $k$ at a point of $K^n$ goes through $k \to K$.
• $n = 0$ is allowed throughout; so is the unit ideal $J = k[X]$, where $\mathrm V(J) = \emptyset$ and empty intersections of ideals are the whole ring.
• Irreducibility is stated through closed sets (algebraic sets) without putting a topology on $K^n$. The degree in the $n=1$ statement is Mathlib's Polynomial.degree, with $\deg 0 = -\infty$.
• In the goal, the exponent $r$ may be $0$; that witness only works when $J$ is the unit ideal, so it does not trivialize the statement.
• Out of scope: the proofs via resultants and Gröbner bases, the effective Nullstellensatz, Lang's infinite-variable version, the scheme-theoretic generalizations, and the projective and analytic Nullstellensätze.
• Reusable output: the definitions $\mathrm V$, $\mathrm I$, algebraic set, irreducible set and $\mathfrak m_a$, and bridges to Mathlib's MvPolynomial.zeroLocus, MvPolynomial.vanishingIdeal, and IsJacobsonRing.

Selected references

• D. Hilbert, Ueber die vollen Invariantensysteme, Mathematische Annalen 42 (1893).
• Wikipedia contributors, Hilbert's Nullstellensatz. https://en.wikipedia.org/wiki/Hilbert%27s_Nullstellensatz
• M. F. Atiyah, I. G. Macdonald, Introduction to Commutative Algebra, Addison-Wesley, 1969, Chapters 5 and 7.
• D. Eisenbud, Commutative Algebra with a View Toward Algebraic Geometry, Springer GTM 150, 1995, Chapter 4.