[jasonhong]

Interestingly, the main article mentions Bill Thurston's paper "On Proof and Progress in Mathematics" (https://www.math.toronto.edu/mccann/199/thurston.pdf), but doesn't mention a quote from that paper that captures the essence of what you wrote:

> "The rapid advance of computers has helped dramatize this point, because computers and people are very different. For instance, when Appel and Haken completed a proof of the 4-color map theorem using a massive automatic computation, it evoked much controversy. I interpret the controversy as having little to do with doubt people had as to the veracity of the theorem or the correctness of the proof. Rather, it reflected a continuing desire for human understanding of a proof, in addition to knowledge that the theorem is true."

Incidentally, I've also a similar problem when reviewing HCI and computer systems papers. Ok sure, this deep learning neural net worked better, but what did we as a community actually learn that others can build on?

[nicf]

The Four Color Theorem is a great example! I think this story is often misrepresented as one where mathematicians didn't believe the computer-aided proof. Thurston gets the story right: I think basically everyone in the field took it as resolving the truth of the Four Color Theorem --- although I don't think this was really in serious doubt --- but in an incredibly unsatisfying way. They wanted to know what underlying pattern in planar graphs forces them all to be 4-colorable, and "well, we reduced the question to these tens of thousands of possible counterexamples and they all turned out to be 4-colorable" leaves a lot to be desired as an answer to that question. (This is especially true because the Five Color Theorem does have a very beautiful proof. I reach at a math enrichment program for high schoolers on weekends, and the result was simple enough that we could get all the way through it in class.)

[rssoconnor]

Is the proof of the Four Colour Theorem really that unsatisfying?

The Four Colour Theorem is true because there exists a finite set of unavoidable yet reducible configurations. QED.

To verify this computational fact one uses a (very) glorified pocket calculator.

[troymc]

Another example akin to the proof of the 4-color map theorem was the proof of the Kepler conjecture [1], i.e. "Grocers stack their oranges in the densest-possible way."

We "know" it's true, but only because a machine ground mechanically through lots of tedious cases. I'm sure most mathematicians would appreciate a simpler and more elegant proof.

[1] https://en.wikipedia.org/wiki/Kepler_conjecture