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=)
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).
I have included a
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 Comments extension. This is how it looked like for me:
Prof. Russell repeatedly used *1.11 to indicate the inference of a proposition
from another, for example
proposition (8) and (3). In Lean, this could be analogous to several tactics or
atoms, e.g., <|, simp, etc.
The experience I planned for when reading the formalization is to have the
corresponding text in the Principia included in the same file, only with Prof.
Russell’s proofs replaced with their Lean formalization. F
5 Comments
wanderlust123
What do you think of using something like naproche?
krick
> Although the Principia is thought to be “a monumental failure”, as said by Prof. Freeman Dyson
I'd like some elaboration on that. I failed to find a source.
resters
This is useful to anyone who wants to reason through the proofs constructively and tinker with the approaches. Thank you!
hackandthink
I only see these very initial propositional theorems.
Am I missing something, or has the project only just begun?
https://github.com/ndrwnaguib/principia/blob/main/Principia/…
grandempire
It looks like you just have a few pages written. Is that right?
Which theorem are you trying to prove?