This thesis presents the formal, computer-supported exploration of the theory of Gröbner bases in the mathematical assistant system Theorema 2.0. The main motivation for this work is our conviction that a fully formal, verified and even executable representation of the theory has the potential to facilitate its further expansion in the future. The core component of the computer-formalization are so-called reduction rings, introduced by Buchberger more than 30 years ago. Reduction rings generalize the original setting of Gröbner bases in polynomial rings over fields to a much wider class of algebraic structures, namely essentially commutative rings with multiplicative identity and a couple of further functions and relations, satisfying a handful of non-trivial axioms. We represented the central aspects of this theory in Theorema, including all the main definitions and theorems, and proved the results correct using the automated- and interactive proving facilities of Theorema. Moreover, we also implemented Buchberger's algorithm for actually computing Gröbner bases in a completely generic and directly executable manner and proved it totally correct. The result of all this is now available as a collection of 16 Theorema theories, consisting in total of roughly 2240 formulas, that may serve as the basis for future theory explorations in Theorema; this, in particular, holds for eight theories exclusively dealing with elementary mathematical concepts, such as sets, numbers, tuples, etc., that are themselves absolutely independent of Gröbner bases, reduction rings and Buchberger's algorithm. Although the mathematical theories we considered for formalization 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, correcting a subtle error in the theory of reduction rings. This definitely gives evidence to the claim that mathematics profits from being treated formally in software systems and hence constitutes another motivation for our work in particular and for computer-assisted theory exploration in general. Finally, the thesis also reports on four tools in Theorema we developed in the frame of our studies: a powerful first- and higher-order rewriting mechanism, a set of inference rules for general predicate logic, a versatile proof strategy for interactive proving, and a package of functions for analyzing the logical structure of one or more Theorema theories. Each of these four tools already proved extremely useful during our formal treatment of Gröbner bases theory and will certainly aid future theory explorations in Theorema as well.