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!

Show 1 reply

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

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

Show 1 reply

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.

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?

What do you think of using something like naproche? Show 1 reply

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

Which theorem are you trying to prove?

Show 1 reply

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.

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

Show 3 replies

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