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

Benjamin Puyobro 📧, Benoît Ballenghien 📧 and Burkhart Wolff 📧

February 12, 2025

Abstract

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 R[X] denote the ring of polynomials in the indeterminate X over the commutative ring R. Then R[X] is Noetherian if and only if R is.
  • Corollary. R[X1,…,Xn] is Noetherian if and only if R is.
  • Extension. If R is a Noetherian ring, then R[[X]] is a Noetherian ring, where R[[X]] denotes the formal power series over the ring 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.

License

BSD License

Topics

Session Hilbert_Basis