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.