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 Stanf...