Re:CompCert: A formally verified optimizing C compiler
by thoran on Monday March 02, 2015 @05:13PM
(#9134705)
It's my fault, I think I read your answer too quickly and miss a negation somewhere.
So, yes, a formal rewriting of Wiles' proof is "only" a practical challenge. But a big one. Just about 15 years ago, we were just able to prove the Fundamental theorem of algebra in Coq (a 200 years old theorem that is routinely taught to undergraduates).
So, yes, a formal rewriting of Wiles' proof is "only" a practical challenge. But a big one. Just about 15 years ago, we were just able to prove the Fundamental theorem of algebra in Coq (a 200 years old theorem that is routinely taught to undergraduates).