\documentclass{llncs}
\begin{document}
\title{Estimating the Cost of a Standard Library\\for a Mathematical Proof Checker}
\author{Freek Wiedijk}
\institute{\email{freek@cs.kun.nl}\\University of Nijmegen}
\date{}
\maketitle
\begin{abstract}
We estimate the cost of formalizing a proper standard library
for proof checking of mathematics in the spirit of the QED project.
Apparently it will take approximately {\em 140 man-years}.
This estimate does not include the development of the proof checking program,
nor does it include work on the metatheory of that program.
This should discourage any individual or small research group to think they
can reach anything like the goal of the QED project on their own.
\end{abstract}
\section{Introduction}
\subsection{Problem}
The utopia of the QED manifesto \cite{qed:94} is that in the future
all of mathematics will be formalized in a computer.
That it will be formalized in such a way
that one can be completely sure that it is correct.
(One can be completely sure that it is correct, {\em except\/} of course for paradoxes
in the foundations of the logic and bugs in the kernel of the checking
software.
But that logic can be very simple and clear and that kernel can be very small.)
This dream has been dreamt many, many times (the Automath project
\cite {ned:geu:vri:94},
the Mizar project \cite{wie:99:1}, the QED project \cite{qed:94}, the MBase project \cite{fra:koh:00}, it
has been dreamt many times)
and until now nothing has happened.
A favorite passtime of people who like to dream this dream is to
guess how long it will take before the utopia arrives.
Our guess is that when enough mathematics has been formalized,
when the {\em library\/} of formalized mathematics is powerful
enough, people will start routinely formalizing mathematics.
So the thing to estimate is: when will this library be sufficiently large?
That's the subject of this note.
\subsection{Approach}
`Drake's equation' is a way to guess the number of alien civilizations in our galaxy
that are able to communicate with us.
It guesses various factors and multiplies them together to get a very
rough estimate of this number (the point of course is that this estimate is bigger than zero).
We will use a similar approach to Drake's equation.
We will take various factors and combine them to get an estimate
on the number of man-years it will take to get a proper
library of formalized mathematics.
The difference between our approach and Drake's equation is that
the numbers in Drake's equation are all highly speculative while
our numbers are backed by solid experience in research in formal
mathematics.
\subsection{Related work}
As far as we know this estimate has not been published before.
\subsection{Contribution}
We estimate the amount of work needed to arrive at a library
that will be a proper basis
for a world in which mathematics can be formalized routinely.
\subsection{Outline}
In Section \ref{size} we argue what we think should be in
a good library for formal mathematics.
In Section \ref{cost} we study how expensive formalizing mathematics
is.
In Section \ref{estimate} we combine these numbers to estimate
the cost of a good library for formal mathematics.
\section{The union of what all mathematicians know or the intersection
of what all mathematicians know?}\label{size}
Projects that dream the QED dream tend to promise the sky.
Their goal invariably is to formalize {\em all\/} of mathematics.
(As an example of this kind of `grand dream',
the people of the MBase project \cite{fra:koh:00} compare their goals
to that of the human genome project.
Probably they think that `if you promise more, you get more.'
Funding money for their project, that is.)
However this might not be the right approach.
Consider the field of {\em hypertext}.
This used to be an utopian field, just like formal mathematics.
Only a few researchers were active in this area, dreaming of a future
in which all text would be linked together in an interactive net
of hypertext.
And then, suddenly, there was the World Wide Web.
Clearly the thing needed for hypertext to take off was not that
it was {\em perfect}, but that it was {\em good enough}.
We hope for a similar thing to happen to formal
mathematics.
So what would {\em good enough\/} mean for a library of formal mathematics?
Our guess is that it should contain what working mathematicians
take for granted.
These people don't want to be bothered with formalizing mathematics
that `everybody knows'.
So the library should contain the common knowledge of
most mathematicians.
A good approximation to this is:
\begin{center}
{\em the mathematics in the undergraduate
curriculum of a mathematics study}
\end{center}
In \cite{wie:99:2} we investigated the programs of the undergraduate mathematics
studies of the six Dutch universities in which you can study mathematics.
All six turned out to be almost exactly the same.
They all had the following 12 subjects:
\begin{center}
\begin{tabular}{ccl}\label{table}%
a &$\qquad$& Algebra\\
b && Analysis\\
c && Calculus\\
d & 05 & Combinatorics\\
e & 30 & Complex Variables\\
f & 34 & Differential Equations\\
g & 51 & Geometry\\
h & 28 & Integration\\
i & 15 & Linear Algebra\\
j & 03 & Mathematical Logic\\
k & 60 & Probability Theory\\
l & 54 & Topology
\end{tabular}
\end{center}
(In the second column is the MSC classification of these subjects, when appropriate.)
So this is what we think needs to be in a good library of formal mathematics.
\section{How much work is it to formalize something?}\label{cost}
In \cite{wie:00} we studied the relation between the size of an informal
text of mathematics and its formal counterpart.
We called this the {\em de Bruijn factor}.
We measured it for various formalizations in various systems
(good ones, like Mizar and HOL) and in all cases it turned out to be close to 4.
So this number predicts the size of a formalization.
To predict the amount of work needed to {\em write\/} such a formalization we
use two data points:
\begin{itemize}
\item
In the FTA project in Nijmegen \cite{geu:wie:zwa:00} a formalization
of 1 megabyte of formal text was created with approximately
3 man-years of work.
\item
In the Mizar library MML the average size of an {\em article\/}
is 70 kilobytes and writing such an article takes about 1 month.
If we include revisions to the article that are made afterwards,
we can estimate the total work on an article through time to be 1.5 months.
This means it takes is 2 man-years to formalize 1 megabyte of MML text.
\end{itemize}
Below we use the factor of 2.5 man-years per megabyte.
\section{The cost estimate}\label{estimate}
To get a proper library of mathematics it should include a formalization
of textbooks for all 12 subjects from Section \ref{size}.
This textbook should thoroughly cover the basics of the subject.
We guess that such a textbook will have to be about 400 pages long.
A page in such a textbook is about 3 kilobytes of text.
Now we can put our numbers together.
`Drake's equation' to estimate the cost of a good basic library for
formal mathematics is:
\begin{center}
$\mbox{\em number of subjects\/}\cdot\mbox{\em textbook pages per subject\/}
\cdot\mbox{\em kilobytes text per page\/}\cdot\mbox{\em de Bruijn factor\/}\cdot
\mbox{\em man-years per kilobyte of formalization}$
\end{center}
If we plug in the numbers we get:
\begin{eqnarray*}
12\cdot 400\cdot 3\cdot 4\cdot {2{1\over 2}\over 1024} &\approx& 140
\end{eqnarray*}
So it will take 140 man-years to create a good basic library for formal
mathematics.
Here are some numbers {\em per subject\/} that are related to this estimate,
as a sanity check:
\begin{center}
\begin{tabular}{lrl}
{\em Amount of text in a solid textbook\/} & 1.2&megabytes\\
{\em Size of a formalization of such a textbook\/}$\quad$ & 5&megabytes\\
{\em Number of MML article equivalents\/} & 72&articles\\
{\em Cost to formalize such a textbook\/} & 12&man-years\\
{\em Number of Ph.D. equivalents to do this\/} & 6&Ph.D.s\\
\end{tabular}
\end{center}
(We assume here that while doing a Ph.D., about 2 years work is spent
on formalizing, and the rest of the time is spent on other things
like writing the thesis.
So each Ph.D. equivalent would write 12 MML article equivalents in that time.)
\section{Conclusion}
\subsection{Discussion}
Utopian people tend to think they can change the world alone.
People who dream the QED dream like to think that they can make
the {\em perfect proof checker\/} by themselves and when it's
there the QED utopia will arrive.
We claim that the library is
much more important that the system.
A good system without a library is useless.
A good library for a bad system still is very interesting
(the system might be improved or the library might
be ported to a different, better, system).
So the library is what counts.
Therefore the cost estimate from this note should discourage people
or even small research groups
from thinking that {\em they can change the world alone}.
They can't.
It just is too much work.
\medskip\noindent
It is interesting to compare the numbers of this note to the
size of the Mizar library MML.
It consists of 700 articles which took about 90 man-years to
create.
It might seem that the `standard library' as we describe it in this note
is already there.
However most articles in the Mizar library are about topics that
would not be in the library that is proposed here.
In the MML many articles are about more advanced mathematics
than are treated in an undergraduate curriculum and
many MML articles are about applications from computer science.
Also the Mizar library has not been created by translating
textbooks.
Therefore it is not as complete and well organized as a systematic
translation of a good textbook would be.
\medskip\noindent
One might try to modify the numbers in our equation based
on optimistic thoughts about what the future might bring.
Maybe the proof checkers of the future will be so much better
that the de Bruijn factor drops significantly (maybe even below
1!)
Or they become so much easier to use that a person can produce much
more formalized text in the same time.
One should realize that there are reasons to think the numbers
might have to be adjusted in the other direction.
In a textbook basic results often are just taken for granted.
For instance in a book about complex variables (subject `e'
in the list on page \pageref{table}) the {\em Jordan
curve theorem\/} probably is passed over in a few
lines.
In the Mizar project people have been working on a formalization
of this theorem since 1992 \cite{nak:kot:92} and still they're not finished.
Currently there are about 30 articles in this formalization,
so until now it has taken around 4 man-years of work.
(Admittedly, if they had chosen a more abstract proof, like the one
in \cite{new:92}, they
would probably have been finished by now.)
Apparently formalizing only a few lines in a textbook
can sometimes take a very long time.
\subsection{Future work}
Create a library as described in this note.
%\bibliographystyle{plain}
%\bibliography{frk}
\begin{thebibliography}{1}
\bibitem{qed:94}
R.~Boyer.
\newblock {The QED Manifesto}.
\newblock In A.~Bundy, editor, {\em Automated Deduction - CADE 12}, volume 814
of {\em LNAI}, pages 238--251. Springer-Verlag, 1994.
\newblock \hfill\break URL: \verb||.
\bibitem{fra:koh:00}
Andreas Franke and Michael Kohlhase.
\newblock {System Description: MBase, an Open Mathematical Knowledge Base}.
\newblock In {\em CADE-17, Pittsburgh}, 2000.
\bibitem{geu:wie:zwa:00}
H.~Geuvers, F.~Wiedijk, and J.~Zwanenburg.
\newblock {Equational Reasoning via Partial Reflection}.
\newblock In {\em Theorem Proving in Higher Order Logics, 13th International
Conference, TPHOLs 2000}, volume 1869 of {\em LNCS}, pages 162--178, Berlin,
Heidelberg, New York, 2000. Springer Verlag.
\bibitem{nak:kot:92}
Yatsuka Nakamura and Jaros{\l}aw Kotowicz.
\newblock {The Jordan's Property for Certain Subsets of the Plane}.
\newblock {\em Journal of Formalized Mathematics}, 4, 1992.
\newblock MML Identifier: \verb|JORDAN1|.
\bibitem{ned:geu:vri:94}
R.P. Nederpelt, J.H. Geuvers, and R.C.~de Vrijer.
\newblock {\em Selected Papers on Automath}, volume 133 of {\em Studies in
Logic and the Foundations of Mathematics}.
\newblock Elsevier Science, Amsterdam, 1994.
\bibitem{new:92}
M.H.A. Newman.
\newblock {\em Elements of the Topology of Plane Sets of Points}.
\newblock Dover Publications, 1992.
\bibitem{wie:99:1}
F.~Wiedijk.
\newblock {Mizar: An Impression}.
\newblock \hfill\break URL:
\verb||, 1999.
\bibitem{wie:99:2}
F.~Wiedijk.
\newblock {Selecting the Domain of a Standard Library for a Mathematical Proof
Checker}.
\newblock \hfill\break URL:
\verb||, 1999.
\bibitem{wie:00}
F.~Wiedijk.
\newblock {The De Bruijn Factor}.
\newblock \hfill\break URL:
\verb||, 2000.
\end{thebibliography}
\end{document}