Re: Discussion regarding Mr. Diabys algorithm

In article <gg2dl2lm2320hq0dpa24k1aefdh37s5gp5@xxxxxxx>,
A.L. <alewando@xxxxxxxxxxxx> wrote:
Computer program can be the argument, but hardly can be a proof. The
Four Color Theorem "proven" using LP CPLEX is still controversial.

The Four Color Theorem was not proven using CPLEX. You may be thinking
about Hales's proof of the Kepler conjecture.

In any case, the number of mathematicians who worry about the objections
that you raise about the operating system having bugs and so forth is
diminishing daily. Certainly there can be bugs, but if bugs are what bother
you, then human checking of proofs is far more bug-prone than computer
checking of proofs, especially if you take the standard precautions of
writing and running code on several entirely independent platforms
(different hardware, OS, source code, compiler, etc.). Furthermore, the
trend nowadays is to move towards machine-checkable certificates, i.e., the
*entire proof* of a statement is provided as a computer file with a very
simple format, and you can write your own very simple program to check that
the file has the claimed format. Then all you have to trust is that your
very short program is correctly verifying the format of the file. The goal
of Hales's Flyspeck project is to produce exactly such a proof of the Kepler
conjecture.
--
Tim Chow tchow-at-alum-dot-mit-dot-edu
The range of our projectiles---even ... the artillery---however great, will
never exceed four of those miles of which as many thousand separate us from
the center of the earth. ---Galileo, Dialogues Concerning Two New Sciences
.