Hacker Remix
Show HN: Formalizing Principia Mathematica using Lean
152 points by ndrwnaguib 19 hours ago | 31 comments
This project aims to formalize the first volume of Prof. Bertrand Russell’s Principia Mathematica using the Lean theorem prover. 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 rigour. Before starting this project, I had already found Prof. Elkind’s formalization of the Principia using Rocq (formerly Coq), which is much mature work than this one. However, I still thought it would be fun to do it using Lean4.
looofooo0 1 hour ago
Nice, really great work. How did you get into lean?
Few style Remarks: I personally would not call them Prof. Or Dr. In formal English that would be the latter. But the name of them stands for itself.
meghprkh 11 hours ago
What is the real difference between rocq vs lean? Alternatively, what is your motivation to do this in lean as compared to playing around with the rocq one if it exists?
I recently completed the natural number lean game and found it pretty fun, and would like to learn more about the differences between the two. Thanks!
yuppiemephisto 10 hours ago
I don’t know about their motivation, but I would say mine is that Lean is a real programming language. Coq is not really meant for “prosaic” programming, more’s the pity.
Lean is also a lot faster.
resters 19 hours ago
This is useful to anyone who wants to reason through the proofs constructively and tinker with the approaches. Thank you!
ndrwnaguib 17 hours ago
Thank you!
hackandthink 17 hours ago
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/...
ndrwnaguib 17 hours ago
You're not missing something. The project begun several months ago (I had to pause while I was writing my thesis). I resumed working on it recently.