Comment by sergevar
14 hours ago
Interestingly, there was a Show HN last year formalizing PM in Lean (https://www.principiarewrite.com) verified all 189 propositional logic theorems (sections 1-5) in Coq against the original proof sketches
14 hours ago
Interestingly, there was a Show HN last year formalizing PM in Lean (https://www.principiarewrite.com) verified all 189 propositional logic theorems (sections 1-5) in Coq against the original proof sketches
I believe the Principia Rewrite is at https://principia-rewrite.org/.
Yep, thanks!