Complexity Analysis of the Bivariate Buchberger's 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. This analysis dates back to both the rough complexity analysis in
Buchberger's PhD thesis in 1965 and his paper of 1983 with a completely formal proof for optimal complexity bounds in
the case of two variables. In the past two decades, research has been carried out for creating software systems that can
help in creating and/or verifying formal proofs for mathematical theorems. Among these systems is our Theorema system
(see also the talk "Theorema 2.0: A System for Mathematical Theory Exploration" in this ICMS session).
In this talk, 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 K[x,y] (i.e. rings of bivariate
polynomials over fields) to the discrete space of pairs of natural numbers by a simple map that maps each polynomial to
the exponent vector of its leading monomial (w.r.t. some graduated admissible ordering). All the complexity analysis is
then carried out in the discrete space, mostly by means of combinatorial methods that require many tedious case
distinctions. Since none of these cases requires deep mathematical thinking but only straightforward reasoning, it is
only natural to delegate this task to a theorem prover. 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, and we invented
and implemented a special prover (with special inference rules and proving strategies) for such proofs on tuples of
objects of a certain kind. In the talk we show how the Theorema philosophy of working in parallel both on the meta-level
(inference level) and the object level (design of the notions and theorems) of a theory can lead to a new quality and
style of mathematical research.
In addition to a completely formal and machine-verified proof, as a side-effect of the formal treatment, two
improvements of Buchberger's original elaboration could be achieved: Firstly, the formalized theory does not restrict
the exponents to be the domain of natural numbers but works with far more general domains ("totally-ordered Abelian
monoids"), and secondly we were able to simplify and shorten some of the original proofs drastically. From a
methodological point of view, this is interesting because - as expected in our philosophy - formal treatment of
mathematics will often lead also to improvements of the mathematical content.