[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/