|
|
|
|
|
|
by gergo_barany
723 days ago
|
|
|
That Coq proof is not "without computer assistance". No Coq proof is, as Coq is literally an "assistant" that runs on a computer. And those many jobXtoY.v and taskXtoY.v files sure look like they also do the same as the Appel and Haken proof, namely enumerate lots and lots of cases that are then machine-checked. So I don't think the computerized Coq proof is really qualitatively different from other computerized proofs that enumerate so many cases that a manual check would be impractical. |
|
|