Formalizing Mathematics
General
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
- 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
The following people in Nijmegen are involved in the research on
Formalizing Mathematics.
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