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, \ldots, 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.