"In contrast to humans, computers are good at performing formal processes.
There are people working hard on the project of actually formalizing
parts of mathematics by computer, with actual formally correct formal
deductions. I think this is a very big but very worthwhile project,
and I am confident that we will learn a lot from it. The process will
help simplify and clarify mathematics. In not too many years, I expect
that we will have interactive computer programs that can help people
compile significant chunks of formally complete and correct mathematics
(based on a few perhaps shaky but at least explicit assumptions), and
that they will become part of the standard mathematician's working
environment." (p. 171)
What follows is Thurston's response. It contains an extract from a
message I sent him after reading an earlier draft of this article.
I apologize for any inaccuracies on my part; please bear in mind that
my purpose in this message was to argue that doing formal mathematics
by computer is plausible--even inevitable--and a good thing, too.
Peter Doyle
doyle@math.ucsd.edu
=================================
I have not done much investigation of this personally, but I
have talked to various people, and in particular, Peter Doyle from
the mathematics department at UCSD, who influenced me to make some
modification of what I had said in the earlier draft. In my mind,
the main issue here has to do with the time scale for computer-aided
formalizations to become mathematically important, not about whether
or not it will happen. It could be 5 years, it could be 50 --- but in 50
years, there will be really phenomenal advances in computing, so I think
it is almost inevitable by then.
I will append a quote from one of Peter Doyle's messages, which he wrote when
he saw an earlier draft of this paper. Peter, I hope you don't mind my
quoting you --- maybe you'll add some comments.
Bill Thurston wpt@msri.org
================================
======== Peter Doyle: ==========
================================
I have spent a lot of time over the past three or four months thinking
about formal proofs. I got into this by way of Ed Nelson's massive
work-in-progress (ftp to math.princeton.edu, get qed.tar.Z). Ed has
decided that not only is Peano arithmetic inconsistent, but so is
Robinson's arithmetic, which was the basis for his books "Predicative
Arithmetic" and "Radically elementary probability theory". He is continuing
his program of proving this, which now involves proving everything
formally using his program qed. It is clear that he thinks proving everything
formally is a lot of fun, and it looks like a lot of fun to me, and I think
it will not be as long as you suggest before much of mathematics is
formalized and proven formally. In this connection, I will send along
a copy of the "QED manifesto" which seems to be the work of Boyer and Moore,
and also an article by Boyer and Moore describing their theorem-prover and
detailing the mathematics that has already been formalized using their
theorem prover NQTHM.
I really think that a formal deduction gives you something that you
don't get from an informal proof. It's not better or worse, it's different.
Well, OK, it is worse: We've gotten along fine for thousands of years
without formal deductions, but we couldn't survive without proofs.
But the emerging possibility of doing computer-checked formal deductions
I find very exciting. We just have to remember that formal deductions
are for computers, and proofs are for people. (I like to say that the
proof is the part that's left over when you get done formalizing.)
Ed Nelson and Bob Boyer estimate that generating formal deductions is
between 10 and 100 times slower than it would be to write things out
completely at a level accessible to advanced undergraduates. That seems
kind of plausible to me, and as the tools improve the factor is bound to
decrease. I think there are people who would enjoy formalizing proofs,
and my vision is that we can offer modest cash prizes of say $50 apiece
for formal deductions of our favorite 1000 theorems and let the free market
do its thing.
Of course I'm not advocating formalizing deductions because I think it is
necessary in order to achieve certainty. It will certainly uncover flaws
in certain arguments, and require certain arguments to be changed, and
undoubtedly certain accepted results will turn out to be unredeemably
false. This can't be bad, though I doubt that the rearrangements to our
thinking that will be required will come close to repaying the effort
of formalizing. Nor do I think that mathematics will gain something by
being based on foundations that are less reliable than the structure that
they are supposed to support, and that will have to be replaced when
Ed deduces from Peano's axioms that 2+2=5. It's mainly that I think
it would be fun to see a lot of math formalized. (Like a player piano.)
Concerning your argument that it will be tough to standardize definitions
in a way that will satisfy everyone and anticipate future extensions, I don't
think this should be that much of a problem, though I have worried about it
some. The great thing about having your deductions formalized is that if you
want to make some modest change to the definitions, you should be able to
accomodate this by making modest changes to the deductions. Thus you don't
have to get everything straight once and for all.