[FOM] formal proofs (was: Hersh on Flyspeck

[Josef Urban]

Here are some more examples of "accepted proofs":
http://en.wikipedia.org/wiki/List_of_incomplete_proofs

Voevodski describes in
http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/2014_IAS.pdf
several situations of recent buggy proofs and contradictory theorems
in his field that stayed unresolved for some time, and how he started
to feel uncertain about possible errors produced in "high-level" math
research.

Andrzej Trybulec had similar motivation when he started to work on
Mizar in 1973. He wanted a machine to check his (several times
rewritten) PhD thesis in topology under Borsuk. (It was originally
supposed to be a small side-project: "I am a mathematician, so I will
easily program this and then go back to serious science" :-).

Josef

On Sun, Oct 12, 2014 at 12:55 PM, Rob Arthan <rda at lemma-one.com> wrote:
> 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.
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>