[FOM] Has Principia Mathematica been formally verified?

[Timothy Y. Chow]

Thanks to all those who replied to my query, including some who sent me 
email but whose replies may not appear on FOM.

I should clarify that my interest is primarily historical.  I don't care 
about the actual theorems in PM for their own sake, or even so much about 
automating the process of finding proofs of those theorems.  What I wanted 
to know was how much "updating" needed to be done to shoehorn PM into a 
modern formalist viewpoint, and, assuming that the answer to that question 
was "relatively little," how much correcting and gap-filling would be 
needed to get PM to meet the standards of a computer program.  I thought
that PM would serve as an interesting benchmark in this regard.

The most relevant work seems to be that of Randall Holmes (pointed out to 
me by Peter Smith) and the paper by Kamareddine, Laan, and Nederpelt 
(Bull. Symb. Logic 8 (2002), 185-245).  They discuss at great length the 
issues involved in formalizing PM, and in particular the type theory in 
PM, which plays a central role but which is not formalized in PM itself.  
It's still not clear to me, though, whether anyone has bothered to go 
through PM theorem by theorem and enter everything in the computer (or 
have students do so).

Tim