But you have to take into account that the Coq proofs are actual proofs of big THEOREMS. What Buzzard has done is implementing a big DEFINITION :-) Also, the F

But you have to take into account that the Coq proofs are actual proofs of big THEOREMS. What Buzzard has done is implementing a big DEFINITION :-) Also, the Flyspeck project has formalised the proof of a pretty recent theorem as well, mostly in HOL-Light and Isabelle.