[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