<- Back
Comments (28)
- meghprkhWhat 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!
- restersThis is useful to anyone who wants to reason through the proofs constructively and tinker with the approaches. Thank you!
- ks2048This 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?
- hackandthinkI 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/...
- grandempireIt looks like you just have a few pages written. Is that right?Which theorem are you trying to prove?
- wanderlust123What do you think of using something like naproche?
- krick> Although the Principia is thought to be “a monumental failure”, as said by Prof. Freeman DysonI'd like some elaboration on that. I failed to find a source.
- StarlaAtNightWhen I saw “Lean” I thought https://en.m.wikipedia.org/wiki/Lean_manufacturing