Rigour leading to insight

Question

On MathOverflow, Timothy Gowers asked a question titled "Demonstrating that rigour is important". Most of the discussion there was about cases showing the importance of proof, which people on CSTheory probably do not need to be convinced about. In my experience proofs need to be more rigorous in theoretical computer science than in many parts of continuous mathematics, because our intuition so often turns out to be wrong for discrete structures, and because the drive to create implementations encourages more detailed arguments. A mathematician may be content with an existence proof, but a theoretical computer scientist will usually try to find a constructive proof. The Lovász Local Lemma is a nice example [1].

I would therefore like to know

are there specific examples in theoretical computer science where a rigorous proof of a believed-to-be-true statement has led to new insight into the nature of the underlying problem?

A recent example that is not directly from algorithms and complexity theory is proof-theoretic synthesis, the automatic derivation of correct and efficient algorithms from pre- and post-conditions [2].

• [1] Robin A. Moser and Gábor Tardos, A Constructive Proof of the General Lovász Local Lemma, JACM 57, article 11, 2010. http://doi.acm.org/10.1145/1667053.1667060
• [2] Saurabh Srivastava, Sumit Gulwani, and Jeffrey S. Foster, From program verification to program synthesis, ACM SIGPLAN Notices 45, 313–326, 2010. http://doi.acm.org/10.1145/1707801.1706337

---

Edit: The kind of answer I had in mind is like those by Scott and matus. As Kaveh suggested, this is a triple of something people wanted to prove (but which wasn't necessarily unexpected by "physics", "handwaving", or "intuitive" arguments), a proof, and consequences for the "underlying problem" that followed from that proof that weren't anticipated (perhaps creating a proof required unexpected new ideas, or naturally leads to an algorithm, or changed the way we think about the area). Techniques developed while developing proofs are the building blocks of theoretical computer science, so to retain the value of this somewhat subjective question, it would be worth focusing on personal experience, such as provided by Scott, or an argument that is backed up by references, as matus did. Moreover, I'm trying to avoid arguments about whether something qualifies or not; unfortunately the nature of the question may be intrinsically problematic.

We already have a question about "surprising" results in complexity: Surprising Results in Complexity (Not on the Complexity Blog List) so ideally I am looking for answers that focus on the value of rigorous proof, not necessarily the size of the breakthrough.

Answer 1

András, as you probably know, there are so many examples of what you're talking about that it's almost impossible to know where to start! However, I think this question can actually be a good one, if people give examples from their own experience where the proof of a widely-believed conjecture in their subarea led to new insights.

When I was an undergrad, the first real TCS problem I tackled was this: what's the fastest quantum algorithm to evaluate an OR of √n ANDs of √n Boolean variables each? It was painfully obvious to me and everyone else I talked to that the best you could do would be to apply Grover's algorithm recursively, both to the OR and to the ANDs. This gave an O(√n log(n)) upper bound. (Actually you can shave off the log factor, but let's ignore that for now.)

To my enormous frustration, though, I was unable to prove any lower bound better than the trivial Ω(n^1/4). "Going physicist" and "handwaving the answer" never looked more appealing! :-D

But then, a few months later, Andris Ambainis came out with his quantum adversary method, whose main application at first was a Ω(√n) lower bound for the OR-of-ANDs. To prove this result, Andris imagined feeding a quantum algorithm a superposition of different inputs; he then studied how the entanglement between the inputs and the algorithm increased with each query the algorithm made. He showed how this approach let you lower-bound quantum query complexity even for "messy," non-symmetric problems, by using only very general combinatorial properties of the function f that the quantum algorithm was trying to compute.

Far from just confirming that the quantum query complexity of one annoying problem was what everyone expected it to be, these techniques turned out to represent one of the biggest advances in quantum computing theory since Shor's and Grover's algorithms. They've since been used to prove dozens of other quantum lower bounds, and were even repurposed to obtain new classical lower bounds.

Of course, this is "just another day in the wonderful world of math and TCS." Even if everyone "already knows" X is true, proving X very often requires inventing new techniques that then get applied far beyond X, and in particular to problems for which the right answer was much less obvious a priori.

Answer 2

Parallel repetition is a nice example from my area:

A Brief explanation of parallel repetition. Suppose you have a two-prover proof system for a language $L$: Given input $x$, known to everyone, a verifier sends question $q_1$ to prover 1, and question $q_2$ to prover 2. The provers answer with answers $a_1$ and $a_2$, respectively, without communicating. The verifier performs some check on $a_1$ and $a_2$ (depending on $q_1,q_2$) and decides whether to accept or reject. If $x\in L$, there exists a provers strategy that the verifier always accepts. If $x\not\in L$, for any provers strategy, the verifier accepts with probability at most $s$ ("error probability").

Now suppose we want a smaller error probability. Maybe $s$ is close to $1$, and we want $s = 10^{-15}$. A natural approach would be parallel repetition: let the verifier send $k$ independent questions to each prover, $q_1^{(1)},\ldots,q_1^{(k)}$ and $q_2^{(1)},\ldots,q_2^{(k)}$, receive k answers from the provers $a_1^{(1)},\ldots,a_1^{(k)}$ and $a_1^{(1)},\ldots,a_1^{(k)}$, and performs $k$ checks on the answers.

The history. At first, it was "clear" that the error probability had to decrease like $s^{k}$, just as if the verifier would have made $k$ sequential checks. The legend says it was given to a student to prove, before it was realized that the "obvious" statement is simply false. Here is an exposition of a counterexample: http://www.cs.washington.edu/education/courses/cse533/05au/na-game.pdf. It took a while (and several weaker results), before Ran Raz finally confirmed that the error probability indeed decreases exponentially, but has a slightly complicated behavior: it is $s^{\Omega(k/\log|\Sigma|)}$, where the alphabet $\Sigma$ is the set of possible provers answers in the original system. The proof used information theoretic ideas, and was said to be inspired by an idea of Razborov in communication complexity. A messy part of Ran's original proof was later beautifully simplified by Thomas Holenstein, resulting in one of my favorite proofs.

Insights for the problem and more consequences. First there are the immediate things: a better understanding of the quantitative behavior of parallel repetition, and the role that the alphabet $\Sigma$ plays, a better understanding of when the provers can use the parallel questions to cheat, a better understanding of the importance of independence in parallel repetition between the $k$ pairs of questions (later formalized by Feige and Kilian).

Then, there are the extensions that became possible: Anup Rao was able to adapt the analysis to show that when the original proof system is a {\em projection game}, i.e., the answer of the first prover determines at most one acceptable answer of the second prover, there is no dependence on the alphabet at all, and the constant in the exponent can be improved. This is important because most hardness of approximation results are based on projection games, and unique games are a special case of projection games. There are also quantitative improvements in games on expanders (by Ricky Rosen and Ran Raz), and more.

Then, there are the far-reaching consequences. Just a few examples: An information theoretic lemma from Raz's paper was used in many other contexts (in cryptography, in equivalence of sampling and searching, etc). The "correlated sampling" technique that Holenstein used was applied in many other works (in communication complexity, in PCP, etc).

Answer 3

Another good example of rigor (and new techniques) being needed to prove statements that were believed to be true: smoothed analysis. Two cases in point:

• The simplex algorithm
• The k-means algorithm

For both methods, it was "well known" that they worked well in practice, and for the first, it was known that it took worst-case exponential time. Smoothed analysis can be seen as having "explained" the good empirical behavior in both cases. In the second, while it was known that the worst-case complexity of $k$-means was $O(n^{c \cdot kd})$, it was not known whether there were lower bounds that were exponential in $n$, and now we know that's true, even in the plane !

Answer 4

I think the following example spawned a lot of research which had results of the kind you are looking for, at least if I follow the spirit of your LLL example.

Robert E. Schapire. The strength of weak learnability. Machine Learning, 5(2):197-227, 1990.

This paper resolved the question: are strong and weak PAC learning equivalent? I can not tell you for certain whether the people in that circle (Schapire, Valiant, Kearns, Avrim Blum, ..) felt strongly one way or another (i.e. if this is already an instance of what you seek), though I have some suspicions, and you can form your own by looking at the papers around then. Briefly (and approximately/probably), a problem is PAC learnable (by a hypothesis class, for a distribution) if, for any $\epsilon>0, \delta>0$, there exists an ('efficient') algorithm which can produce with probability at least $1-\delta$ a hypothesis with error at most $\epsilon$. If you could satisfy the $\epsilon$ but not the $\delta$, then as long as $\delta$ was not trivial ('triviality' depends on some details, since i'm leaving out the meaning of 'efficient'), repeated trials would boost the confidence $\delta$. But if instead you could only achieve some $\gamma$ advantage over random guessing (same 'triviality' condition applies), could you somehow cleverly boost this result to attain arbitrarily good error?

Anyway, things became very interesting after Schapire's paper. His solution produced a majority-of-majority over hypotheses in the original class. Then came:

Yoav Freund. Boosting a weak learning algorithm by majority. Information and Computation, 121(2):256--285, 1995.

This paper had a 'reproof' of Schapire's result, but now the constructed hypothesis used only a single majority. Along these lines, the two then produced another reproof, called AdaBoost:

Yoav Freund and Robert E. Schapire. A decision-theoretic generalization of on-line learning and an application to boosting. Journal of Computer and System Sciences, 55(1):119-139, 1997.

The weak/strong learning question started out as a primarily theoretical concern, but this sequence of 'reproofs' resulted in a beautiful algorithm, one of the most influential results in machine learning. I could go off on all sorts of tangents here but will restrain myself. In the context of TCS, these results breath a lot of life in the context of (1) multiplicative weight algorithms and (2) hard-core set results. About (1), I'd just like to clarify that AdaBoost can be seen as an instance of the multiplicative weights / winnow work of Warmuth/Littlestone (Freund was a Warmuth student), but there is a lot of new insight in the boosting results. About (2), I'd like to clarify that although Russell Impagliazzo was graduating Berkeley around when Kearns was visiting and the Kearns+Vazirani learning theory book appeared (Kearns had thought a lot about boosting, and material appeared in the book), I have a few reasons to believe that Russell produced his results essentially independently (further work along these lines relied on the Boosting results more closely).

For historical accuracy I should also say that the dates on my citations are maybe not what some people would expect, since for a few of these there were earlier conference versions.

Back to the nature of your question. The key value of 'rigor' here was in providing the hypothesis class one learns over (weighted majorities over the original hypothesis class) and efficient algorithms to find them.

Answer 5

This example is along the lines of Dana and Scott's answers.

It is "obvious" that the best way of computing the PARITY of $n$ bits with an unbounded fan-in circuit of depth $d$ is the following recursive strategy. When the depth $d$ is 2, there's nothing better you can do than write out the CNF (or DNF) of all $2^{n-1}$ terms. When $d$ is greater than $2$, break the set of input variables into $n^{1/(d-1)}$ parts, guess the parity of each of the parts (take an OR of fan-in $2^{n^{1/(d-1)}}$), and for those guesses which add up to parity $1$, recursively solve the problem on each of the parts (take an AND of fan-in $n^{1/(d-1)}$) with a depth $d-1$ circuit. If you alternate at each level of recursion between doing an OR of $2^{n^{1/(d-1)}}$ ANDs and doing an AND of $2^{n^{1/(d-1)}}$ ORs (taking the complement), you end up with a circuit of depth $d$ and size $2^{O(n^{1/(d-1)})}$ that computes PARITY.

In 1985, Hastad proved that the "obviously best" depth-$d$ circuit is optimal up to constants in the exponent. To do this, he proved the Switching Lemma which has been a very valuable tool in proving lower bounds for circuits, parallel algorithms, and proof systems. This is one of the few instances where we know that a particular natural algorithm is optimal, and it led to a very detailed understanding of the power of $AC^0$.

Answer 6

Rasborov and Rudich's paper "Natural Proofs" offers a rigorous proof of (a formalization of) the painfully obvious statement "It's really hard to prove that P≠NP."

Answer 7

The idea that some algorithmic problems require an exponential number of steps, or exaustive search over all possibilities, was raised since the 50s and perhaps before. (Of course, the competing naive idea that computers can do everything was also common.) The major breakthrough of Cook and Levin was to put this idea on rigorous grounds. This, of course, changed everything.

Update: I just realized that my answer like the nice answer of Turkistany addresses the title of the question "rigour leading to insight" but perhaps not the specific wording which was about "rigorous proof to a theorem".

Answer 8

Alan Turing formalized the notion of algorithm (effective computability) using Turing machines. He used this new formalism to prove that the Halting problem is undecidable (i.e. Halting problem can't be solved by any algorithm). This led to a long research program which proved the impossibility of the Hilbert 10th problem. Matiyasevich in 1970 proved that there is no algorithm that can decide whether a integer Diophantine equation has an integer solution.