[FOM] Certificates are Fully Practical

[Timothy Y. Chow]

Harvey Friedman wrote:

> Because of the extensive work on "proof assistants", we know from 
> experience (although I an many other people were convinced much earlier) 
> that this expansion process to fully rigorous proofs of actual 
> mathematical theorems by actual mathematicians is well under control and 
> can be and has been carried out in reality.
>
> Granted, this has not been done for really big sophisticated proofs yet, 
> such as FLT and classification of finite simple groups. But there is now 
> little doubt that the certificates have completely feasible size, and 
> will be actually constructed, say by 2150.

For the benefit of FOM readers who may have missed the news last year, the 
formalization of the Feit-Thompson odd-order theorem in Coq was completed 
in October 2012.

http://research.microsoft.com/en-us/news/features/gonthierproof-101112.aspx

I predict that the full classification will be formalized much sooner than 
2150.

Tim