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.)