Show HN: Formalizing Principia Mathematica using Lean • Hacker News Board

Re: Show HN: Formalizing Principia Mathematica using Lean

#31

Post by vixen99 » Sat, Apr 26, 2025, 5:55 AM UTC

psychoslave wrote: post #14

jandrese wrote: post #10

Earlier quoted context omitted.

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.

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 God…

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.

Re: Show HN: Formalizing Principia Mathematica using Lean

#32

Post by dudeinjapan » Sat, Apr 26, 2025, 5:55 AM UTC

StarlaAtNight wrote: post #24

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

Re: Show HN: Formalizing Principia Mathematica using Lean

#33

Post by woolion » Sat, Apr 26, 2025, 8:59 AM UTC

gnulinux wrote: post #13

krick wrote: post #3

> 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 con…

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.

Re: Show HN: Formalizing Principia Mathematica using Lean

#34

Post by looofooo0 » Sat, Apr 26, 2025, 1:02 PM UTC

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.

Re: Show HN: Formalizing Principia Mathematica using Lean

#35

Post by hackandthink » Sat, Apr 26, 2025, 1:42 PM UTC

woolion wrote: post #33

gnulinux wrote: post #13

Earlier quoted context omitted.

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 con…

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 th…

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)

Re: Show HN: Formalizing Principia Mathematica using Lean

#36

Post by gitroom » Sat, Apr 26, 2025, 5:12 PM UTC

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.

Re: Show HN: Formalizing Principia Mathematica using Lean

#37

Post by SkySkimmer » Sat, Apr 26, 2025, 8:42 PM UTC

yuppiemephisto wrote: post #28

meghprkh wrote: post #27

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.

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

Re: Show HN: Formalizing Principia Mathematica using Lean

#38

Post by meghprkh » Sat, Apr 26, 2025, 9:46 PM UTC

yuppiemephisto wrote: post #28

meghprkh wrote: post #27

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.

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.