Formalizing Russell's Principia Mathematica in Lean4

This project formalizes the first volume of Bertrand Russell's Principia Mathematica using the Lean theorem prover. The goal is to ensure the formalization aligns with the book's theorems, avoiding confusion. The project rigorously follows Russell's proofs, minimizing added statements. A new tactic, `Syll`, handling a more general form of syllogism, was created. While Principia Mathematica is considered a 'monumental failure', the author found the formalization process enriching.