Theory Exploration in Theorema: Recent Approaches to Gröbner Bases Theory

Computer-assisted mathematical theory development primarily aims at the structured representation of a mathematical theory in a software system. In contrast to mathematics in books, this shall happen in such a way that both humans and machines (i.e. software) are able to understand the contents. Among other things, understanding, in the context of software, means that computer programs can derive new facts from known ones fully automatically. In this way, mathematicians who seek to develop new theories based on existing ones are supported, or assisted, by the software systems, and therefore such systems are called mathematical assistant systems. In short, computer-assisted theory development can be thought of teaching maths to computers (but not only calculating, but first and foremost logical thinking). The main objective of this project is the formal development of a particular mathematical theory in the Theorema mathematical assistant system. Said theory is the theory of Gröbner bases. This theory was invented in 1965 by Bruno Buchberger, who also initiated and leads the Theorema project, and nowadays have numerous applications in many areas of natural- and technical sciences, e. g. in robotics, cryptography, thermodynamics, computer-aided design, and many other fields that are concerned with non-linear processes. The focus in the formalization of the theory lies on a method for computing Gröbner bases using matrices, which was invented only recently. First, this method shall be formalized and implemented, and then its correctness shall be proved with the help of the Theorema system (employing Theorema for the proving tasks ensures that every single step in a proof is logically correct and, hence, that no wrong inferences are made). Actually, this is the first time that precisely that aspect of Gröbner bases theory we are going to consider will be formalized in a mathematical assistant system. An important motivation for carrying out this project is the planned participation in the international Global Digital Mathematics Library project, whose ambitious long-term goal is collecting and digitizing a substantial part of mathematics in existence and providing it in a form that can not only be processed by humans, but in particular also by software systems. Buchberger is one of eight members of the steering committee of this global mathematics project. In parallel to the mathematical projects in the frame of Theorema, now also other industrial applications of the automation of mathematical thinking in the areas of the semantic web and the automatic development of software for applications of artificial intelligence are pursued.

The main achievement of this project was the creation of a formal library of mathematical theories concerned with so-called Gröbner bases. This means that we took existing theories, available in the form of articles and textbooks, and translated their natural-language contents into a formal language comprehensible by a software system -- a so-called proof assistant. This software system -- in our case Isabelle/HOL -- then checks every single step in every proof thus translated and confirms that it is indeed correct, and that no further steps are missing. Therefore, formalized mathematical theories can be fully trusted by the scientific community and used as a solid basis for further formal and informal development. In this project, the mathematical theory we were concerned with was the theory of Gröbner bases. Invented in 1965 by Bruno Buchberger, they nowadays constitute one of the central and most widely used theories in commutative algebra. Interestingly, however, only comparably small parts of it had been formalized in proof assistants before. Working on this research project, we extended the available formal theories substantially. In particular, we were interested in recent approaches to computing Gröbner bases by new algorithms that were developed only a few years ago. One such approach consists of transforming the given input, which is a list of polynomials, into a big matrix (i.e. a tabular arrangement of numbers), then performing some well-known operations on this matrix, and finally transforming the result back into the desired output. Furthermore, we also formalized so-called signature-based algorithms for computing Gröbner bases. This class of algorithms was developed around 2001 and proved totally correct in 2012, and represents the state-of-the-art in Gröbner basis computations, outperforming any other known algorithm in almost all instances. These formalizations are the first of their kind in any proof assistant, and are freely accessible by everyone. Hence, they constitute an added value to the scientific community, since researchers and practitioners in the field are now able to base their own formalizations upon them. A second major achievement of this project was the development of an add-on package for the open-source Theorema proof assistant, called Theorema-HOL. Theorema-HOL adds many features present in Isabelle/HOL but missing in standard Theorema to the system. These include, among others, an arsenal of sophisticated methods for proving theorems automatically, and a flexible, text-based interactive proof mode for more complicated theorems that cannot be proved automatically. Originally, we planned to formalize the theories listed above in Theorema-HOL, but unfortunately had to switch to the more mature Isabelle/HOL for the time being, postponing the formalization in Theorema-HOL to a potential future effort.