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!
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.
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.
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.
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!
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.
This is useful to anyone who wants to reason through the proofs constructively and tinker with the approaches. Thank you!
Thank you!
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/...
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.
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?
It looks like you just have a few pages written. Is that right?
Which theorem are you trying to prove?
Yes; the goal is to finish the first volume. I am particularly looking forward to formalizing the well-known 1+1 proof.
What do you think of using something like naproche?
I have not used `naproche` before; thanks for the suggestion. I will try several propositions and see what do I get!
> 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.
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://www.youtube.com/watch?v=9RD5D4swZfk - Possibly this.
When I saw “Lean” I thought https://en.m.wikipedia.org/wiki/Lean_manufacturing
I thought purple drank https://en.wikipedia.org/wiki/Lean_(drug) Always seemed odd they would name a proof assistant language after cough syrup