In examples/README, it mentions of exmaples/zenon -- certification of Tom's output using zenon and Coq. Apparently, the "zvtov" tool required for that is part of FoCaLize. Given that Coq was used to create a surveyable proof of 4-color problem, it sounds impressive.
2 comments
[ 2.6 ms ] story [ 11.7 ms ] threadhttp://www.loria.fr/~moreau/Papiers/MoreauRV-CC2003.pdf
In examples/README, it mentions of exmaples/zenon -- certification of Tom's output using zenon and Coq. Apparently, the "zvtov" tool required for that is part of FoCaLize. Given that Coq was used to create a surveyable proof of 4-color problem, it sounds impressive.
Links:
FoCaLize -- http://focalize.inria.fr/
Coq -- http://coq.inria.fr/
http://en.wikipedia.org/wiki/Coq#Four_color_theorem_and_ssre...