\documentclass[runningheads,envcountsame,envcountsect]{llncs}
\usepackage{amssymb,url,alltt}
\raggedbottom

\def\acro#1{{\small #1}}
\def\footacro#1{{\small #1}}
\def\QED{\acro{QED}}
\def\HOL{\acro{HOL}}
\def\HOLs{{\HOL\hspace{.5pt}s}}
\def\PRL{\acro{PRL}}
\def\sys#1{\hbox to 3.5em{\hss #1\hss}}

\begin{document}

\title{The {\Large QED} manifesto revisited}
\titlerunning{The \footacro{QED} manifesto revisited}
\author{Freek Wiedijk}
\institute{
%Foundations of Computing Science \\
Institute for Computing and Information Sciences \\
%Faculty of Science \\
Radboud University Nijmegen \\
Toernooiveld 1, 6525 ED Nijmegen, The Netherlands}
\maketitle

\begin{abstract}
We present an overview of the current state of formalization of
mathematics, and argue what will be needed to make the vision
from the {\QED} manifesto come true.
\end{abstract}


\noindent
This short and intentionally provocative paper is dedicated to Andrzej Trybulec.
%
When I first wrote about the Mizar system, Andrzej wrote to me:
\begin{quote}
\emph{I have looked to pages that you have prepared. {\rm [\dots]}
I advertise them, even if they are a bit enemical} {\small\texttt{:-)}}
\end{quote}
I hope that Andrzej will enjoy this paper, and will not
consider it to be too `enemical'.


\section{Why the {\large QED} manifesto has not been a success (yet)}

One of the most interesting documents about the formalization of mathematics
is the \emph{{\QED} manifesto} \cite{qed:94}.
This anonymous\footnote{
One of the main people behind the \footacro{QED} manifesto was Bob Boyer,
but for idealistic reasons the authors of the \footacro{QED} manifesto were
not identified in it.
} pamphlet from 1994 paints a future in which most of
mathematics will be put in the computer, even the proofs --
\emph{especially} the proofs -- in such a way that the computer will be able to check it for correctness.
The {\QED} manifesto describes the development of a system, the {\QED} system, that
mathematicians will adopt for this purpose.

The future that the {\QED} manifesto sketches has not happened.
There is no such system as the {\QED} system in regular use by mathematicians
today.
%Yet.
\medskip

\noindent
There are two main reasons that the future from the {\QED} manifesto currently
is not much closer than it was in 1994:

\begin{itemize}
\item
The most important reason is that \emph{only very few people are working on formalization of mathematics.}
If there had been a larger research community interested in that subject, a system
like the {\QED} system would have been realized long ago.

There are various reasons why not many people are working on the
vision from the {\QED} manifesto.
For one thing formalization has no `killer application'.
If one writes a formalization of a mathematical result, then
one has to work quite hard, and then at the end one has a \texttt{tar.gz}
file with several computer program-like files in it.
However, unlike a computer program, those files have no immediate
further use.
The fact that they \emph{fully} describe the mathematics has some aesthetic appeal, and it is nice that they make it completely certain that
the mathematics is correct, but the unformalized version of the result already
was beautiful and understandable, so not much is gained.

There are people who think that \emph{education} is a good application
for this kind of technology.
The use of proof assistant would teach students what proof is, and
it would allow them to work on proofs in a non-threatening, crystal
clear environment.
I strongly disagree with this point of view.
The use of a proof assistant is a way to keep students busy, but
it cannot compete with the more traditional way to do mathematics --
which is much easier --
to actually make them understand something.

An application that \emph{might} become important at some point is the correctness
of computer algebra.
Computer algebra systems (the most important being, in order of the
number of users:\label{list1} Mathematica \cite{wol:96}, Maple \cite{mon:ged:hea:lab:vor:97}, Mu\acro{PAD} \cite{cru:oev:04} and Reduce \cite{hea:95})
are notorious for occasionally giving wrong answers.
This can
be very irritating.
Therefore, building an integrated system that combines the automation of
computer algebra with the correctness of proof assistants might
be seen as a real step forward.
If that happens, it could make
people start using proof assistant technology without them
even realizing it.

An aspect where `{\QED}-like systems' currently are notoriously
bad at is \emph{communication}.
A formalization is completely useless for
communicating the mathematics that is formalized in it.
Here is the most to be gained for
formal mathematics.
In particular the visual side of mathematics is currently completely absent:
there are no such things as graphs and diagrams in current
proof assistants.\footnote{
Proof assistants sometimes show diagrams about the structure of the
\emph{proof process},
like for instance \acro{PVS} does,
but there never are diagrams about the \emph{mathematics}.
}

\item
The other reason that there has not been much progress on the
vision from the {\QED} manifesto is that currently
\emph{formalized mathematics does not resemble real mathematics} at all.
Formal proofs look like computer program source code.
For people who \emph{do} like reading program source code\footnote{
Books that appeal to people like that are for instance Lions' commentary on the Unix kernel source code \cite{lio:77},
Donald Knuth's `{\TeX}: The Program' \cite{knu:86}, and
John Harrison's forthcoming book on theorem proving \cite{har:07}.
However, proof assistants should appeal to more than just those people.
} that is nice,
but most mathematicians, the target audience of the {\QED} manifesto,
do not fall in that class.

To make things worse there are two choices made by large parts
of the formalization community that scare mathematicians away
even more.
Often proof assistants are \emph{constructive} instead of classical,
and often they do proof in a \emph{procedural} way instead of
in the more recognizable declarative way \cite{har:96:2}.
%
If we want to make some progress of getting people actually to use
formal mathematics, it has to be close to the way mathematics
already is being done for centuries.
Improving on tradition is good, but ignoring tradition is
stupid.
This means that the focus in formal mathematics should be on
\emph{classical} \& \emph{declarative} systems.\footnote{
Georges Gonthier, the author of the most impressive formalization
in existence today -- the formalization of the Four Color Theorem \cite{gon:06} --, disagrees with this opinion.
He uses Coq, which is a constructive \& procedural system.
He claims that a primarily procedural approach is much more
efficient than a declarative proof style, and that for that reason
the declarative proof style cannot compete.
}
From this point of view, among the systems from Section~\ref{art} the Mizar and Isabelle/{\HOL} systems
-- the two systems
in that section that are both classical \& declarative -- are the most
interesting.

\end{itemize}

\section{The state of the art in formalization of mathematics}
\label{art}

We define the \emph{{\QED}-like systems} to be the five highest ranking systems
in an investigation of which theorems already have been formalized from
an arbitrary list of 100 well-known theorems.\footnote{
The current state of this investigation can be found on the web page\hfill\break
$\langle${\small\texttt{http://www.cs.ru.nl/\char`\~freek/100/}}$\rangle$.
}
%
The counts as of March 2007 are:
\begin{center}
\begin{tabular}{lr}
\hline
{\HOL} Light & 63 \\
\noalign{\smallskip}
Coq & 38 \\
ProofPower & 37 \\
Mizar & 35 \\
Isabelle/{\HOL} & 33 \\
%\noalign{\medskip}
\noalign{\smallskip}
\acro{PVS} & 15 \\
%\noalign{\smallskip}
nqthm \& \acro{ACL}2 & 12 \\
Nu{\PRL} \& Meta{\PRL}$\quad$ & 8 \\
\hline
\end{tabular}
\end{center}
(At that point in time, in all systems together 77 of the 100 theorems have been formalized.)
Clearly there is some kind of gap after the fifth system, which is why we put the
boundary of being a `{\QED}-like system' there.

This means that the current {\QED}-like systems are:
\begin{itemize}
\item
\textbf{Mizar} \cite{muz:93,wie:07}

\item
{{\HOLs}}

\begin{itemize}
\item[--]
\textbf{{\HOL} Light} \cite{har:00}

\item[--]
\textbf{Isabelle/{\HOL}} \cite{nip:pau:wen:02,wen:02:1}

\item[--]
\textbf{ProofPower} \cite{lem:00}

\end{itemize}

\item
\textbf{Coq} \cite{coq:06}

\end{itemize}
We grouped the three systems from the {\HOL} family together.
They have (almost) the same logic and share a very similar architecture.\footnote{
In one respect they are not similar:
unlike the other {\HOLs}, Isabelle/{\HOL} provides a declarative language called Isar, which is
quite close in look and feel to Mizar.
}
\medskip

\noindent
Projects in the spirit of the {\QED} manifesto have been proposed again and again.
For instance, the Automath project
from the seventies clearly already was one of these.
Here is a list of projects that still are active and that might be considered
to aim at implementing the vision from the {\QED} manifesto.
We indicate with each project which {\QED}-like system it uses.
\begin{itemize}
\item
\textbf{\acro{MML}, the {Mizar Mathematical Library}} (Mizar)

\item
\textbf{John Harrison's work} on the formalization of mathematics ({\HOL} Light)

\item
\textbf{Georges Gonthier's project} in the Microsoft/\acro{INRIA} institute (Coq)

\item
\textbf{The Archive of Formal Proofs} (Isabelle/{\HOL})

\end{itemize}
\noindent
The first and the fourth are just the `collected works' of their respective provers.
(The `contribs' of Coq is another of those, but it does not have
a fancy name, so I did not put it in the list.)
The second and third are currently just the work of one person.
However for the third there are plans to extend it into something that is more,
in the joint Microsoft/\acro{INRIA} institute in Paris.

I do not believe that these four projects are already implementing the vision
from the {\QED} manifesto.
None of these projects have solved the difficult problem of how to
integrate work by multiple people into a nice coherent whole.
The first and the fourth project have contributions from multiple people,
but they currently fail to build a coherent whole out of it.\footnote{
Try for instance finding a lemma in the \acro{MML}!
}
The second and the third projects have a library that is a nice coherent whole,
but these libraries do not yet contain contributions by a significant number
of people.\label{library}

\section{A benchmark of four statements}

Here are four mathematical statements that most mathematicians
will consider to be totally non-problematic\footnote{
Most of them will probably not know the statement of the proper forcing axiom,
but they \emph{will} know the meaning of $\aleph_0$ and $\aleph_2$, and
will consider that meaning to be -- again -- non-problematic.
}:
\begin{enumerate}
\item
$$\int_0^1\!\int_0^1 \sum_{n = 0}^\infty (xy)^n dx\,dy = {\pi^2\over 6\,}$$

\item
\emph{Every field has an algebraic closure.}

\item
\emph{Natural transformations are the morphisms of the functor category.}

\item
\emph{PFA (the proper forcing axiom) implies} $$2^{\aleph_0} = {\aleph_2}$$

\end{enumerate}
We claim that currently none of the {\QED}-like systems can express all four
statements in a good way.
Either they do not have good syntax for it (statement~1 in Mizar),
or their foundations do not give one enough power to define the
notions in these statements in a good way (statement~2 in the {\HOLs},
statement~3 in Mizar, and statement~4 in Coq.)
Here is a table that shows which of the {\QED}-like systems have the
framework to express which of these four statements:
\begin{center}
\label{table1}
\begin{tabular}{lccccccc}
& \sys{Mizar} & \sys{\HOLs} & \sys{Coq} \\
\noalign{\smallskip}
\hline
\noalign{\smallskip}
1. Calculus & $-$ & $+$ & $+$ \\
2. Abstract algebra$\quad$ & $+$ & $-$ & $+$ \\
3. Category theory & $-$ & $-$ & $+$ \\
4. Set theory & $+$ & $-$ & $-$ \\
\noalign{\smallskip}
\hline
\end{tabular}
\end{center}
\noindent
Of course one can easily extend the systems with axioms that allow one
to write down these statements.
However, that really amounts to `changing the system'.
It would mean that both the library and the
automation of the system will not be very useful anymore.
Classical \& extensional reasoning in Coq or abstract algebra
in the {\HOLs} by \emph{postulating} the necessary types and axioms
will not be pleasant without re-engineering the
system.
\medskip

\noindent
The first of these statements\footnote{
Incidentally, computer algebra systems like Mathematica and
Maple produce this result without trouble.
Now why is there no proof assistant that can do the same?
%
Also, note that the sum $\sum_{n = 0}^\infty (xy)^n$ diverges when
$xy \to 1$, so the inner integral is improper for $y = 1$.
}
is from \emph{Proofs from the Book} \cite{aig:zie:01}.
There we find the following `calculation'\footnote{
After this calculation it then is shown that $I = {\pi^2\over 6}$.
The goal in \emph{Proofs from the Book} is not to show the statement
that we put in the benchmark (that is just an intermediate result there), but to show that $\zeta(2) = {\pi^2\over 6}$.
However, for the benchmark we wanted an expression with many nested binders, which is the reason
why we selected this intermediate equality.
}:
\begin{eqnarray*}
I &=& \int_0^1\!\int_0^1 \sum_{n \ge 0} (xy)^n dx\,dy =
\sum_{n \ge 0} \int_0^1\!\int_0^1 x^n y^n dx\,dy \\ &=&
\sum_{n \ge 0} \big(\int_0^1 x^n dx\big) \big(\int_0^1 y^n dy\big) =
\sum_{n \ge 0} {1\over n + 1}{1\over n + 1} \\ &=&
\sum_{n \ge 0} {1\over (n + 1)^2} =
\sum_{n \ge 1} {1\over n^2} =
\zeta(2)
\end{eqnarray*}
\noindent
Now the Mizar system has support for `iterated equalities' like this, but there
is no hope of writing this calculation in Mizar in a way that resembles
the way it is written in the book.
Instead of being able to write
$$\int_0^1\!\int_0^1 \sum_{n = 0}^\infty (xy)^n dx\,dy$$
in Mizar one has to write
$$
\begin{array}{rcrcl}
\hspace{5em} \int_0^1 f(y) dy
& \enskip\mbox{\it where}\enskip & f(y) &=& \int_0^1 g(x,y) dx \\
& \mbox{\it where} & g(x,y) &=& \sum_{n = 0}^\infty h(x,y,n) \\
& \mbox{\it where} & h(x,y,n) &=& (xy)^n
\end{array}
$$
\noindent
Since Mizar has no user-definable `\emph{binders}', one has to introduce a \emph{name} for every sub-expression.
(Another way of saying this is to say that Mizar is too much of a `first order' system.)
This makes doing calculations like the one from \emph{Proofs from the Book}
cumbersome in Mizar.
\medskip

\noindent
The second of the statements from this section is difficult to state in a nice way in the {\HOLs}.
The reason for this is that the {\HOL} type system is too poor.
It is not possible in {\HOL} to define a type of \emph{fields} in a uniform way.
Therefore, instead of writing the formal equivalent of
\begin{quote}
\emph{For all fields \dots}
\end{quote}
in {\HOL} one has to write
\begin{quote}
\emph{For all fields of which the elements are from this given carrier type \dots}
\end{quote}
The quantification of this carrier type will be implicit.
For that reason only universal quantification over these carrier types is possible.
Which means that in {\HOL} it is \emph{not} possible to write
\begin{quote}
\emph{There exists a carrier type together with a field with that carrier type \dots}
\end{quote}
Instead one explicitly has to \emph{construct} a carrier type from the
already given types.
This makes the whole statement clumsy.

Also, one gets a copy of a given field for many different carrier types, and it will need work to navigate these equivalences.
\medskip

\noindent
One would hope that with set theory -- the foundation of Mizar -- one does not have the kind of
problem that the {\HOLs} had with the second statement.
Unfortunately, this is not true.
Mizar has no problems with the statement about fields,
but it encounters a similar problem in a different subject.

If one formalizes category theory in set theory, one steps out of the
set theoretic universe, and therefore one gets exactly the same kind of problem there that the {\HOLs}
have with algebraic structures.
Instead of being able to write
\begin{quote}
\emph{For all categories \dots}
\end{quote}
one needs to write
\begin{quote}
\emph{For all \emph{small} categories \dots}
\end{quote}
or maybe
\begin{quote}
\emph{For all categories that are from this given universe \dots}
\end{quote}
In both cases the categories that one talks about will not be proper classes,
they will be \emph{small} categories,
and therefore the theorems that one proves will not apply to categories
like the category of all groups (which is \emph{not} a small category.)
This is not acceptable.
It means that one cannot talk categorically about the most common kind of
algebraic structure.

When one talks about `natural transformations', one is
not only talking about natural transformations where only small categories are
involved.
Here is a statement that one would like to be able to formalize
without making it more complicated than it informally is:
\begin{quote}
\emph{Consider the category ${\bf Grp}$ of all groups with group homomorphisms
as morphisms.}
\emph{The identity functor ${\rm id}_{\bf Grp} : {\bf Grp} \to {\bf Grp}$
is naturally isomorphic to the opposite functor
${\,\cdot\,\strut}^{\rm op} : {\bf Grp} \to {\bf Grp}$.}
\end{quote}
\noindent
Here the natural isomorphism that is being talked about is a natural transformation
between functors that go from the category of groups to the category of groups.
That is, between {large} categories.

The ideal {\QED} system should allow statements like this without one having to talk
(or even to \emph{think}) about universes.
\medskip

\noindent
Finally, I have never seen the infinities from set theory -- of which
$\aleph_0$ and $\aleph_2$ are the first and the third -- been formalized
in a proof assistant that is based on type theory.
For some reason the Coq system has not really been designed
to talk about set theoretical notions like the cardinal numbers.

Even worse, also more in general it seems that
classical \& extensional mathematics
is much more difficult in Coq than one would like it to be.\footnote{
Of course I would not mind being shown wrong here.
}

\subsection*{Intermezzo: on constructive proof assistants}
A system that implements the {\QED} manifesto should be usable to people
who are not aware of the existence of constructive mathematics.
The possibility to do constructive mathematics with the system,
if at all present\footnote{
Henk Barendregt talks about a \emph{dial} on a proof assistant
that allows people to put it in more or less constructive modes.
This intermezzo describes some settings on such a dial.
}, should be hidden to people who are not interested in it.

Constructive mathematics seems to be all about being able to point your finger
at other people and say `Oh!  They are bad!'
It is a very moralistic kind of mathematics.
%
The Coq people point at the Nu{\PRL} people and say `Oh!  They are extensional!'
(`Type checking of proof terms is not even decidable!')
The Agda people point at the Coq people and say `Oh!  They are impredicative!'
(Apparently impredicativity is not to be trusted for philosophical reasons.)
The other people point at the Agda people and say `Oh!  Their system does not
even check termination!'
Or maybe someone will say about someone else `Oh!  They use countable choice!'
And so on, and so forth.

Instead of trying to prove \emph{as many} true statements as possible, constructive
mathematics is about making it \emph{difficult} to prove something.
(Of course, \emph{if} you then prove it, the proof contains
a bit more information.)
Constructivism also takes a strange position with respect to
a question like `does this mathematical statement hold?'
The answer often is: `It depends on how you interpret the statement';
or maybe: `It depends on what principles you allow yourself.'
I guess that this would surprise many classical mathematicians.

Of course for logicians and other philosophers this is all very interesting,
but classical mathematicians should not be bothered by these issues.
This kind of fine structure of the axiomatics probably does not
interest them.
\medskip

\noindent
There are various ways in which you can be restrictive:
\begin{itemize}
\item
First of all you can allow yourself the use of the law of the excluded middle\footnote{
$p \lor \neg p$.
} or not.
This is the distinction between being \emph{classical} or \emph{constructive}.

\item
Second, you can be \emph{extensional} or \emph{intensional}.
If you are extensional there is \emph{one} equality, that behaves
like you would expect equality to behave.
If you are not extensional you get into a morass of many different
kinds of equality: syntactic identity, convertibility (also called $\beta\delta\iota$-equality), Leibniz
equality, John-Major equality\footnote{
Also called `{heterogeneous} equality'.
This is a typed equality in which one allows the terms that are
being compared to have different types.
Heterogeneous equality generally is a good idea.
The equality of the {\HOLs} is homogeneous, but the equality of
Mizar is heterogeneous.
}, setoid equality, etc. etc.

\item
Third, there is \emph{predicativity}.
Predicativity means that you are not allowed to define something by
referring to a whole that contains the thing being defined.
Although this seems rather clear,
logicians do not agree on which systems are predicative and which are
not.
Some of them claim that the natural formalization of predicativity is
a system called \emph{Feferman-Sch\"utte} \cite{sch:77}.
Others think that `inductively generated structures' are also predicative.
Here we agree with the second -- less strict -- opinion, because else no system
in our list below would turn out
to be predicative.

\item
Finally there is the \emph{axiom of choice}.
Even most classical mathematicians are aware of the fact that one might
do mathematics without choice.\footnote{
If you believe that the union of countably many countable sets is countable,
then you do believe in choice.
}
Now there are various levels of having choice:
\begin{itemize}
\item
The weakest version of choice is to take the statement of the axiom of choice
$$\forall R\,\big([\forall x\,\exists y\,R(x,y)\big] \to [\exists f\,\forall x\;R(x,f(x))]\big)$$
only to give existence of a function $f$ that does \emph{not} have to respect equality.
This is called \emph{intensional choice}, and one gets it for free
in type theory because of the Curry-Howard-de Bruijn interpretation.
(In Coq this is slightly subtle: there this only works for the `informative'
existential quantifier.)
%
In the table below we call this `weak choice'.

\item
Then there is the axiom of choice from set theory.
Here one knows that there is a choice function that respects equality, but one cannot
necessarily define one explicitly.
This axiom is called \emph{extensional choice}.
Constructivists think that this axiom is a confused version of
their intensional choice axiom.

\item
Finally there is the existence of a \emph{Hilbert choice operator}
$\epsilon$, an operator that returns a specific element for any given non-empty
set.

In the table below we call both of these last two properties `strong choice'.\footnote{
There are no systems in the table that have extensional choice
but do not have a Hilbert choice operator.
}

\end{itemize}

\end{itemize}
\noindent
Here is the table that shows which systems satisfy which restrictions:
\begin{center}
\label{table2}
\begin{tabular}{lccccccc}
& \sys{Mizar} & \sys{\HOLs} & \sys{Coq} & \sys{Nu{\PRL}} & \sys{Agda} && \\
&&& \sys{\acro{CIC}} && \sys{\acro{ITT}} & \sys{\acro{IZF}} & \sys{\acro{CZF}} \\
\noalign{\smallskip}
\hline
\noalign{\smallskip}
Classical & $+$ & $+$ & $-$ & $-$ & $-$ & $-$ & $-$ \\
Impredicative & $+$ & $+$ & $+$ & $-$ & $-$ & $+$ & $-$ \\
Extensional & $+$ & $+$ & $-$ & $+$ & $-$ & $+$ & $+$ \\
Weak choice & $+$ & $+$ & $+$ & $+$ & $+$ & $-$ & $-$ \\
Strong choice$\quad$ & $+$ & $+$ & $-$ & $-$ & $-$ & $-$ & $-$ \\
\noalign{\smallskip}
\hline
\end{tabular}
\end{center}
Surprisingly there is no `bottom' proof assistant that has minuses \emph{everywhere}, one that both does not support
extensionality nor any form of the axiom of choice.\footnote{
The `{logic-enriched type theories}' of Peter Aczel \cite{gam:acz:06} are designed to
remove the Curry-Howard-de Bruijn interpretation from intensional type theory.
However, currently this seems primarily to be used as a logical framework, and not yet as a
foundational system for mathematics.
}

\section{A criticism of current systems}

At one of the meetings of the \acro{TYPES} project, Georges Gonthier was mentioning
a paper from the Mizar community to me in which Mizar was described
as a `state of the art proof assistant'.
This seemed to amuse him.
As Mizar is certainly in the same ball park as the proof assistant
that he uses himself -- Coq -- I asked him which of the proof assistants in {his} opinion
\emph{are} `state of the art'.
His answer was that `there is no state of the art proof assistant yet.'

I agree that the {\QED}-like systems that exist today are not good enough
to start developing a library as is described in the {\QED} manifesto.
I will for each of the three classes of the {\QED}-like systems
indicate what in my opinion are their most important weaknesses:

\begin{description}
\item[Why Mizar is not acceptable as the {\QED} system yet.] \strut\\
There are three major reasons why Mi\-zar is not yet attractive enough
to be taken to be the {\QED} system:
\begin{itemize}
\item
In the previous section I already addressed the problem that Mizar
has no way to define {binders}.
This means that common operations from calculus, like
$\sum_{x=a}^b f(x)$, $\lim_{x\to c} f(x)$, ${d \over dx} f(x)$, $\int_a^b f(x)\,dx$, etc.,
can not be properly written down without naming sub-expressions.

\item
An aesthetic flaw of Mizar that is not very important but that \emph{is}
irritating, is that Mizar does not support empty types.\footnote{
For a type theorist this restriction to non empty types is \emph{very} strange.
}
For this reason the Mizar library \acro{MML} has many lemmas that
are restricted to {non empty set}s, while there really is no good
mathematical reason for that.

Also it means that many natural mathematical notions cannot be expressed
as a Mizar type.
For instance it is not possible to talk about `the normal form of a term
in a given term rewriting system' as a Mizar type (because some terms might not
\emph{have} a normal form.)

\item
Finally, and I do not know how important this is but I expect it to be
very important, Mizar does not support `user automation'.
If you, as a user of the system, know a way to solve a certain class
of mathematical problems algorithmically, it is not possible to `teach'
this to the system.

The only people who can do that kind of automation are the developers
of the Mizar system itself, who can add so-called `\emph{requirements}' to the system.
This `closed' architecture is too restrictive.
\medskip

\end{itemize}

\item[Why the {\HOLs} are not acceptable as the {\QED} system yet.] \strut\\
There is one important reason why the {\HOLs} are not yet attractive enough to be taken to be the {\QED} system:
\begin{itemize}
\item
The {\HOL} type system is too poor.
As we already argued in the previous section, it is too weak to properly do
abstract algebra.

But it is worse than that.
In the {\HOL} type system there are no \emph{dependent types}, nor is there
any form of \emph{subtyping}.
(Mizar and Coq both have dependent types and some form of subtyping.
In Mizar the subtyping is built into the type system.
In Coq a similar effect is accomplished through the use of automatic
\emph{coercions}.)

For formal mathematics it is essential to both have dependent types and some form
of subtyping.

\end{itemize}
\medskip

\item[Why Coq is not acceptable as the {\QED} system yet.] \strut\\
There are two important reasons why Coq is not yet attractive enough to be taken to be the {\QED} system:
\begin{itemize}
\item
The foundations of Coq are too complicated.
They are baroque to say the least.
Maybe they are even \emph{beyond} baroque.
They might even be called \emph{rococo}.

There is no paper in which the foundations of Coq are spelled out in full
mathematical precision.
Bob Solovay told me that this was one of the reasons for him to lose interest
in Coq as a system.

Also, apparently giving a set theoretical interpretation to the foundations
of Coq in all its details -- to show Coq's consistency relative to some set theory -- might not be as easy as it sounds.

Also, the foundations of Coq are sufficiently complicated that they are
tinkered with, and therefore change between versions of the system.

\item
As already noted in the previous section,
Coq is not designed for classical mathematics,
which means that doing classical \& extensional mathematics in it is not as
easy as one would like it to be.

At the very least one would need to add some axioms for that.
For instance axioms that would be needed are:
\begin{itemize}
\item
excluded middle
\item
the $K$ axiom\footnote{
The $K$ axiom states that if two dependent pairs
$\langle x_1, y_1\rangle$ and
$\langle x_2, y_2\rangle$ are equal , then $y_1$ has to be equal to $y_2$.
In the Coq logic this is not provable.
(It \emph{is} provable that $x_1$ has to be equal to $x_2$.)
`Dependent pairs' means that the types of the $y_i$ depend
on the $x_i$.
}
\item
axioms for extensionality/quotient types
\item
choice
\end{itemize}
and it is not very clear when enough axioms like that will have been added.


\end{itemize}

\end{description}

\section{What has to be done?}

To realize the vision from the {\QED} manifesto, three things need to happen:

\begin{itemize}
\item
First of all, \emph{a project should be started that is not based on the expectation that other people
will do the work.}

Currently people often just build a system and then hope that other people
will start using it for formalization of mathematics.
The {\QED} manifesto is an even more extreme version of this: it just presents
a \emph{vision}, and then hopes that other people will \emph{both} make
a system and start using it for formalization of mathematics.
That approach does not work.
If you want something accomplished, you should work on it yourself.

An important aspect of this project should be that it should involve
a \emph{small} number of people,\footnote{
The original Unix system was created by only two people (who shared
an office at the time),
Ken Thompson and Dennis Ritchie.
Starting something very good does not need a large group of people.
} and have a clear focus.
Only that way there will be enough coherence to get a good result.

It seems important to focus on formalization of actual
mathematical practice,
and \emph{not} also try to `improve' on the way that people currently
do mathematics.

\item
In this project, \emph{a good system for formalization of mathematics should
be developed.}

As I argued in the previous section, the current crop of systems is
not yet good enough to be the `{\QED} system' in which to build a library of
all of mathematics.

Ideally, the system should be set up in such a way, that the mathematics
that is formalized in it can survive a `redesign of the foundations'.
Suppose that one builds a {\QED}-like library on top of Coq, and
then changes one's mind and switches to a {\HOL}-like system.
Basically, this will mean that one will have to start from scratch.\footnote{
Even if one does not mind having to start from scratch like that
(taking that as the way that science progresses),
it still seems sensible to work with foundations that are not \emph{too} idiosyncratic.
}
%This seems a reason not to start building on a system like Coq.
It seems very arrogant to think that we already know what the best
foundations for our formal library should be, and one would therefore
prefer not to be `locked in' to a specific version of the foundations.

This is one more argument for having a declarative proof style over
a procedural proof style.
Proofs in a declarative style are much more `robust' with respect to
changes in foundation than proofs in a procedural style.
An argument for this is the close similarity between the Mizar and Isar\footnote{
Isar is the proof language of the Isabelle/{\HOL} system \cite{wen:02:1}.
}
proof languages, despite the wildly different foundations of their underlying systems.

I do \emph{not} believe that the {\QED} system will consist of many
different systems living peacefully together.
One of the systems -- hopefully the best one -- will kill the others.
That is how evolution works.
It is this system that should be built.\footnote{
From that point of view, spending time on having different systems be able to communicate their mathematics is lost energy.
}

\item
Finally, \emph{a multi-contributor library of formal mathematics should be created that
is well-organized.}
As I claimed in Section~\ref{library}, the sociological puzzle has not been solved yet of how
to set up a library in such a way that it both admits many contributors, but
also stays well-organized.
Current attempts that have not yet been very successful in this respect are:
\begin{itemize}
\item
\emph{multi-contributor, but not really well-organized:}
\begin{itemize}
\item
\acro{MML}
\item
Coq contribs
\item
\acro{AFP}
\end{itemize}
\item
\emph{well-organized, but not really multi-contributor:}
\begin{itemize}
\item
{\HOL} Light library
\item
C-\acro{C}o\acro{RN} \cite{cru:geu:wie:04}
\end{itemize}
\end{itemize}
\noindent
A good first goal for this library will be to formalize `all of undergraduate mathematics'.
This will take more than a hundred man-years \cite{wie:02:4}, which means that it
will need the involvement of a non-trivial number of contributors.
Also, with something like that it will be clear whether it is well-organized
or not.
\medskip

\noindent
The success of Wikipedia suggests that it might be possible to solve
the puzzle of having \emph{both} many contributors and still also have
a well-organized whole.
However, aiming for a `Wikipedia for formalized mathematics' is for me too much like
hoping that someone else will do the work.
I will believe that such an approach
can be successful when I see it happening.

\end{itemize}

\section{What will happen?}

Henk Barendregt always asks people when they expect the future from
the {\QED} manifesto to arrive.
He tells me that the more experience people have with proof formalization,
the more pessimistic they are about this.
(The answers seem to range from `it already is here!' to `in about fifty years.')

I myself certainly believe that the {\QED} system will come.
If we do not blow up the world to a state that mathematics will not
matter much anymore, then at some point in the future
people will formalize most of their proofs routinely in the computer.
And I expect that it will happen earlier than we now expect.

So I \emph{do} believe that in a reasonable time
\begin{itemize}
\item
a proper system will be created
\item
a proper basic library for this system is made
\item
a proper infrastructure is set up for keeping this library well-organized despite
it having many contributors
\end{itemize}
\noindent
I expect that if the first and third of these items arrive, then
the second of these items -- the {\QED} library -- will flow from that in a natural way.

%I hope this short paper will contribute to bring this time near.

%\medskip
\paragraph{Acknowledgments.}
Thanks to Jacques Carette for interesting discussions about the
relation between formal mathematics and computer algebra.
Thanks to Bas Spitters for explaining to me that there is no consensus
on what the word `predicative' means, by pointing out that there
are people who claim that one can predicatively prove Kruskal's theorem.
Finally, thanks to Michael Beeson, John Harrison and Bob Solovay for
helpful comments on a draft of this paper.

\bibliographystyle{plain}
\bibliography{frk}

\end{document}