I thought there were several examples of theorems that had only been proved by computers, like the Four Color Theorem, but that they’re sort of in their own universe because they rely on checking thousands of cases, and so not only could a person not really be sure that they verified the proof (because the odds of them making a mistake would be so high) they couldn’t get much in the way of intuition or shared technique from the proof.
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.
I thought there were several examples of theorems that had only been proved by computers, like the Four Color Theorem, but that they’re sort of in their own universe because they rely on checking thousands of cases, and so not only could a person not really be sure that they verified the proof (because the odds of them making a mistake would be so high) they couldn’t get much in the way of intuition or shared technique from the proof.
Yes, although as far as I know things like that, and the FCT in particular, have only been proved by custom software written for the problem.
There’s also a distinction between using a computer to find a proof, and using it to formalise a proof found by other means.
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.