Proofs In Math: What’s The Point?
Tyler Cowen pointed me to an article on automated theorem proving. Namely, a computer “has solved the longstanding Erdős discrepancy problem!” This would not be such a big deal, except the 13 gigabyte proof is too complicated for anyone to understand.
So, of course, the Boeotians are in rare form as the clack of keyboards fills the metaphorical air in an attempt to sate the internet’s endless appetite for stupidity. Or: people are saying some really dumb stuff.
The discussions tend to anchor around trust. Can we trust the computer? What if there was a bug in the software? Gil Kalai, a math professor at the Hebrew University of Jerusalem, said, “I’m not concerned by the fact that no human mathematician can check this, because we can check it with other computer approaches.”
The mistake here is to assume that mathematics is about proof. It’s not. Proof is a means to producing insight, and a proof that no one can understand is close to worthless.
But don’t listen to me. Take it from Fields medalist Bill Thurston. He wrote a paper “On Proof and Progress in Mathematics.” It has profoundly influenced my ideas about what intellectual enterprise and mathematics particularly are about.
We are not trying to meet some abstract production quota of definitions, theorems and proofs. The measure of our success is whether what we do enables people to understand and think more clearly and effectively about mathematics.
…
In not too many years, I expect that we will have interactive computer programs that can help people compile significant chunks of formally complete and correct mathematics (based on a few perhaps shaky but at least explicit assumptions), and that they will become part of the standard mathematician’s working environment. However, we should recognize that the humanly understandable and humanly checkable proofs that we actually do are what is most important to us, and that they are quite different from formal proofs.
…
When I started working on foliations, I had the conception that what people wanted was to know the answers. I thought that what they sought was a collection of powerful proven theorems that might be applied to answer further mathematical questions. But that’s only one part of the story. More than the knowledge, people want personal understanding.
Or as Richard Hamming put it, “The purpose of computing is insight, not numbers.”