Re: [HM] Proofs and the computer

Michael Deakin (mdeakin@gizmo.maths.monash.edu.au)
Wed, 9 Jun 1999 15:57:26 +1000

My understanding is that Frank Allaire, using a different programme,
and allegedly a simpler one, reproduced the result by Haken, Appell &
Katz.

Mike D

>
> You wrote
>
> > The famous 4-colour problem took more or less a hundred years to
> > be "solved" after several intelligent and creative attempts.
> > However, the "proof" required the helping hand of the computer.
> > I once heard the question "How are we to prove the correctness of
> > the program?"
>
> We can't prove its correctness, but think of Wiles's proof of Fermat's Last
> Theorem:
>
> How can we prove its correctness?
>
> We've had fine number theorists go over it with a metaphorical fine-toothed
> comb.
>
> With the 4 color program, perhaps the most effective way is to have a new
> team of programmers under the direction of mathematicians re-program it
> from scratch to try to obtain the same result.
>
> Best wishes,
>
> Sam Kutler
>
>