Interesting article on progress in automated reasoning

[Timothy Y. Chow]

Sam Sanders wrote:
>> The article also implies that the proof of the four-colour theorem
>> is controversial (another assertion by Michael Harris).
>
> That is indeed absurd, unless arguments were given.

In general, I find myself often disagreeing with Michael Harris, but 
here's the exact quote from the Quanta Magazine article:

> The computer code proving the four-color theorem, which was settled more 
> than 40 years ago, was impossible for humans to check on their own. 
> "Mathematicians have been arguing ever since whether or not it's a 
> proof," said the mathematician Michael Harris of Columbia University.

Without further information, I would not reject Harris's statement here as 
absurd.  As I read it, what is being referred to here is the original 
Appel-Haken-Koch proof.  As far as I'm concerned, it's fair game to argue 
whether that was really a proof.  There were something like 400 pages on 
microfilm tucked into a pocket on the inside back cover of the journal, 
containing innumerable hand-drawn diagrams.  I don't know if anyone ever 
went through them all; there was a serious effort at one point to check 
them, which uncovered numerous errors.  Robertson-Seymour-Thomas was 
partly motivated by the hopelessly messy state of the proof, which they 
gave up trying to verify, in favor of creating a new proof based on the 
same ideas.

This might not have been Harris's objection, but again, purely on the 
basis of what is written in the article, I don't see any reason to reject 
the statement attributed to Michael Harris as absurd.

Tim