[deadbeef57]

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]

Thanks for pointing that out. This is still magnitudes less things to manually check for correctness than an entire proof.