This is really very cool, and makes me want to pick up Coq again. I know the set of formally verified proofs is very small as compared to traditional mathematics, but I think Coq and its cousins are vital for a future revolution in mathematics.