Formalizing Mathematics


What? We are interested in formalizing mathematics on a computer. The concrete aim is to make formalizing of known mathematics of the same degree of easiness as writing it up in LaTeX. In addition, we want the formalized mathematics to be available in an active form, that represents also the semantics. So, we want to be able to

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.


The following people in Nijmegen are involved in the research on Formalizing Mathematics.