5 ms·

Interestingly, the main article mentions Bill Thurston's paper "On Proof and Progress in Mathematics" (https://www.math.toronto.edu/mccann/199/thurston.pdf http

Interestingly, the main article mentions Bill Thurston's paper "On Proof and Progress in Mathematics" (https://www.math.toronto.edu/mccann/199/thurston.pdf 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 2y ago
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 2y ago
  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.
  - godelski 2y ago
    I think you're missing the core component. We care __WHY__ the theorem is true. To be honest, the __IF__ part matters a lot less. The thing is that the underlying reasoning (the logic) is what provides real insights. This is how we recognize other problems that are similar or even identical. The steps in between are just as important, and often more important. I'll give an example from physics. (If you're unsatisfied with this one, pick another physics fact and I'll do my best. _Any_ will do.) Here's a "fact"[0]: The atoms with even number of electrons are more stable than those with an odd number. We knew this in the 1910's, and this is a fact that directly led to the Pauli Exclusion Principle, which led us to better understand chemical bonds. Asking why Pauli Exclusion happens furthers our understanding and leading us to a better understanding of the atomic model. It goes on and on like this. It has always been about the why. The why is what leads us to new information. The why is what leads to generalization. The why is what leads to causality and predictive models. THe why is what makes the fact useful in the first place. [0] Quotes are because truth is very very hard to derive. https://hermiene.net/essays-trans/relativity_of_wrong.html https://hermiene.net/essays-trans/relativity_of_wrong.html
    - rssoconnor 2y ago
      I do think the why that the Four Colour Theorem is true is captured my statement. The reason why it is true is because there exists some finite unavoidable and reducible set of configurations. I'm fairly sure that people are only getting hung up on the size of this finite set, for no good reason. I suspect that if the size of this finite set were 2, instead of 633, and you could draw these unavoidable configuration on the chalk board, and easily illustrate that both of them are reducible, everyone would be saying "ah yes, the four colour theorem, such an elegant proof!" Yet, whether the finite set were of size 2 or size 633, the fundamental insight would be identical: there exists some finite unavoidable and reducible set of configurations.
      - gsf_emergency_2 2y ago
        If it were size 2, we could more easily make sure that the answer is definitely mind-blowing. Have programmers given up on wanting their mind blown by unbelievable simplicity?
troymc 2y ago
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 https://en.wikipedia.org/wiki/Kepler_conjecture

nicf 2y ago

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 2y ago
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.
- godelski 2y ago
  I think you're missing the core component. We care __WHY__ the theorem is true. To be honest, the __IF__ part matters a lot less. The thing is that the underlying reasoning (the logic) is what provides real insights. This is how we recognize other problems that are similar or even identical. The steps in between are just as important, and often more important. I'll give an example from physics. (If you're unsatisfied with this one, pick another physics fact and I'll do my best. _Any_ will do.) Here's a "fact"[0]: The atoms with even number of electrons are more stable than those with an odd number. We knew this in the 1910's, and this is a fact that directly led to the Pauli Exclusion Principle, which led us to better understand chemical bonds. Asking why Pauli Exclusion happens furthers our understanding and leading us to a better understanding of the atomic model. It goes on and on like this. It has always been about the why. The why is what leads us to new information. The why is what leads to generalization. The why is what leads to causality and predictive models. THe why is what makes the fact useful in the first place. [0] Quotes are because truth is very very hard to derive. https://hermiene.net/essays-trans/relativity_of_wrong.html https://hermiene.net/essays-trans/relativity_of_wrong.html
  - rssoconnor 2y ago
    I do think the why that the Four Colour Theorem is true is captured my statement. The reason why it is true is because there exists some finite unavoidable and reducible set of configurations. I'm fairly sure that people are only getting hung up on the size of this finite set, for no good reason. I suspect that if the size of this finite set were 2, instead of 633, and you could draw these unavoidable configuration on the chalk board, and easily illustrate that both of them are reducible, everyone would be saying "ah yes, the four colour theorem, such an elegant proof!" Yet, whether the finite set were of size 2 or size 633, the fundamental insight would be identical: there exists some finite unavoidable and reducible set of configurations.
    - gsf_emergency_2 2y ago
      If it were size 2, we could more easily make sure that the answer is definitely mind-blowing. Have programmers given up on wanting their mind blown by unbelievable simplicity?

troymc 2y ago

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 https://en.wikipedia.org/wiki/Kepler_conjecture