←back to thread

Show HN: Formalizing Principia Mathematica using Lean

(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://ndrwnaguib.com/principia/

https://github.com/ndrwnaguib/principia

Show context
krick ◴[25 Apr 25 19:13 UTC] No.43797518[source]▶
> 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.

replies(3): >>43797657 #>>43798512 #>>43800892 #
Jtsummers ◴[25 Apr 25 19:26 UTC] No.43797657[source]▶
https://www.youtube.com/watch?v=9RD5D4swZfk - Possibly this.
replies(2): >>43797812 #>>43797894 #
imglorp ◴[25 Apr 25 19:42 UTC] No.43797812[source]▶
TLDW: Godel's incompleteness theorem is at odds with the goals of Principia.
replies(3): >>43797837 #>>43797935 #>>43798256 #
mikrl ◴[25 Apr 25 20:35 UTC] No.43798256[source]▶
I remember my Java IDE in undergrad warned me about an infinite loop, and this was before I learned about the diagonalization proof of the non-computability of the halting problem, one of my favourite proofs ever. The fact that not all programs and inputs can be shown to halt did not stop the engineer who wrote that guardrail for the IDE.

Surely the principia and similar efforts will still yield useful results even if they cannot necessarily prove every true statement from the axioms?

replies(1): >>43800322 #
1. jhanschoo ◴[26 Apr 25 02:13 UTC] No.43800322{3}[source]▶
Yes, you can't prove important properties of the class of all programs, but you can prove properties of smaller, limited classes of programs that you are interested in.

So the Java IDE had been able to recognize an infinite loop of the kind you wrote by an algorithm, that can be proven to be correct for a limited class.

On the other hand, you can loop infinitely deciding to exit on the return value of opaque calls to some entity external to your analyzer, and your IDE shouldn't be able to catch that.

replies(1): >>43801244 #
2. ◴[26 Apr 25 05:49 UTC] No.43801244[source]▶