5 ms·

Show HN: Formalizing Principia Mathematica using Lean

188 points by ndrwnaguib 1y ago

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

wanderlust123 1y ago
What do you think of using something like naproche?
- ndrwnaguib 1y ago
  I have not used `naproche` before; thanks for the suggestion. I will try several propositions and see what do I get!
krick 1y 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.
- Jtsummers 1y ago
  https://www.youtube.com/watch?v=9RD5D4swZfk https://www.youtube.com/watch?v=9RD5D4swZfk - Possibly this.
  - imglorp 1y ago
    TLDW: Godel's incompleteness theorem is at odds with the goals of Principia.
    - deleted 1y ago
      [deleted]
    - yablak 1y ago
      Which is weird because he used the formalism of principia to actually state the theorem, or at least part of it
      - grandempire 1y ago
        Russel builds a logical system - it just can’t ground mathematics. Gödel’s paper is about the system in Russels book.
    - mikrl 1y 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?
      - jhanschoo 1y ago
        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.
- gnulinux 1y 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/ https://plato.stanford.edu/entries/hilbert-program/
  - woolion 1y ago
    Nobody argues about the result of an addition because the computation is mechanistically verifiable. Same with statements that are properly formalized in logic. The goal was to have the same for all of mathematics. So incompleteness is not a problem per se -- even if it shook people so much at the time (because proof theory always work within a given system). Incompleteness is the battery ram that is used to break the walls of common sense. If incompleteness isn't the killer of the Hilbert program, what is? The axiom of choice and the continuum hypothesis. Both lack any form of naturalness that would prevent any philosophical arguing. Worse, not accepting them also do. There is such a wealth of intuitionistically absurd results implied by these systems -- most famously, there is the joke that “The axiom of choice is obviously true, the well-ordering principle obviously false, and who can tell about Zorn's lemma?”, when these 3 statements are _logically_ equivalent. So, we're back to a mathematical form of epistemological anarchism; there is no universal axiomatic basis for doing mathematics; any justification for the use of one has to be found externally to mathematics.
- deleted 1y ago
  [deleted]
resters 1y ago
This is useful to anyone who wants to reason through the proofs constructively and tinker with the approaches. Thank you!
- ndrwnaguib 1y ago
  Thank you!
hackandthink 1y ago
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/PartI/SectionA/primitive_ideas_and_propositions.lean https://github.com/ndrwnaguib/principia/blob/main/Principia/...
- ndrwnaguib 1y ago
  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 1y ago
It looks like you just have a few pages written. Is that right? Which theorem are you trying to prove?
- ndrwnaguib 1y ago
  Yes; the goal is to finish the first volume. I am particularly looking forward to formalizing the well-known 1+1 proof.
  - grandempire 1y 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?
StarlaAtNight 1y ago
When I saw “Lean” I thought https://en.m.wikipedia.org/wiki/Lean_manufacturing https://en.m.wikipedia.org/wiki/Lean_manufacturing
- dudeinjapan 1y ago
  I thought purple drank https://en.wikipedia.org/wiki/Lean_(drug) https://en.wikipedia.org/wiki/Lean_(drug) Always seemed odd they would name a proof assistant language after cough syrup
ks2048 1y 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?
meghprkh 1y 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!
- yuppiemephisto 1y 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.
  - SkySkimmer 1y ago
    >Lean is also a lot faster. What do you base that on? I don't think I've seen a performance comparison but I'm not great at internet searches.
  - meghprkh 1y ago
    No specific motivation tbh. I did the number theory game on the recommendation of a friend and found it fun. Made me think. What does the real programming language part help in? Developing tactics? Or is it because even when you are typing the "math parts" it corresponds to a real programming language giving you a nicer mental model? Because from what I understand Rocq too has Gallina or something right? I guess my other point is Rocq seems to have a lot of textbooks too so I was wondering which one to read about when I get some more time - Rocq or Lean.
looofooo0 1y ago
Nice, really great work. How did you get into lean? Few style Remarks: I personally would not call them Prof. Or Dr. In formal English that would be the latter. But the name of them stands for itself.
gitroom 1y ago
Bruh, doing Principia in Lean is next level. Always blows my mind how far formal math stuff has come lately, but yeah, I barely got through the Lean natural numbers game myself lol.

188 points by ndrwnaguib 1y ago

wanderlust123 1y ago

What do you think of using something like naproche?

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

krick 1y 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.

Jtsummers 1y ago
https://www.youtube.com/watch?v=9RD5D4swZfk https://www.youtube.com/watch?v=9RD5D4swZfk - Possibly this.
- imglorp 1y ago
  TLDW: Godel's incompleteness theorem is at odds with the goals of Principia.
  - deleted 1y ago
    [deleted]
  - yablak 1y ago
    Which is weird because he used the formalism of principia to actually state the theorem, or at least part of it
    - grandempire 1y ago
      Russel builds a logical system - it just can’t ground mathematics. Gödel’s paper is about the system in Russels book.
  - mikrl 1y 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?
    - jhanschoo 1y ago
      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.
gnulinux 1y 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/ https://plato.stanford.edu/entries/hilbert-program/
- woolion 1y ago
  Nobody argues about the result of an addition because the computation is mechanistically verifiable. Same with statements that are properly formalized in logic. The goal was to have the same for all of mathematics. So incompleteness is not a problem per se -- even if it shook people so much at the time (because proof theory always work within a given system). Incompleteness is the battery ram that is used to break the walls of common sense. If incompleteness isn't the killer of the Hilbert program, what is? The axiom of choice and the continuum hypothesis. Both lack any form of naturalness that would prevent any philosophical arguing. Worse, not accepting them also do. There is such a wealth of intuitionistically absurd results implied by these systems -- most famously, there is the joke that “The axiom of choice is obviously true, the well-ordering principle obviously false, and who can tell about Zorn's lemma?”, when these 3 statements are _logically_ equivalent. So, we're back to a mathematical form of epistemological anarchism; there is no universal axiomatic basis for doing mathematics; any justification for the use of one has to be found externally to mathematics.
deleted 1y ago
[deleted]

resters 1y ago

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

ndrwnaguib 1y ago
Thank you!

hackandthink 1y ago

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/PartI/SectionA/primitive_ideas_and_propositions.lean https://github.com/ndrwnaguib/principia/blob/main/Principia/...

ndrwnaguib 1y ago
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 1y ago

It looks like you just have a few pages written. Is that right? Which theorem are you trying to prove?

ndrwnaguib 1y ago
Yes; the goal is to finish the first volume. I am particularly looking forward to formalizing the well-known 1+1 proof.
- grandempire 1y 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?

StarlaAtNight 1y ago

When I saw “Lean” I thought https://en.m.wikipedia.org/wiki/Lean_manufacturing https://en.m.wikipedia.org/wiki/Lean_manufacturing

dudeinjapan 1y ago
I thought purple drank https://en.wikipedia.org/wiki/Lean_(drug) https://en.wikipedia.org/wiki/Lean_(drug) Always seemed odd they would name a proof assistant language after cough syrup

ks2048 1y 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?

meghprkh 1y 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!

yuppiemephisto 1y 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.
- SkySkimmer 1y ago
  >Lean is also a lot faster. What do you base that on? I don't think I've seen a performance comparison but I'm not great at internet searches.
- meghprkh 1y ago
  No specific motivation tbh. I did the number theory game on the recommendation of a friend and found it fun. Made me think. What does the real programming language part help in? Developing tactics? Or is it because even when you are typing the "math parts" it corresponds to a real programming language giving you a nicer mental model? Because from what I understand Rocq too has Gallina or something right? I guess my other point is Rocq seems to have a lot of textbooks too so I was wondering which one to read about when I get some more time - Rocq or Lean.

looofooo0 1y ago

Nice, really great work. How did you get into lean? Few style Remarks: I personally would not call them Prof. Or Dr. In formal English that would be the latter. But the name of them stands for itself.

gitroom 1y ago

Bruh, doing Principia in Lean is next level. Always blows my mind how far formal math stuff has come lately, but yeah, I barely got through the Lean natural numbers game myself lol.