|
|
|
|
|
|
by vilhelm_s
709 days ago
|
|
|
No, 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. |
|
|