News for hackers. Stuff that matters.

A comment on A fleet of computers helps settle a 90-year-old math problem. Parent comment

Re:A fleet of computers helps settle a 90-year-old math problem by ogogmad on Thursday August 27, 2020 @04:28AM (#24291297)
As 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.

[ Parent | on HN ]
Re:A fleet of computers helps settle a 90-year-old math problem by isolli on Thursday August 27, 2020 @05:47AM (#24291816)
Non-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.
[ Parent | on HN ]