3 ms·
A proof of this theorem was also formalized in the Rocq proof assistant (called Coq back then). See here for more: https://inria.hal.science/hal-04034866/docume
by jojomodding 8mo ago
A proof of this theorem was also formalized in the Rocq proof assistant (called Coq back then). See here for more: https://inria.hal.science/hal-04034866/document https://inria.hal.science/hal-04034866/document
- macintux 8mo agoReferenced at the very end; I came here to mention the sheer size of this effort. 60,000 lines is incredible. I can barely review 1,000 lines of Python without wanting to become a manual laborer instead. > Ten years later their approach was fully machine-checked by the French computer scientist Georges Gonthier who verified 60,000 lines of formal language proof before declaring that their proof was indeed correct