3 ms·
The original four color theorem proof used a computer as a computational aid for some nasty casework: the procedure for checking each case and the list of cases
by nyssos 2y ago
The original four color theorem proof used a computer as a computational aid for some nasty casework: the procedure for checking each case and the list of cases that needed to be checked were found by hand.
Proving something in a theorem prover means the proof itself is an object constructed in the prover's language.
- Almondsetat 2y agoI think that's a bit too harsh. An entire complicated proof concocted solely looking at a computer screen in Coq? Every mathematician will have plenty of hand written sketches, ideas and parts of proofs. Does that mean it was "ported" to Coq?
- Sniffnoy 2y ago> I think that's a bit too harsh. An entire complicated proof concocted solely looking at a computer screen in Coq? Nobody is suggesting this, and in this case, it was indeed "ported" to Coq from existing sketches. The distinction here isn't between on-paper-first vs computer-first. The distinction here is between using a custom computer program to perform computations for a mostly-paper proof, versus taking an existing general-purpose theorem-checker (Coq, in this case) and writing down the entire proof in its language so it can check it.
- vilhelm_s 2y agoNo, the point is that the proof itself should be written in the Coq language. The original 4-color proof in 1976 was written in English. They used computer programs to do certain computations, but the proof that those programs were correct and that they were computing the right thing was written in English and checked by humans.