Formalizing Mathematics

General

• browse and search libraries of formalized mathematics, (so it should both be readable, like a mathematics book and searchable like a database),
• use the stored formalized mathematics, e.g. by computing with it or proving with it (so it should be possible to actively use the mathematics in a computer algebra system or a theorem prover),
• extend the corpus of formalized mathematics. For example by extending the formalized theory or by adding an illuminating example. Extending should be as easy as writing it up in, say, LaTeX.

Why? There is a lot of mathematical knowledge. This knowledge is mainly stored in books and in the heads of mathematicians and other scientists. Putting this knowledge in the right form on a computer, the mathematics should be more readily available to be used by others (either humans or other computer applications). In this respect, a positive thing about mathematical knowledge is that it has a rather formal (and precise) nature, which makes it easier to formalize.

How? We perform and study concrete (large) formalizations of mathematics in mathematical assistants. Presently there are two types of system in which mathematics can be presented in some kind of semantical form: Theorem Provers (TPs) and Computer Algebra Systems (CAs). The first have the advantage that a lot of mathematical concepts can be represented (defined) very precisely and hence completely formalized proofs can be given. The second have the advantage that it is much simpler to represent mathematics (if it falls within the expressive scope of the CA) and its computation capabilities are much larger.

At present, TPs are the only systems in which one can really formalize a large piece of mathematics, so we focus on those. We are mainly users of Coq and we have experimented (and we presently still are) with some larger developments in Coq. We also develop specific tools for supporting and automating the proof-process. Other systems that we look into are Mizar and HOL-light (but this list may vary from time to time). We have also done some experiments with combining TPs and CAs, to let the TP profit from the computing facilities of the CA. Another topic that we study is the presentation of formalized mathematics. Ideally this should be done via an (interactive) document that can be read roughly as an ordinary mathematics book.

People

• Herman Geuvers
• Henk Barendregt
• Freek Wiedijk
• Dan Synek
• Venanzio Capretta
• Milad Niqui
• Jasper Stein
• Luis Cruz Filipe

Projects

• The Fundamental Theorem of Algebra (FTA) project. This comprises the full formalization in Coq of a constructive proof of the Fundamental Theorem of Algebra (every non-trivial polynomial over the complex numbers has a root). Details can be found at the FTA page. The formalization has been finished by November 2000. We are still building on top of this development and we will make sure that it remains compatible with new versions of Coq.
• Formalizing the real numbers in Coq. This started out as a subproject of FTA: give a complete construction of the reals in Coq. Now we are interested in `real' representations of the reals (i.e. as infinitary objects), the algorithms one can represent over them and the properties that can be proved about them. One of the challenges is to program (and prove correct) actual functions over the reals, within Coq.
• Linear Algebra in Coq. Represent (abstract) notions like vector space, linear transformation, etcetera and construct (concrete) instances of these, like IRxIR, matrix, etcetera. The challenge lies in the connection between abstract structures and their concrete instances.
• Analysis in Coq. Based on the FTA files, define notions like differentiation and integration for real (or complex) valued functions. As TPs are generally more geared towards abstract reasoning than concrete epsilon-delta reasoning (involving many `simple' computation steps), this is a real challenge.
• Four Color Theorem in HOL-light. The four color theorem is a well-known `difficult proof' in mathematics. Various faulty proofs have been given in the 19th and 20th century and the actual (widely accepted) proof consists of a large set of algorithms that all have to be proved correct and executed to obtain the final result. The formalization of this proof is an obvious challenge, because it really requires a lot of computation and also because not all mathematicians accept the existing proof as a `real proof'.
• User Manual for Mizar. Mizar is the oldest (still working) system for theorem proving. It has an impressive library of mathematical results, which is still actively extended. Particular features of the system are that it is batch oriented (not interactive) and uses a `declarative' proof style which is in spirit quite close to ordinary mathematical text. A problem of the system is that it has no user manual, so it is hard to learn and therefore quite under-valued.
• Formalizing Partial Functions. In ordinary (say first order) logic, functions are viewed as single-valued relations. This follows the standard set-theoretic approach and it generalises straightforwardly to partial functions. In formal mathematics, one would like the functions to be actual operations (or even algorithms), allowing to just write f(x) instead of talking about `the y for which R(x,y) holds'. This does not so easily generalize to partial functions, as it is not clear what f(x) means if x is not in the domain of f: is it an illegal expression? or is it legal, but can we just not prove anything about it?
• Combining Coq with a CAs. A first phase of this project is finished, yielding an implementation of a primality checker in Coq, which uses GAP to yield `witnesses'. The algorithm used is based on Pocklington's Criterion, which requires the factorization of large numbers. These factorizations -- which are hard to find in Coq -- are asked to GAP and then checked in Coq. There are more ways in which CAs can be used within a TP, which are still to be exploited.
• Presentation of formalized mathematics. Given a piece of formalized mathematics, we want to present it to the world, e.g. to mathematicians to evaluate it or to students to build on top of it. The actual computer code is very system specific and contains far too much detail to access the material. On the other hand, an `accompanying paper' in the standard mathematical style does not show sufficient detail of what has actually been formalized (and may not at all be a faithful representation of the formalization). Coq has a way of generating natural language from a formalized proof. It is also possible to generate system independent encodings (OMDoc, XML) from Coq proofs. A different angle is taken by Mizar, which tries to keep the proof files themselves close to `ordinary mathematics'. None of these approaches have so far led to a satisfactory solution.

Results