[FOM] Certificates are Fully Practical

Timothy Y. Chow tchow at alum.mit.edu
Fri Sep 20 21:58:33 EDT 2013

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.


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


More information about the FOM mailing list