[FOM] formal proofs (was: Hersh on Flyspeck

[Rob Arthan]

On 12 Oct 2014, at 03:34, Hendrik Boom <hendrik at topoi.pooq.com> wrote:

> When a proof of a major theorem has been completely formalized and 
> mechanically checked there is a tendency to think, "So what?  It was a 
> lot of work, but we already knew the theorem was true.” 


But Kepler “knew” his sphere-packing conjecture was true!  Here is an extract
from what Robert MacPherson wrote as editor of Annals of Mathematics
about the outcome of the peer review process for Hales’s proof of that conjecture:

  " The news from the referees is bad .... They have not been able to certify … the proof,
   and will not be able to certify it ..., because they have run out of energy to devote to the problem.’"

The “problem” here being to verify the output of a large body of computer programs.

MacPherson went on to say:

  “Fejes Toth thinks that this situation will occur more and more often in mathematics.
  He says it is similar to the situation in experimental science --- other scientists acting as referees can’t
  certify the correctness of an experiment, they can only subject the paper to consistency checks.
  He thinks that the mathematical community will have to get used to this state of affairs."

The methods used in the Flyspeck work demonstrate that it is possible to perform large-scale
calculations in such a way that

1) every calculation has a detailed and precise formal mathematical specification, 

2)  the risk of any calculation failing to conform to its specification is mitigated by
automated checks that every step is valid.

As a bonus, you can also formalise and check mechanically the deduction of
the theorem you were interested in (the sphere-packing conjecture, in this case)
from the results of the calculations and the specifications of those calculations.
I say this is a bonus, because it was trying to check the calculations that drained
the energy out of all those referees and their students.

I believe that this demonstrates that the Fejes Toth was too pessimistic: we can carry
out computation with a degree of confidence that is as good as our confidence
in any other kind of mathematical activity. 

> 
> Perhaps machine proof-checking will finally come of age when an attempt 
> to check an important proof reveals that the informal version of 
> the proof is critically flawed in a way that isn't a mere lack of 
> formality, and places the truth of the theorem in doubt.


I think this is like saying that the automobile will finally come of age when
it can fly. In the present context, I think the problem to be addressed is the
increasing dependency on large-scale calculations to make progress in some
areas of mathematics. If mechanised theorem-proving can prevent the
degradation of those areas of mathematics into some kind of experimental
science, then it will have made a very valuable contribution.

Regards,

Rob.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20141012/ba8153f2/attachment-0001.html>