New math book rescues landmark topology proof

Re:New math book rescues landmark topology proof by lostmsu on Thursday September 09, 2021 @02:49PM (#28473182)

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.

[ Parent | on HN ]

Re:New math book rescues landmark topology proof by deadbeef57 on Friday September 10, 2021 @08:57AM (#28480849)

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.

[ Parent | on HN ]

Re:New math book rescues landmark topology proof by lostmsu on Friday September 10, 2021 @01:33PM (#28484750)

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

[ Parent | on HN ]