Re: Discussion regarding Mr. Diabys algorithm

On 13 Nov 2006 16:23:47 GMT, tchow@xxxxxxxxxxxxx wrote:

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.


I checked my resources. Agree with the above.


I believe your confidence that human checking of proofs is less prone to
error than mechanical checking of proofs is a bit...ahem...naive.

Maybe. But I am always worrying when I am taking monies using ATM...
A.L.
.