# Re: Discussion regarding Mr. Diabys algorithm

*From*: A.L. <alewando@xxxxxxxxxxxx>*Date*: Sun, 12 Nov 2006 19:32:13 -0600

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.

.

**Follow-Ups**:**Re: Discussion regarding Mr. Diabys algorithm***From:*tchow

**References**:**Re: Discussion regarding Mr. Diabys algorithm***From:*deepakc

**Re: Discussion regarding Mr. Diabys algorithm***From:*Patricia Shanahan

**Re: Discussion regarding Mr. Diabys algorithm***From:*Radoslaw Hofman

**Re: Discussion regarding Mr. Diabys algorithm***From:*A . L .

**Re: Discussion regarding Mr. Diabys algorithm***From:*tchow

- Prev by Date:
**Re: Discussion regarding Mr. Diabys algorithm** - Next by Date:
**recursion theorem from sipser book ...** - Previous by thread:
**Re: Discussion regarding Mr. Diabys algorithm** - Next by thread:
**Re: Discussion regarding Mr. Diabys algorithm** - Index(es):