A mathematician looks at a line in a proof and asks herself ‘is that a correct application of logical inference rules?’ She either spots a violation or gets a feeling that it’s in fact correct. There’s a very high chance she got it right but no mystical state of pure logic that guarantees it.
In this scene, does an automated proof verifier count as a mathematician? I’d agree that there’s still neither a 100% chance of correctness nor a mystical state of pure logic at work here, but calling the process “intuition” still strikes me as very misleading.
But people don’t work al all like automated proof verifiers. You couldn’t feed most mathematical proofs to an automated proof verifier. And even when people fully formalize their proofs, they still rely on a learned and slightly fuzzy ability to assess the correctness of any single step. You can’t run a proof-checking procedure on your brain. (You can emulate running that procedure but then you have to rely on your learned, slightly fuzzy ability to emulate any single step of the computation.)
In this scene, does an automated proof verifier count as a mathematician? I’d agree that there’s still neither a 100% chance of correctness nor a mystical state of pure logic at work here, but calling the process “intuition” still strikes me as very misleading.
But people don’t work al all like automated proof verifiers. You couldn’t feed most mathematical proofs to an automated proof verifier. And even when people fully formalize their proofs, they still rely on a learned and slightly fuzzy ability to assess the correctness of any single step. You can’t run a proof-checking procedure on your brain. (You can emulate running that procedure but then you have to rely on your learned, slightly fuzzy ability to emulate any single step of the computation.)