3 ms·
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-tho
by kvb 13y ago
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/ http://www.msr-inria.fr/news/feit-thomson-proved-in-coq/