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 progra

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 https://github.com/coq-community/fourcolor [1] https://github.com/NixOS/nixpkgs/blob/master/pkgs/development/coq-modules/fourcolor/default.nix https://github.com/NixOS/nixpkgs/blob/master/pkgs/developmen...