Gröbner bases of modules and Faugère’s F4 algorithm in isabelle/HOL

Abstract

We present an elegant, generic and extensive formalization of Gröbner bases, an important mathematical theory in the field of computer algebra, in Isabelle/HOL. The formalization covers all of the essentials of the theory (polynomial reduction, S-polynomials, Buchberger’s algorithm, Buchberger’s criteria for avoiding useless pairs), but also includes more advanced features like reduced Gröbner bases. Particular highlights are the first-time formalization of Faugère’s matrix-based F4 algorithm and the fact that the entire theory is formulated for modules and submodules rather than rings and ideals. All formalized algorithms can be translated into executable code operating on concrete data structures, enabling the certified computation of (reduced) Gröbner bases and syzygy modules.