Our Obsession with Proofs

Computational Complexity 2024-05-01

Bullinger's post on this blog last week focused on Vijay Vazirani's public obsession of finding a proof for the 1980 Micali-Vazirani matching algorithm. But why does Vijay, and theoretical computer science in general, obsess over proofs? 

You can't submit a paper to a theory conference without a claimed complete proof, often contained in an appendix dozens of pages long. Often we judge papers more on the complexity of the proof than the statement of the theorem itself, even though for a given theorem a simpler proof is always better.

A proof does not make a theorem true; it was always true. The Micali-Vazirani algorithm is no faster with the new proof. Would we have been better off if the algorithm didn't get published before there was a full proof?

We're theoretical computer scientists--doesn't that mean we need proofs? Theoretical economists and physicists don't put such an emphasis on proofs, they focus on models and theorems to justify them.

Once a senior CS theorist told economists that his group had given the first full proof of a famous economics theorem and wondered why the economists didn't care. The economists said they already knew the theorem was true, so the proof added little to their knowledge base.

More than one journalist has asked me about the importance of a proof that P \(\ne\) NP. A proof that P = NP would be both surprising and hopefully give an algorithm. While a proof that P \(\ne\) NP would be incredibly interesting and solve a major mathematical challenge, it wouldn't do much more than confirm what we already believe.

I'm not anti-proof, it is useful to be absolutely sure that a theorem is true. But does focusing on the proofs hold our field back from giving intuitively correct algorithms and theorems? Is working out the gory details of a lengthy proof, which no one will ever read, the best use of anyone's time? 

As computing enters a phase of machine learning and optimization where we have little formal proof of why these models and algorithms work as well as they do, does our continued focus on proofs make our field even less relevant to the computing world today?