PhD Defence: Computer-Assisted Exploration of Gröbner Bases Theory in Theorema

In this thesis we present the formal, computer-supported exploration of the theory of Gröbner bases in the mathematical assistant system Theorema 2.0. The core component of the our formalization are so-called reduction rings, introduced by Buchberger more than 30 years ago, which generalize the original setting of Gröbner bases in polynomial rings over fields to a much wider class of algebraic structures, namely commutative rings with identity and a couple of further functions and relations, satisfying a handful of non-trivial axioms. We represented the main definitions, theorems and algorithms of this theory in Theorema and proved all results formally correct using the automated- and interactive reasoning capabilities of the system. Although the mathematical theories we considered in the frame of our studies are by no means novel, we nevertheless managed to contribute to them as well, by (drastically) simplifying one proof, generalizing various definitions and results, and, most importantly, detecting and correcting a subtle error related to reduction rings.