Re: Discussion regarding Mr. Diabys algorithm



On 12 Nov 2006 19:51:44 GMT, tchow@xxxxxxxxxxxxx wrote:

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.


I am not sure. I will check. But I am pretty confident that this was
4 color. Will let you know.

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.

As computer engineer (but also with math degree) developing software
that belongs to "mission critical" category I am deeply impressed by
your confidence in software being "error free" or "testable"
Unfortunately, I am not that confident. I also believe that your
remarks reagrding testing techniques are a bit ehem... naive...

A.L.
.