**Hilbert's basis theorem**, first proved by David Hilbert in 1888, states that, if

*k*is a field, then every ideal in the ring of multivariate polynomials

*k*[

*x*

_{1},

*x*

_{2}, ...,

*x*

_{n}] is finitely generated. This can be translated into algebraic geometry as follows: every variety over

*k*can be described as the set of common roots of finitely many polynomial equations.

Hilbert produced an innovative proof by contradiction using mathematical induction; his method does not give an algorithm to produce the finitely many basis polynomials for a given ideal: it only shows that they must exist. One can determine basis polynomials using the method of Gröbner bases.

A slightly more general statement of Hilbert's basis theorem is: if *R* is a left (respectively right) Noetherian ring, then the polynomial ring *R*[*X*] is also left (respectively right) Noetherian.

The Mizar project has completely formalized and automatically checked a proof of Hilbert's basis theorem in the HILBASIS file.