Show HN: Bertrand Russell's Principia Mathematica in Lean

Summary

Formalizing Bertrand Russell’s Principia Mathematica Using Lean4 This project aims to formalize the first volume of Prof. Bertrand Russell’s Principia Mathematica using the Lean theorem prover. The goal is to ensure that the formalization aligns clearly with the corresponding theorems in the book to avoid confusion (See Metaprogramming =Syll=) Notation Principia Mathematica’s notation (Peano-Russell notation) is exceptionally known for its sophistication that it has a separate entry on the Stanford Encyclopedia of Philosophy (SEP). Also, Prof. Landon Elkind’s Squaring the Circles: a Genealogy of Principia’s Dot Notation explains the notation skillfully. I do not think there is a need to read them, I would like to believe that after reading a few examples of how some formulas were formalized and contrasting them against Prof. Russell’s notation should make it clear. Throughout the formalization, I tried to rigorously follow Prof. Russell’s proof, with no or little added statements from my side, which were only necessary for the formalization but not the logical argument. Should you notice any inaccuracy (even if it does not necessarily falsify the proof), please let me know as I would like to proceed with the same spirit of rigor as Prof. Russell. Before starting this project, I had already found Prof. Elkind’s formalization of the Principia using Coq, which is much mature work than this one. However, I still thought it would be fun to do it using Lean4 (See Remarks). Editing I have included a $\LaTeX$ fragment with each theorem that represents Prof. Russell’s proof. If you use Emacs, I recommend enabling org-preview-latex in the Lean buffer. If you are using VSCode, perhaps a similar experience can be achieved by installing the Better extension. This is how it looked like for me: Notes on the formalization $∗ 1 ⋅ 11$ Prof. Russell repeatedly used *1.11 to indicate the inference of a proposition from another, for example $[(3).(8).∗ 1⋅ 11]$ is the proposition deduce...