Hacker News Reader

Because programmatically checked proofs don't work the way you think they do.

And even programatically checked proofs are still programs. And programs still need code review.

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.

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.

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

Reply on news.ycombinator.com