Not a lot gets written in the general press about foundational issues in mathematics, but this afternoon I found myself talking to a journalist about the subject of certainty in mathematics.
It turned out to be a pretty interesting conversation, so I thought I’d write here about a few things that came up.
Mathematics likes to think of itself as a very certainty-based business. If you’ve “proved something mathematically”, then it’s supposed to just be true. No ifs or buts. Complete certainty.
But in practice that’s not quite how it works—at least the way mathematics has traditionally been done. Because in reality a mathematical proof of the kind people publish in papers is something much more social. It’s a vehicle for convincing other humans—one’s fellow mathematicians—that something is true.
There’ve been a few million mathematical proofs published over the past century or so. Essentially all of them are written in a kind of human-compatible mixture of mathematical formalism and ordinary natural language.
They’re intended for human consumption. For people to read, and process. The best of them aren’t just arguments for some particular theorem. Instead they’re expositions that illuminate some whole mathematical structure.
But inevitably they require effort to read. It’s not just a mechanical matter. Instead, every reader of every proof has to somehow map what the proof is saying into their particular patterns of thought. So that they can personally be convinced that the proof is true.
And of course, in practice, proofs written by humans have bugs. Somewhere between the imprecision of ordinary language, and the difficulty of really thinking through every possible eventuality, it’s almost inevitable that any long proof that’s been published isn’t perfect. And even with an army of people to check it, not every bug will be found.
So how do computers—and Mathematica change this picture?
