_______ __ _______
| | |.---.-..----.| |--..-----..----. | | |.-----..--.--.--..-----.
| || _ || __|| < | -__|| _| | || -__|| | | ||__ --|
|___|___||___._||____||__|__||_____||__| |__|____||_____||________||_____|
on Gopher (inofficial)
URI Visit Hacker News on the Web
COMMENT PAGE FOR:
URI Show HN: Formalizing Principia Mathematica using Lean
gitroom wrote 21 hours 47 min 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.
looofooo0 wrote 1 day 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.
meghprkh wrote 1 day 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 wrote 1 day 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.
meghprkh wrote 17 hours 13 min 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.
SkySkimmer wrote 18 hours 17 min 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.
ks2048 wrote 1 day 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?
StarlaAtNight wrote 1 day ago:
When I saw âLeanâ I thought
URI [1]: https://en.m.wikipedia.org/wiki/Lean_manufacturing
dudeinjapan wrote 1 day ago:
I thought purple drank [1] Always seemed odd they would name a proof
assistant language after cough syrup
URI [1]: https://en.wikipedia.org/wiki/Lean_(drug)
grandempire wrote 1 day ago:
It looks like you just have a few pages written. Is that right?
Which theorem are you trying to prove?
ndrwnaguib wrote 1 day ago:
Yes; the goal is to finish the first volume. I am particularly
looking forward to formalizing the well-known 1+1 proof.
grandempire wrote 1 day 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?
hackandthink wrote 1 day ago:
I only see these very initial propositional theorems.
Am I missing something, or has the project only just begun?
URI [1]: https://github.com/ndrwnaguib/principia/blob/main/Principia/Pa...
ndrwnaguib wrote 1 day 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.
resters wrote 1 day ago:
This is useful to anyone who wants to reason through the proofs
constructively and tinker with the approaches. Thank you!
ndrwnaguib wrote 1 day ago:
Thank you!
krick wrote 1 day 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.
gnulinux wrote 1 day 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.
URI [1]: https://plato.stanford.edu/entries/hilbert-program/
woolion wrote 1 day 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.
hackandthink wrote 1 day ago:
I would add that there is/was a certain desire for categorical
theories.
"In mathematical logic, a theory is categorical if it has exactly
one model (up to isomorphism)."
(categorical is stronger than complete)
Jtsummers wrote 1 day ago:
[1] - Possibly this.
URI [1]: https://www.youtube.com/watch?v=9RD5D4swZfk
krick wrote 1 day 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".
jandrese wrote 1 day 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.
davidrjones1977 wrote 1 day ago:
I believe you are thinking of Cantor, regarding God and
subsequent insanity.
And it was Russell who knifed Frege. :-)
psychoslave wrote 1 day ago:
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. [1]
URI [1]: https://plato.stanford.edu/entries/neutral-monism/
URI [2]: https://en.wikipedia.org/wiki/Copleston%E2%80%93Russel...
vixen99 wrote 1 day ago:
Incidentally his co-author AN Whitehead was not an atheist as
a reading of Science and the Modern World (from lectures at
Harvard in 1926 I think.) makes clear.
krick wrote 1 day ago:
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
Gödel 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.
imglorp wrote 1 day ago:
TLDW: Godel's incompleteness theorem is at odds with the goals of
Principia.
mikrl wrote 1 day 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 wrote 1 day 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.
yablak wrote 1 day ago:
Which is weird because he used the formalism of principia to
actually state the theorem, or at least part of it
grandempire wrote 1 day ago:
Russel builds a logical system - it just canât ground
mathematics. Gödelâs paper is about the system in Russels
book.
wanderlust123 wrote 1 day ago:
What do you think of using something like naproche?
ndrwnaguib wrote 1 day ago:
I have not used `naproche` before; thanks for the suggestion. I will
try several propositions and see what do I get!
DIR <- back to front page