3 ms·
You 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
by deadbeef57 5y ago
You 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.