Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Show HN: Formalizing Principia Mathematica using Lean

github.com

Post reply on HN
Print view View original

1–10 of 38 posts

Show HN: Formalizing Principia Mathematica using Lean

#1

Post by ndrwnaguib »

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 HN: Formalizing Principia Mathematica using Lean
github.com

Re: Show HN: Formalizing Principia Mathematica using Lean

#6

Post by imglorp »

Jtsummers wrote: post #5
krick wrote: post #3

> 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.

https://www.youtube.com/watch?v=9RD5D4swZfk - Possibly this.

TLDW: Godel's incompleteness theorem is at odds with the goals of Principia.

Re: Show HN: Formalizing Principia Mathematica using Lean

#8

Post by krick »

Jtsummers wrote: post #5
krick wrote: post #3

> 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.

https://www.youtube.com/watch?v=9RD5D4swZfk - Possibly this.

Thanks. It appears, however, that Dyson considers the whole approach a failure (referring to Gödel as a demolisher of it). So while he is saying it about a book, ironically, it seems hardly applicable in this context anymore. Because with this reasoning, any program in Lean (and the Lean programming language itself) should be seen as "a monumental failure".

Re: Show HN: Formalizing Principia Mathematica using Lean

#9

Post by yablak »

imglorp wrote: post #6
Jtsummers wrote: post #5

Earlier quoted context omitted.

https://www.youtube.com/watch?v=9RD5D4swZfk - Possibly this.

TLDW: Godel's incompleteness theorem is at odds with the goals of Principia.

Which is weird because he used the formalism of principia to actually state the theorem, or at least part of it

Re: Show HN: Formalizing Principia Mathematica using Lean

#10

Post by jandrese »

krick wrote: post #8
Jtsummers wrote: post #5

Earlier quoted context omitted.

https://www.youtube.com/watch?v=9RD5D4swZfk - Possibly this.

Thanks. It appears, however, that Dyson considers the whole approach a failure (referring to Gödel as a demolisher of it). So while he is saying it about a book, ironically, it seems hardly applicable in this context anymore. Because with this reasoning, any program in Lean (and the Lean programming language itself) should be seen as "a monumental failure".

This is just my opinion, but reading about Bertrand Russell my impression is that he dedicated his life to Pincipia Mathematica partially because he expected to find God in the foundations of the mathematics, and when that didn't happen it drove him rather insane. And then Gödel shows up and basically knifes him on stage with the Incompleteness Theorm.
Post reply on HN