fourcolor

Hi, my two cents; you claim "Although mathematicians believe their proof is correct, it is too complex to verify without computer assistance", but I'm not sure "believe" is the correct verb since the proof has been formally verified (see for instance https://github.com/coq-community/fourcolor for a formal verification in Coq). I understand that you want to emphasize the fact that no human can understand the proof with a full overview, but I wonder whether the current sentence will not make people think mathematicians are not perfectly sure of the proof.

Surprised that the article didn't mention that the four-color theorem has been fully formalized in Coq[0], which also helped uncover bugs in the original program used to check the configurations. The formal proof remains maintained to this day with CI continuously checking its validity. It's also been packaged into Nixpkgs.[1] So for those who want to follow along at home and rebuild it: $ nix build --rebuild nixpkgs#coqPackages.fourcolor Takes 4m 19s on my M1 Pro. [0] https://github.com/coq-community/fourcolor [1] https://github.com/NixOS/nixpkgs/blob/master/pkgs/developmen...

Appel and Haken were pioneers in the field of computer proofs. They didn't do it to modern (or contemporary) standards, and it did leave a bad taste for those who seek "elegance" in proof. Since then, theory and practice have advanced in strides; but we may have to agree to disagree on the thrust of your post. I'd strongly recommend Gonthier's treatment of that particular theorem. In my opinon, [1] is beautifully written and illustrated; a shining example of how computer proofs should be written... and [2] is the actual proof. > What we lose when we turn everything over to ML is the ability to understand anything. Yuck, we agree here. [1] https://www.ams.org/notices/200811/tx081101382p.pdf [2] https://github.com/math-comp/fourcolor