Re: Discussion regarding Mr. Diabys algorithm

In article <4gifl2dorm0i7o9604jeol9an6pe9j89d3@xxxxxxx>,
A.L. <alewando@xxxxxxxxxxxx> wrote:
On 12 Nov 2006 19:51:44 GMT, tchow@xxxxxxxxxxxxx wrote:
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.

CPLEX was definitely not used in the proof of the four-color theorem. The
original proof by Appel and Haken (and Koch) dates back to the mid-1970's.
CPLEX 1.0 did not exist until 1988.

The second-generation proof by Robertson, Seymour, Sanders, and Thomas
(http://www.math.gatech.edu/~thomas/FC/fourcolor.html) also does not use
CPLEX.

More to the point, the methods of proof don't involve integer linear
programming, so CPLEX wouldn't even be the relevant tool. On the other
hand, CPLEX was heavily used by Hales.

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
[...]
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"

I said nothing about software being error-free.

Unfortunately, I am not that confident. I also believe that your
remarks reagrding testing techniques are a bit ehem... naive...

I believe your confidence that human checking of proofs is less prone to
error than mechanical checking of proofs is a bit...ahem...naive.
--
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
.

Relevant Pages

  • Re: Discussion regarding Mr. Diabys algorithm
    ... about Hales's proof of the Kepler conjecture. ... But I am pretty confident that this was ... CPLEX was definitely not used in the proof of the four-color theorem. ... the methods of proof don't involve integer linear ...
    (comp.theory)
  • Re: Discussion regarding Mr. Diabys algorithm
    ... The second-generation proof by Robertson, Seymour, Sanders, and Thomas ... so CPLEX wouldn't even be the relevant tool. ...
    (comp.theory)