Catching up with Tim Gowers’s blog, I notice he makes some interesting remarks in passing about the idea of a proof. He’d initiated/co-ordinated a “polymath” project — a collaborative all-comers group effort trying to find a combinatorial proof of a result in Ramsey theory previously known from a proof in ergodic theory. After hundreds on contributions, but of course before any attempt to put the bits and pieces together into a conventionally written-up proof, Gowers says “I am basically sure that the problem is solved (though not in the way originally envisaged).”
Why do I feel so confident that what we have now is right, especially given that another attempt that seemed quite convincing ended up collapsing? Partly because it’s got what you want from a correct proof: not just some calculations that magically manage not to go wrong, but higher-level explanations backed up by fairly easy calculations, a new understanding of other situations where closely analogous arguments definitely work, and so on. And it seems that all the participants share the feeling that the argument is “robust” in the right way.
So, interestingly, getting a “correct” proof in his sense involves more than getting a proof in the austere logician’s sense of a correct proof as just (“magically”) getting out the desired result without logical gaps — it goes with explanations and understanding.
Let’s not fuss about terminology. It undoubtedly is the case that a notion of a correct proof in something like Gowers’s sense functions centrally in mathematicians’ thinking. But how good are the attempts by philosophers of mathematics to elucidate this notion?