Hacker News new | ask | show | jobs
by SkiFire13 1025 days ago
The thing about proof checkers is that they won't accept invalid proofs (assuming their internal axioms are consistents...), so if you make a mistake there it will simply reject your proof. The only place where it won't catch some mistakes is in proposition you want to prove, because the only way for it to know what you want to prove if for you to tell it, but that's much easier to humanly verify.