2 ms·
I understand that you might need a code review for the proof to look nice, but the point of a checked proof is that you don't need a separate code review for co
by lostmsu 5y ago
I understand that you might need a code review for the proof to look nice, but the point of a checked proof is that you don't need a separate code review for correctness. If it checks (sans internal checker issues) - it is correct.
- deadbeef57 5y agoYou still need to check that the definitions are correct. If you define `x^n = 42`, then proving FLT for `n > 2` is really easy. And proof checkers cannot check that you get the definitions right.
- lostmsu 5y agoThanks for pointing that out. This is still magnitudes less things to manually check for correctness than an entire proof.