Thread by @wtgowers

Several people I follow have retweeted this link to an excellent Mathoverflow answer about robustness of mathematical proofs. Here's a quick thread on the topic. The short version of Mike Shulman's answer is that mathematical proofs are more to do with ideas and understanding 1/

https://twitter.com/HigherGeometer/status/1163141811600101377

than with formal verification. I agree with that analysis, but it leaves various very interesting questions not fully answered. I wish I could answer them myself, but the best I can do for now is offer a few observations. 2/

I think the two most obvious questions are (1) What are "ideas" and "understanding"? and (2) What is it about mathematical proofs that allows them to be "robust" and "fault tolerant"? I'll have more to say about the second. 3/

An useful thing to bear in mind is that not all mathematical proofs are robust. This is nicely illustrated by taking well-known NP-complete problems in graph theory and looking at random instances with various different edge probabilities. 4/

For example, let's take the problem of finding a Hamilton cycle -- that is, a cycle that visits every vertex of a graph exactly once. And let's suppose that we take a random graph with edge probability p. If p is large, then finding a Hamilton cycle is easy: you just ... 5/

keep on visiting a vertex you haven't yet visited, and you won't get stuck till right near the end, at which point you make a few small adjustments and find your cycle. If p is small but a Hamilton cycle is "planted" in the graph, then it will be easy to find for ... 6/

more or less the opposite reason: at each step you will be so short of options that your move is more or less forced. But there is a sweet spot in between where there are lots of tempting long paths, only a tiny proportion of which turn into Hamilton cycles, and ... 7/

few enough edges that if you get near the end and fail to find a cycle, you basically have to junk what you've done and start again. Or if you think you've found a Hamilton cycle and suddenly notice you've missed out a vertex, this near miss will be of no help. 8/

That last possibility is an example of a fragile, non-robust proof that the graph contains a Hamilton cycle: it is wrong, and it can't be locally corrected, as it could in the dense case.

It's clear that at least one way in which a proof can be robust is if it is "locally correctable", and one very good way for a proof to be locally correctable is if it is modular -- that is, made up of lots of small pieces that can be put together. 10/

Talking of modularity of proofs, I recently had my attention drawn to this article, which I am intending to read soon. 11/

andrew.cmu.edu/user/avigad/Pa…

A word of caution though. I once found a nicely modular but wrong proof of Szemerédi's theorem. The mistake was nicely confined to one lemma, but unfortunately that lemma was false, as was the statement I needed it for, as was the statement I needed *that* for. 12/

Even then the modularity was useful though, as it made it very clear what still needed to be done, and a couple of years down the line I eventually got there -- though with a much less simple argument. 13/

So why is so much mathematics robust? The best I can do here is to say that a huge process of selection goes on. The fact that some funny graph happens to contain a Hamilton cycle that can only be found after a huge brute-force search is something we tend to dislike, 14/

saying that there aren't any interesting ideas. So I think that robustness, modularity, ideas, understanding, etc. are all parts of that tiny fraction of statements that we find interesting and are capable of finding proofs of. It's a bit like the anthropic principle 15/

but less dubious: we can actually see that the mathematics we like sits inside a vast "multiverse" of mathematical statements that we don't like. 16/16