[FOM] Mathematical Certainty Problem

[Harvey Friedman]

Reply to Baldwin 8:41PM 7/2/03.

>I am reposting Leo Marcus's note because I think many readers, those 
>as uniformed as I, may have missed the
>significance.  Hale's proof involves extensive computer checking. 
>The paper has been accepted by the Annals
>(with an asterisk).  Hales is  organizing a project for further computer work.
>
>Leo Marcus wrote:
>
>>For a popular exposition of some relevant issues,
>>see  the article in Nature about Hales' proof of the
>>Kepler Conjecture:
>>
>>
>>http://www.nature.com/cgi-taf/DynaPage.taf?file=/nature/journal/v424/n6944/full/424012a_fs.html
>>

This is a note to clarify the relationship between the issues raised 
in this article and the issues that I have been discussing in my 
postings regarding "Mathematical Certainty Problem".

1. I discussed only the verification of human created proofs, and 
said nothing about the verification of computer assisted proofs.

2. In the process of verification of human created proofs that I was 
discussing, a human - possibly the original author, or possibly 
someone else - who COMPLETELY UNDERSTANDS THE PROOF IN THE NORMAL 
WAY, first provides a Lemma enriched exposition, and then gradually 
turns this into a computer assisted FORMAL proof. The formal proof - 
with extreme annotation - is then checked by the infallible CORE 
PROOF CHECKER, which is a universally accepted standard.

3. In the process I am talking about, the original proof is 
completely understood in human terms, involving no computers.

4. If one wants to extend my discussion to ORIGINALLY computer 
assisted proofs, then in general one must get into the business of 
formal verification of computer programs - although in some relevant 
cases, this might be avoided by forcing the computer to leave 
telltale tracks that can be used for special purpose verification.

Harvey Friedman