Piotr Rudnicki 
Dept. of Computing Science, University of Alberta
Edmonton, Alberta, Canada T6G 2E8 
http://web.cs.ualberta.ca/~piotr

On a Repository of Formalized Mathematics

I am interested in certain pragmatic aspects of building a repository
of formalized, machine checked mathematics.  I take it for granted
that the value gained from building such a repository or repositories
is self evident.  This is a bold assumption in the light of the thin
response to the QED Manifesto (http://www-unix.mcs.anl.gov/qed),
particularly from core mathematicians.

It puzzles me why we have so many different proof assistant systems
for doing formalized mathematics and yet the body of formalized
mathematics organized in a systematic way is so pathetically small.  I
have been involved in the Mizar project for the last 30 years (see
http://mizar.org).  The Mizar Mathematical Library (MML) is considered
the largest of such formalized repositories, yet it is minuscule with
respect to the body of established mathematics.  Even within the Mizar
system, people more frequently propose changes to the system rather
than, say, volunteer to complete the long ago started formalization of
the Jordan curve theorem.

Mizar to a large extent is conducted by a group of enthusiasts with
very mediocre support from funding agencies.  It is an exception
rather than a rule that an actively working mathematician is willing
to learn Mizar and even when they do, their interest is typically
short lived.  It is possible that Mizar is not good enough for them
while it is commonly believed that Mizar is closest to the way daily
mathematics is done.  Leibniz dreamt about such a system, Peano
started building it using pencil and paper and met with indifference
towards his endeavor.

The QED Manifesto noted that we have to involve mathematicians into
using proof assistants and contributing to the repository of proof
checked mathematics.  This has not materialized.  It is my opinion
that current proof assistants offer very little that can attract a
mathematician to use them.  The use of proof assistants in teaching
does not seem to be more widespread than say 10 years ago.  I have
resigned from using Mizar for undergraduate teaching as I could not
find qualified instructors and teaching assistants.

On the other hand, Computer Algebra Systems (CAS), with all their
shaky foundations, are gaining wider and wider usage as they really
offer some real assistance in a daily work in some branches of
mathematics.  The hoped for marriage between CAS and proof assistants
would probably help the latter in gaining wider usage.  However, for
such a marriage to materialize we need the proof assistants to be
developed to a certain level and here the circle closes as it is not
clear who will do it.

I am planning to contribute to MML and my plans for the future are
based on the hope that in a longer period MML will grow to the point
that we can attract some interest of research mathematicians.  Some
recent efforts in expressing the contents of MML in formats acceptable
by automated theorem provers may substantially change the perspective
in a short time and thus I remain moderately optimistic about the
formalized repository of mathematics gaining wider use.

There is quite a number of ongoing efforts within the Mizar project
which aim at formalizing substantial fragments of mathematics.  I
would like to name a few: the theory of continuous lattices, Jordan
curve theorem, the theory of Groebner bases.  The central question is:
how can we attract mathematicians to contribute to such a repository?