[cap-talk] (Was: Web calculus) theory and practice (flame?)

Jed Donnelley jed at nersc.gov
Mon Feb 27 21:48:47 EST 2006


At 05:12 PM 2/27/2006, David Hopwood wrote:
>Jed at Webstart wrote:
> > David,
> >
> > Whew!  I can see I touched a sensitive point on this contrast between
> > theory and practice.  While I see you disagreeing with many of my
> > words, I don't pick up any essential disagreement about our understandings
> > of theory and practice.
>
>Perhaps I am a bit touchy on this subject, yes :-) We don't seem to disagree
>on anything fundamental.

Glad to hear it.

>...
> >> I hope and expect that at some point in the near future (< 10 years),
> >> progress in computer-assisted reasoning will make it feasible to produce
> >> strictly formal proofs (that can be checked by very simple theorem
> >> checkers) with a similar investment of effort as is currently the case
> >> for semi-formal reasoning.
> >
> > I find the above delightful.  I've long argued that it's important to place
> > mathematics on a more formal footing by using computers to check proofs.
> > Many people don't seem to appreciate that while it's indeed impossible to
> > develop an algorithm that will prove all possible "true" statements in
> > adequately rich theories (Gödel, etc.), it's still straight forward (if not
> > necessarily simple) to
> > have computer algorithms check the correctness of any proof.  By having
> > computers do such checking it seems to me that we could avoid some
> > problems like the questions about whether quite complex proofs (e.g.
> > for the Four Color Problem, or Fermat's so-called 'last theorem' or others)
> > are correct.
>
>Actually, precisely this process has recently (2005) been applied by Georges
>Gonthier and Benjamin Werner to one of the proofs of the four colour theorem,
>using the Coq theorem prover:
>
>   <http://mathworld.wolfram.com/Four-ColorTheorem.html>
>
>   Devlin, K. "Devlin's Angle: Last Doubts Removed About the Proof of the Four
>   Color Theorem." January 2005. <http://www.maa.org/devlin/devlin_01_05.html>
>
>   Knight, W. "Computer Generates Verifiable Mathematics Proof."
>   New Scientist Breaking News. April 19, 2005.
>   <http://www.newscientist.com/article.ns?id=dn7286>
>
>   Georges Gonthier's home page at Microsoft 
> Research, from which the Coq proof
>   can be downloaded: <http://research.microsoft.com/~gonthier/>
>
>This still doesn't mean that the proof is at all easy to understand -- it's
>2.6 Mbytes (!) of rather dense code. The important points are:
>
>  - the process is already feasible, even for extremely complicated proofs.
>    That's why I'm estimating less than 10 years 
> for it to become more accessible
>    to mathematicians who are not experts in computer-based theorem proving.
>
>  - unlike the 1976 Appel and Haken computer-verified proof of the 4-colour
>    theorem, which relied on software specific to that proof, to accept this
>    version you only need to trust Coq and its libraries (which you can run
>    using diverse compilers and hardware).
>
>This is the same Georges Gonthier who 
>co-developed the join calculus, incidentally.

Ho Ha!  Thanks for the above references!  I'm 
happy to see that approach being pursued. I found this interesting from:

http://www.maa.org/devlin/devlin_01_05.html

"What makes the new result particularly 
significant from a reliability point of view is 
that the proof assistant Gonthiers employed, 
called Coq, is a widely-used general purpose 
utility, which can be verified experimentally..."

Do you know what is meant my "verified experimentally"?

I guess I'll have to look somewhat more into the 
above "Coq" proof assistant.  My hope has been 
that a proof verifier could be simple enough that 
many people (including Mathematicians) could 
examine the program and verify it directly.  A 
verifier can be quite simple, in principle 
(there's that word again) ;-).  Just verify that 
each statement is either an axiom, a previous 
proven result, or follows from some of those by a 
rule of inference.  Then I imagined that all of 
Mathematics would be put into a database of 
axioms and proven statements that could be 
referenced in any future proofs as 
needed.  Somehow I had this idea that 
Mathematicians would still prove theorems in 
pretty much the usual way, but then would give 
any proofs to graduate students or the like to 
transcribe the proof into a computer readable 
form for mechanical verification.  Pretty blue 
sky I know.  I'll be interested to see how close 
the reality matches my initial blue sky thoughts.

> > The above is quite different from the effort of, say, the Principia
> > Mathematica (which seems to have had relatively little - dare I say it -
> > 'practical' value) where the emphasis was on completing mathematics.
>
>Principia Mathematica had some significant, if indirect, influence on later
>developments -- for example, the Ramified Theory of Types that it introduced
>was one of the first type theories.

Interesting.  I've never before heard that term 
"ramified".  Most of my exposure to
set theory was to ZF set theory where, as I 
recall, no theory of types is needed.
I'll have to catch up a bit on some of these 
areas.  Thanks again for the references.

--Jed http://www.webstart.com/jed/ 




More information about the cap-talk mailing list