What do you think of using something like naproche?

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

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

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

Which theorem are you trying to prove?

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