[FOM] Has Principia Mathematica been formally verified?

[Timothy Y. Chow]

I have a vague recollection that I once saw a paper or perhaps a master's 
thesis that attempted to verify all the proofs in Russell and Whitehead's 
PM mechanically with a computer.  Does anybody else know of such a 
documented effort?

Though I've never made a serious effort to read PM in detail, my 
impression is that their approach was not what we would today consider 
purely formal, in the sense of providing purely syntactic rules for 
everything.  Still, it would seem that formalizing PM and putting it into 
a computer should be a relatively straightforward, if tedious, exercise.

If a full verification of PM doesn't exist, then I'm wondering if anyone 
has at least programmed up a modern formalist description of the system.

I'm aware that Newell, Simon, and Shaw wrote a program in the 1950's 
called Logic Theorist that was designed to *find* proofs of PM theorems.  
Though this isn't exactly what I'm asking about, it's close.  
Unfortunately I haven't been able to find too many details of how Logic 
Theorist chose to formalize things, since their paper was apparently 
rejected for publication.

Tim