Complexity Analysis of the Bivariate Buchberger Algorithm in Theorema

In this talk we present the formalization and formal verification of the complexity analysis of Buchberger’s algorithm in the bivariate case in the computer system

Theorema

as a case study for using the system in mathematical theory exploration.

We describe how Buchberger’s original complexity proof for Groebner bases can be carried out within the

Theorema

system. As in the original proof, the whole setting is transferred from rings of bivariate polynomials over fields to the discrete space of pairs of natural numbers by mapping each polynomial to the exponent vector of its leading monomial. The complexity analysis is then carried out in the discrete space, mostly by means of combinatorial methods that require many tedious case distinctions, making this proof a natural candidate for automated theorem proving. However, following our

Theorema

philosophy, we do not expect general theorem provers (like resolution provers) to carry out this task in a natural and efficient way. Rather, we designed and implemented a special prover for such proofs. We show how the

Theorema

philosophy of working in parallel both on the meta level (designing and implementing special provers) and on the object level (design of the notions and theorems) of a theory can lead to a new quality and style of mathematical research.