Indeed, the computer-generated proofs of 4CT were not only not formal proofs, they were not correct. Once a decade, someone would point out an error in the previous version and code his own. But now there is a version for an off the shelf verifier.
Indeed, the computer-generated proofs of 4CT were not only not formal proofs, they were not correct. Once a decade, someone would point out an error in the previous version and code his own. But now there is a version for an off the shelf verifier.