[HN Gopher] Show HN: Formalizing Principia Mathematica using Lean
___________________________________________________________________
Show HN: Formalizing Principia Mathematica using Lean
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
Author : ndrwnaguib
Score : 70 points
Date : 2025-04-25 18:49 UTC (4 hours ago)
(HTM) web link (github.com)
(TXT) w3m dump (github.com)
| wanderlust123 wrote:
| What do you think of using something like naproche?
| ndrwnaguib wrote:
| I have not used `naproche` before; thanks for the suggestion. I
| will try several propositions and see what do I get!
| krick wrote:
| > 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.
| Jtsummers wrote:
| https://www.youtube.com/watch?v=9RD5D4swZfk - Possibly this.
| imglorp wrote:
| TLDW: Godel's incompleteness theorem is at odds with the
| goals of Principia.
| yablak wrote:
| Which is weird because he used the formalism of principia
| to actually state the theorem, or at least part of it
| grandempire wrote:
| Russel builds a logical system - it just can't ground
| mathematics. Godel's paper is about the system in Russels
| book.
| mikrl wrote:
| 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?
| krick wrote:
| Thanks. It appears, however, that Dyson considers the whole
| approach a failure (referring to Godel 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".
| jandrese wrote:
| 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 Godel shows up
| and basically knifes him on stage with the Incompleteness
| Theorm.
| krick wrote:
| I would like if you could refer me to that reading as
| well. I really know nothing about, uh, any of that, so I
| cannot judge. But your description strikes me as rather
| weird: "dedicating his life" seems a bit dramatic, since
| Principia is a pretty early work of his. He was active
| for 50-60 more years since he must have been "driven
| insane", as you say. Most of his famous works were
| written after that. Also, all of famous results of Godel
| were after Russell finished with Principia. Not that he
| ever finished, but given the fact Second Edition was 15
| years after the First one, and mostly contained
| relatively minor fixes... it seems only logical to
| conclude that he wasn't pursuing the topic after the
| first publication, basically, ever since realizing how
| big of a task would it be to try and formalize all of
| math like that.
| psychoslave wrote:
| I don't know what you red about Russell, but in my own
| readings he has always been presented as a fervent
| atheist, so except with a far stretched interpretation of
| "neutral monism" as some form of gnoseologic divinity,
| it's hard to imagine such a character looking for any
| god.
|
| Also Russel himself ruined the cathedral of Frege with
| its eponymous paradox, he was clearly among the best to
| understand how a thing like Godel's incompleteness
| theorem could come along the way.
|
| And for his relation to madness, his personal life have
| been felt with many turmoil from an early age. If
| anything it seems that mathematics saved him, preventing
| his early desire for suicide.
|
| https://plato.stanford.edu/entries/neutral-monism/
|
| https://en.wikipedia.org/wiki/Copleston%E2%80%93Russell_d
| eba...
| davidrjones1977 wrote:
| I believe you are thinking of Cantor, regarding God and
| subsequent insanity. And it was Russell who knifed Frege.
| :-)
| gnulinux wrote:
| Principia was written during the naive Logicist era of
| philosophy of mathematics that couldn't foresee serious
| foundational decidability issues in logic like Godel's
| incompleteness theorems, or the Halting Problem.
| Formalism/Platonism and Constructivism are two streams that
| came out of Logicism as a way to fix logical issues, and
| they're (very roughly speaking) the philosophical basis of
| classical mathematics and constructive mathematics today.
|
| The way formalists (mainstream mathematical community) dealt
| with the foundational issues was to study them very closely and
| precisely so that they can ignore it as much as possible. The
| philosophical justification is that even though a statement P
| is undecidable, ultimately speaking, within the universe of
| mathematical truth, it's either true or false and nothing else,
| even though we may not be able to construct a proof of either.
|
| Constructivists on the other hand took the opposite approach,
| they equated mathematical truth with provability, therefore
| undecidable statements P are such that they're neither true nor
| false, constructively. This means Aristotle's law of excluded
| middle (for any statement P, P or (not P)) no longer holds and
| therefore constructivists had to rebuild mathematics from a
| different logical basis.
|
| The issue with Principia is it doesn't know how to deal with
| issues like this, so the way it lays out mathematics no longer
| makes total sense, and its goals (mathematical program) are
| found to be impossible.
|
| Note: this is an extreme oversimplification. I recommend
| Stanford Encyclopedia of Philosophy for a more detailed
| overview. E.g. https://plato.stanford.edu/entries/hilbert-
| program/
| resters wrote:
| This is useful to anyone who wants to reason through the proofs
| constructively and tinker with the approaches. Thank you!
| ndrwnaguib wrote:
| Thank you!
| hackandthink wrote:
| 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 wrote:
| 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.
| grandempire wrote:
| It looks like you just have a few pages written. Is that right?
|
| Which theorem are you trying to prove?
| ndrwnaguib wrote:
| Yes; the goal is to finish the first volume. I am particularly
| looking forward to formalizing the well-known 1+1 proof.
| grandempire wrote:
| My understanding is the first bit follows first order logic
| fairly close but then diverges as Russel builds different
| classes of sets etc, do you have line of sight of how it's
| going to translate?
___________________________________________________________________
(page generated 2025-04-25 23:00 UTC)