Proofs at first exude a strong aroma of certainty.

On closer inspection though, more subtle notes emerge. Despite the dreams of formalists, the overwhelming majority of proofs in use and circulation are not minute low-level logical derivations, but rather intuitive high-level explanations. Some of which turn out to be false even after peer-review. Similarly, the level of details varies enormously across accepted proofs.

And yet it works, most of the time. Enough to build massive and intricate systems, and enough for millions of daily practical applications in the physical world.

What gives?

I think this mystery dissolves if we refuse to give proofs a special status. Instead of being the one and only form of certainty accessible to man, they make far more sense as “just” a strong form of evidence in the traditional scientific sense.

If proof is only evidence, then obviously different contexts call for different levels of details. We accept many geometric or intuitive proofs of the Pythagorean theorem, but ask for detailed checks on tens-of-pages-long advanced algebraic geometry proofs.

The other positive externality of desacralizing proofs comes in the form of methodological flourishing. Indeed, if proofs are merely sources of evidence, then any other way to generate evidence about formal statements is as valid, as long as the total evidence ends up approximately the same.

Or to put it more provocatively: proofs are not necessary if we find alternative ways of gathering the same amount of evidence.

Nowhere has this rich ground been better exploited than in computational complexity theory, the field studying the resources needed (time, memory, coin flips) to solve computational problems. For you see, conjectures in complexity theory are atrociously hard to prove. They’re some of the hardest across all of mathematics. But complexity theorists still want to advance their field, and so they have evolved an opportunistic methodology that accumulates evidence through alternative ways (based on proofs of other, simpler statements mostly).

Let’s look at two example methods to get an idea:

• (Approximation algorithms breaking) Imagine that we have a class of problem C that we conjecture cannot be solved with a certain amount of resources (say polynomial time). But we have approximation algorithms that can approximate the solutions to problems in C within the resource bounds. If we find out that all the approximation algorithms that we come up with mysteriously break down when we try to make the approximation more precise, this is evidence for problems in C being impossible to solve with these resources — because such result is far easier to explain for the conjecture that C cannot be solved with these resources than for the opposite conjecture.^[1]
• (Consistency proofs) Imagine that there is a mathematical theory in which we can prove many of the key results in complexity theory. Then showing that this theory is consistent with our conjecture (that there exists a valid model of the theory where the conjecture is true) is a form of logical falsification: we have shown that our conjecture is coherent with much of the established results of the field. Obviously, the more powerful the original theory is in terms of rederiving complexity theory results, the more evidence comes from the conjecture surviving this falsification.^[2]

With all this defense of methodological innovation, beware the subtle mistakes one can make in estimating the evidence coming front their new method. One classic example in complexity theory is to take “People have been trying to solve NP-complete problems quickly for 50 years and failed” as relatively strong evidence for $P\ne NP$. Absence of evidence is evidence of absence, but in this case the evidence would only be significant if we knew one additional fact: that our current software engineers and computer scientists are actually good at finding efficient algorithms. Which, given our limitations in formal sciences and the youth of computer science, is far from obvious.

So while proofs as strong evidence empowers us, we should remember Yudkowsky’s warning when discussing Einstein’s success with a similar kind of methodological shortcut.

I will not say, "Don't try this at home."  I will say, "Don't think this is easy."  We are not discussing, here, the victory of casual opinions over professional scientists.  We are discussing the sometime historical victories of one kind of professional effort over another.  Never forget all the famous historical cases where attempted armchair reasoning lost.

Einstein’s Speed, 2008, Eliezer Yudkowsky

1. ^{^}

   This is actually the case for $P\ne NP$, the most important conjecture of complexity theory. See section 3 of Scott Aaronson’s survey for more precise pointers.

2. ^{^}

   This is one reason to care about superpolynomial lower bounds for Extended Frege proof systems, as such bounds would show that $P\ne NP$ is consistent with Cook’s PV theory, which rederives many key complexity theory results. See chapter 27 of this proof complexity book by Jan Krajíček for more precise pointers.