A Proof of Hilbert Basis Theorem and an Extension to Formal Power Series

The Hilbert Basis Theorem is enlisted in the extension of Wiedijk's catalogue "Formalizing 100 Theorems", a well-known collection of challenge problems for the formalization of mathematics.

In this paper, we present a formal proof of several versions of this theorem in Isabelle/HOL. Hilbert's basis theorem asserts that every ideal of a polynomial ring over a commutative ring has a finite generating family (a finite basis in Hilbert's terminology). A prominent alternative formulation is: every polynomial ring over a Noetherian ring is also Noetherian.

In more detail, the statement and our generalization can be presented as follows:

• Hilbert's Basis Theorem. Let $\mathcal{R}[X]$ denote the ring of polynomials in the indeterminate $X$ over the commutative ring $\mathcal{R}$. Then $\mathcal{R}[X]$ is Noetherian if and only if $\mathcal{R}$ is.
• Corollary. $\mathcal{R}[X_1,\dots ,X_n]$ is Noetherian if and only if $\mathcal{R}$ is.
• Extension. If $\mathcal{R}$ is a Noetherian ring, then $\mathcal{R}[[X]]$ is a Noetherian ring, where $\mathcal{R}[[X]]$ denotes the formal power series over the ring $\mathcal{R}$.

We also provide isomorphisms between the three types of polynomial rings defined in HOL-Algebra. Together with the fact that the Noetherian property is preserved by isomorphism, we get Hilbert's Basis Theorem for all three models. We believe that this technique has a wider potential of applications in the AFP library.