Rigour leading to insight 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.
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 &radic;n ANDs of &radic;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(&radic;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 &Omega;(n1/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 &Omega;(&radic;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.