3 ms·
I had assumed this had already been done, if not in Coq then in some machine formalization, interesting to see it being tackled. Is there a decent chance they'l
by hcs 5y ago
I had assumed this had already been done, if not in Coq then in some machine formalization, interesting to see it being tackled. Is there a decent chance they'll find some of the later proofs not just missing a step but actually wrong? Or has this happened already?
Edit: I may have been thinking of various attempts to prove the theorems by other (usually AI) means, as mentioned on the page:
> This improves significantly on the earlier computer verification work of Allen Newell et al., Hao Wang, and Daniel O’Leary. In all three cases, either some theorems were not verified or their proofs were not reconstructed according to Principia’s proof sketches.
- Palomides 5y agoif 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".