3 ms·
if I'm reading correctly, they've already done the Coq and it verifies. https://github.com/LogicalAtomist/principia/blob/master/PL.v https://github.com/Logical
by Palomides 5y ago
if I'm reading correctly, they've already done the Coq and it verifies.
https://github.com/LogicalAtomist/principia/blob/master/PL.v https://github.com/LogicalAtomist/principia/blob/master/PL.v
- hcs 5y agoWhat's up there now is "only" up to *5. They announced that back in February and it sounds like there's been a lot more work since (though perhaps mostly reorganization and typesetting). Volume I goes up to *97, and the fragment that's commonly printed is "Principia Mathematica to *56".