[FOM] Fwd: Has Principia Mathematic been formally verified
belinfan at math.gatech.edu
belinfan at math.gatech.edu
Thu Jul 28 12:47:31 EDT 2011
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.
More information about the FOM
mailing list