4 ms·
The four color theorem was proven with the help of a computer in 1976 [0]. The event gave rise to the concept of non-surveyable proof [1]. As far as I can tell,
by isolli 6y ago
The four color theorem was proven with the help of a computer in 1976 [0]. The event gave rise to the concept of non-surveyable proof [1]. As far as I can tell, it has never been proven without the help of a computer.
[0] https://en.wikipedia.org/wiki/Four_color_theorem#Proof_by_computer https://en.wikipedia.org/wiki/Four_color_theorem#Proof_by_co...
[1] https://en.wikipedia.org/wiki/Non-surveyable_proof https://en.wikipedia.org/wiki/Non-surveyable_proof
- ogogmad 6y agoAs the Wikipedia article states, the main countermeasure to non-surveyability is to express the proof in formal logic, which can then be verified by an automated proof checker. In fact, this is exactly what the authors of the proof of Keller's conjecture have done. And likewise, the Four Colour Theorem has been verified in this way. I don't think non-surveyability is really the issue here.
- isolli 6y agoNon-surveyability was introduced precisely as a criticism of the 1976 proof. I believe that the four color theorem was proven with the help of an automated proof checker only in 2005.
- MaxBarraclough 6y agoDon't forget the kicker: the original computer-powered proof turned out to to have several serious flaws, brought to light after work done by several researchers unconnected to the original effort. ctrl-f for Schmidt.