←back to thread

Show HN: Formalizing Principia Mathematica using Lean

(github.com)
188 points ndrwnaguib | 3 comments | 25 Apr 25 18:49 UTC | HN request time: 0.628s | source

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.

https://ndrwnaguib.com/principia/

https://github.com/ndrwnaguib/principia

Show context
meghprkh ◴[26 Apr 25 02:45 UTC] No.43800460[source]▶
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!

replies(1): >>43800780 #
1. yuppiemephisto ◴[26 Apr 25 03:49 UTC] No.43800780[source]▶
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.

replies(2): >>43807018 #>>43807483 #
2. SkySkimmer ◴[26 Apr 25 20:42 UTC] No.43807018[source]▶
>Lean is also a lot faster.

What do you base that on? I don't think I've seen a performance comparison but I'm not great at internet searches.

3. meghprkh ◴[26 Apr 25 21:46 UTC] No.43807483[source]▶
No specific motivation tbh. I did the number theory game on the recommendation of a friend and found it fun. Made me think.

What does the real programming language part help in? Developing tactics? Or is it because even when you are typing the "math parts" it corresponds to a real programming language giving you a nicer mental model?

Because from what I understand Rocq too has Gallina or something right?

I guess my other point is Rocq seems to have a lot of textbooks too so I was wondering which one to read about when I get some more time - Rocq or Lean.