Show HN: Formalizing Principia Mathematica using Lean

ndrwnaguib | 188 points

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!

meghprkh | 14 days ago

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

resters | 14 days 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/...

hackandthink | 14 days 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.

looofooo0 | 13 days 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?

ks2048 | 14 days ago

What do you think of using something like naproche?

wanderlust123 | 14 days ago

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

Which theorem are you trying to prove?

grandempire | 14 days 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.

gitroom | 13 days 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.

krick | 14 days ago
StarlaAtNight | 14 days ago