Show HN: Formalizing Principia Mathematica using Lean

(github.com)

132 points by ndrwnaguib 14 hours ago

31 comments

View on Hacker News

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

meghprkh 6 hours ago

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!

Reply View 1 reply
  • yuppiemephisto 5 hours ago

    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.

    Reply View 0 replies
resters 13 hours ago

This is useful to anyone who wants to reason through the proofs constructively and tinker with the approaches. Thank you!

Reply View 1 reply
ks2048 6 hours ago

This is cool and I looked into this many years ago (using MetaMath).

Sorry if this is obvious in one of the links, but does there exist a high quality “OCR-ed” version of the original text?

Reply View 0 replies
grandempire 11 hours ago

It looks like you just have a few pages written. Is that right?

Which theorem are you trying to prove?

Reply View 2 replies
  • ndrwnaguib 11 hours ago

    Yes; the goal is to finish the first volume. I am particularly looking forward to formalizing the well-known 1+1 proof.

    Reply View 1 reply
    • grandempire 11 hours ago

      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?

      Reply View 0 replies
wanderlust123 14 hours ago

What do you think of using something like naproche?

Reply View 1 reply
  • ndrwnaguib 11 hours ago

    I have not used `naproche` before; thanks for the suggestion. I will try several propositions and see what do I get!

    Reply View 0 replies
krick 13 hours ago

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

Reply View 16 replies
  • gnulinux 12 hours ago

    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/

    Reply View 0 replies
  • [removed] 4 hours ago
    [deleted]
    Reply View 0 replies
  • Jtsummers 13 hours ago

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

    Reply View 13 replies
    • imglorp 13 hours ago

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

      Reply View 6 replies
      • mikrl 12 hours ago

        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?

        Reply View 2 replies
      • yablak 13 hours ago

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

        Reply View 1 reply
        • grandempire 11 hours ago

          Russel builds a logical system - it just can’t ground mathematics. Gödel’s paper is about the system in Russels book.

          Reply View 0 replies
      • [removed] 13 hours ago
        [deleted]
        Reply View 0 replies
    • krick 13 hours ago

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

      Reply View 5 replies
      • jandrese 13 hours ago

        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.

        Reply View 4 replies