(github.com)

173 points ndrwnaguib | 2 comments | 25 Apr 25 18:49 UTC | HN request time: 0s | 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://github.com/ndrwnaguib/principia

1. meghprkh ◴[26 Apr 25 02:45 UTC] No.43800460[source]▶

>>43797256 (OP) #

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 #

2. yuppiemephisto ◴[26 Apr 25 03:49 UTC] No.43800780[source]▶

>>43800460 (TP) #

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.

↑

Show HN: Formalizing Principia Mathematica using Lean