[FOM] Fwd: Has Principia Mathematic been formally verified

[belinfan at math.gatech.edu]

Automated reasoning in set theory in general has come a long way.   
Among the many people involved
in this endeavor over the years are:  Larry Paulson, Robert Boyer, Art  
Quaife, Norman Megill,
William Farmer and  Peter Andrew.  I too have done some of this work,  
using Otter, but my work uses NBG class theory.  I do not know about  
the PM system specifically, but my impression is that PM does not  
develop mathematics all that far.

N. G. de Bruijn, "Project AUTOMATH" in "To H. B. Curry, Essays on  
Combinatory Logic etc.,"
edited by Seldin and Hindley, reports that D. T. van Daalen, R. P.  
Nederpelt and others
formally checked proofs in set theory back in the 1970s.