This just in, and just time for the new year:
- the propositional logic of “Principia Mathematica” has been fully computer-checked in Coq (the source code can also be viewed as a PDF)
- the first 132 pages of PM have been typeset in LaTeX and is also available in a pretty PDF
- a TeX package is now available for typesetting all symbols in PM Volume I
A Github repository has the source code in Coq and TeX, plus some PDFs for ease of viewing by non-Coq or non-TeX users: https://github.com/LogicalAtomist/principia.
More updates on the Principia Rewrite Project will be posted to the repository once the quantification theory is computer-checked and typeset. Until then, happy New Year!