[betterunix]

What machine proofs do is concentrate the risk of errors on the proof checker. That is great if your proof checker is reliable, and catastrophic if it is unreliable. Fortunately, proof checkers need not be complicated; you only need a small kernel, from which you can build the rest of the theory.

The other issue is usability. Coq is awesome, but proving something more complicated than basic arithmetic results is hard to do. Likewise with ACL2, PVS, and similar systems. It is getting better, but we are still not quite there.

[kvb]

It's hard to do, but it is being done. See e.g. Gonthier's celebrated work formalizing the Feit-Thompson theorem[1].

[1] http://www.msr-inria.fr/news/feit-thomson-proved-in-coq/