<p>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:</p>

<ul>
<li>The simplex algorithm</li>
<li>The k-means algorithm</li>
</ul>

<p>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 ! </p>

CC BY-SA 2.5
2010-10-13T03:49:06.177Z
2010-10-13T03:49:06.177Z
Suresh Venkat
<p>Parallel repetition is a nice example from my area:</p>

<p><strong>A Brief explanation of parallel repetition.</strong>
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").</p>

<p>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 <em>parallel repetition</em>: 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.</p>

<p><strong>The history.</strong> 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:
<a href="http://www.cs.washington.edu/education/courses/cse533/05au/na-game.pdf">http://www.cs.washington.edu/education/courses/cse533/05au/na-game.pdf</a>.
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.</p>

<p><strong>Insights for the problem and more consequences.</strong> 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).</p>

<p>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. </p>

<p>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). </p>

CC BY-SA 2.5
2010-10-13T14:25:14.113Z
This is a nice example !
Suresh Venkat
CC BY-SA 3.0
2010-10-13T13:26:02.703Z
2011-05-25T19:56:00.917Z
2011-05-25T19:56:00.917Z
Dana Moshkovitz
<p>This example is along the lines of Dana and Scott's answers.</p>

<p>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.</p>

<p>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$.</p>

CC BY-SA 2.5
2010-10-13T16:34:40.720Z
2010-10-13T16:34:40.720Z
Ryan Williams
<p>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.</p>

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

<p>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?</p>

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

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

<p>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:</p>

<p>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.</p>

<p>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).</p>

<p>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.</p>

<p>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.</p>

CC BY-SA 2.5
2010-10-13T02:30:18.797Z
2010-10-13T02:41:10.533Z
2010-10-13T02:41:10.533Z
matus
<p>Rasborov and Rudich's paper <a href="http://en.wikipedia.org/wiki/Natural_proof">"Natural Proofs"</a> offers a rigorous proof of (a formalization of) the painfully obvious statement "It's <em>really</em> hard to prove that P≠NP."</p>

CC BY-SA 2.5
2010-10-12T20:54:26.323Z
"It is really hard to prove that P≠NP" is not equivalent to "natural proofs most likely won't prove P≠NP". There are other barriers such as Relativization and Algebrization. Actually, there could be infinitely many more barriers.
Mohammad Al-Turkistany
CC BY-SA 2.5
2010-10-12T21:48:38.400Z
Relativization is just "It's hard to prove P≠NP."  Algebraization came later, but it's a formalization of "It's *really* **really** hard to prove P≠NP."  (Ha ha only serious.)
Jeffε
CC BY-SA 2.5
2010-10-12T16:54:54.510Z
2010-10-12T16:54:54.510Z
Jeffε
<p>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.  </p>

<p><strong>Update:</strong> I just realized that my answer like <a href="https://cstheory.stackexchange.com/questions/2136/rigour-leading-to-insight/2140#2140">the nice answer of Turkistany</a> addresses the title of the question "rigour leading to insight" but perhaps not the specific wording which was about "rigorous proof to a theorem".</p>

CC BY-SA 2.5
2010-11-16T15:55:00.973Z
2010-11-16T16:12:30.117Z
2017-04-13T12:32:28.077Z
Gil Kalai
<p>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.</p>

CC BY-SA 3.0
2011-05-26T04:22:57.690Z
@Gil, sorry for the late reply. It has been a while but I just saw your comment. No, I agree that I exaggerated and my analogy went too far. My problem was that I felt the answer is under-valuing the work done by Matiyasevich, Julia Robinson, and others. Turing was an important mathematician but I don't like when people credit him for works he has not done. But I guess I could point this out more politely.
Kaveh
CC BY-SA 2.5
2010-10-12T19:05:31.890Z
@Kaveh, What is MRDP?
Mohammad Al-Turkistany
CC BY-SA 2.5
2010-10-12T20:04:57.400Z
There are uncomputable recursively enumerable (RE) sets (such as the Halting problem). Matiyasevich proved that any recursively enumerable set is Diophantine. This immediately implies the impossibility of Hilbert's 10th problem.
Mohammad Al-Turkistany
CC BY-SA 2.5
2010-10-12T20:16:56.547Z
@Kaveh, Why didn't you subject the first answer to your "rigorous" tests? As far as I know, Natural proof is not the only barrier preventing us from proving P vs NP.
Mohammad Al-Turkistany
CC BY-SA 2.5
2010-10-12T20:38:53.847Z
@Kaveh, "It is really hard to prove that $P\ne NP$" is not equivalent to natural proofs most likely won't prove $P\ne NP$. There are other barriers.
Mohammad Al-Turkistany
CC BY-SA 2.5
2010-11-16T16:03:30.607Z
I think it is a nice answer.
Gil Kalai
CC BY-SA 2.5
2010-11-16T16:11:23.643Z
To some extent, the critique of an answer which perhaps does not rigorously answer the question but is clearly related to its general spirit shows that rigour has some drawbacks as well. It can lead to insight and it can lead away from insight.
Gil Kalai
CC BY-SA 2.5
2010-11-25T19:50:43.757Z
Dear Kaveh, I am not sure I agree with your analogy: Claiming that the solution for Hilbert's 10 problem relies (among other things) on the rigorous mathematical definitions of computability by Turing and others is analogous to claiming that the solution for FLT relies on Peano works. Do you really stand by this analogy?
Gil Kalai
CC BY-SA 2.5
2010-10-12T17:46:08.817Z
2010-10-12T18:06:03.990Z
2010-10-12T18:06:03.990Z
Mohammad Al-Turkistany
<p>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 <i>from their own experience</i> where the proof of a widely-believed conjecture in their subarea led to new insights.</p>

<p>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.)</p>

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

<p>But then, a few months later, Andris Ambainis came out with his <a href="http://arxiv.org/abs/quant-ph/0002066">quantum adversary method</a>, 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 <i>superposition</i> 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.</p>

<p>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 <i>classical</i> lower bounds.</p>

<p>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 <i>a priori</i>.</p>

CC BY-SA 2.5
2010-10-13T03:05:20.130Z
2010-10-13T03:20:35.837Z
2010-10-13T03:20:35.837Z
Scott Aaronson
<p>On MathOverflow, Timothy Gowers asked a question titled "<a href="https://mathoverflow.net/questions/37610/demonstrating-that-rigour-is-important">Demonstrating that rigour is important</a>".  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].</p>

<p>I would therefore like to know</p>

<blockquote>
  <p>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?</p>
</blockquote>

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

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

<hr>

<p><em>Edit:</em> 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.</p>

<p>We already have a question about "surprising" results in complexity: <a href="https://cstheory.stackexchange.com/questions/276/surprising-results-in-complexity-not-on-the-complexity-blog-list">Surprising Results in Complexity (Not on the Complexity Blog List)</a> so ideally I am looking for answers that focus on the <strong>value of rigorous proof</strong>, not necessarily the size of the breakthrough.</p>

CC BY-SA 2.5
2010-10-12T17:21:13.773Z
Don't we see/do this every day?
Dave Clarke
CC BY-SA 2.5
2010-10-12T19:00:58.930Z
Just to make sure I understood your question, are you asking for a triple (statement S, proof P, insight I), where the statement S is known/believed to be true, but we obtain a *new* insight (I) when someone come up with the new proof P for S?
Kaveh
CC BY-SA 2.5
2010-10-12T19:05:17.787Z
[continued] E.g. in the LLL case, we had nonconstructive proofs for [LLL](http://en.wikipedia.org/wiki/Lov%C3%A1sz_local_lemma) (S), but [the new constructive proof](http://blog.computationalcomplexity.org/2009/06/kolmogorov-complexity-proof-of-lov.html) [arXive](http://arxiv.org/abs/0903.0544) (P) gives us a [new insight](http://blog.computationalcomplexity.org/2010/04/new-constructive-aspects-of-lov-local.html) (I).
Kaveh
CC BY-SA 2.5
2010-10-13T03:01:14.667Z
Hmm... What about starting with specific algorithms and then using them as data points to generalize?  Such as, people design a few greedy algorithms, and eventually the field develops a notion of a problem with optimal substructure.
Aaron Sterling
<big-list><soft-question><proofs>
Rigour leading to insight
András Salamon
# Rigour leading to insight

(Asked by: username_0 on 2010-10-12)

On MathOverflow, Timothy Gowers asked a question titled "[Demonstrating that rigour is important](https://mathoverflow.net/questions/37610/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 username_7. As username_2 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 username_7 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)](https://cstheory.stackexchange.com/questions/276/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.

**Tags:** big-list, soft-question, proofs

> **Comments:**
> **username_1**: Don't we see/do this every day?  
> **username_2**: Just to make sure I understood your question, are you asking for a triple (statement S, proof P, insight I), where the statement S is known/believed to be true, but we obtain a *new* insight (I) when someone come up with the new proof P for S?  
> **username_2**: [continued] E.g. in the LLL case, we had nonconstructive proofs for [LLL](http://en.wikipedia.org/wiki/Lov%C3%A1sz_local_lemma) (S), but [the new constructive proof](http://blog.computationalcomplexity.org/2009/06/kolmogorov-complexity-proof-of-lov.html) [arXive](http://arxiv.org/abs/0903.0544) (P) gives us a [new insight](http://blog.computationalcomplexity.org/2010/04/new-constructive-aspects-of-lov-local.html) (I).  
> **username_3**: Hmm... What about starting with specific algorithms and then using them as data points to generalize?  Such as, people design a few greedy algorithms, and eventually the field develops a notion of a problem with optimal substructure.  

---

## 8 answers

### Answer by username_11 on 2010-10-13. Score: 35 | Accepted answer

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 Ω(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](http://arxiv.org/abs/quant-ph/0002066), 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 by username_5 on 2010-10-13. Score: 27

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).

> **Comments:**
> **username_4**: This is a nice example !  

---

### Answer by username_4 on 2010-10-13. Score: 20

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 by username_6 on 2010-10-13. Score: 13

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 by username_7 on 2010-10-13. Score: 13

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 by username_8 on 2010-10-12. Score: 11

Rasborov and Rudich's paper ["Natural Proofs"](http://en.wikipedia.org/wiki/Natural_proof) offers a rigorous proof of (a formalization of) the painfully obvious statement "It's *really* hard to prove that P≠NP."

> **Comments:**
> **username_9**: "It is really hard to prove that P≠NP" is not equivalent to "natural proofs most likely won't prove P≠NP". There are other barriers such as Relativization and Algebrization. Actually, there could be infinitely many more barriers.  
> **username_8**: Relativization is just "It's hard to prove P≠NP."  Algebraization came later, but it's a formalization of "It's *really* **really** hard to prove P≠NP."  (Ha ha only serious.)  

---

### Answer by username_10 on 2010-11-16. Score: 6

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](https://cstheory.stackexchange.com/questions/2136/rigour-leading-to-insight/2140#2140) 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 by username_9 on 2010-10-12. Score: 0

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.

> **Comments:**
> **username_9**: @username_2, What is MRDP?  
> **username_9**: There are uncomputable recursively enumerable (RE) sets (such as the Halting problem). Matiyasevich proved that any recursively enumerable set is Diophantine. This immediately implies the impossibility of Hilbert's 10th problem.  
> **username_9**: @username_2, Why didn't you subject the first answer to your "rigorous" tests? As far as I know, Natural proof is not the only barrier preventing us from proving P vs NP.  
> **username_9**: @username_2, "It is really hard to prove that $P\ne NP$" is not equivalent to natural proofs most likely won't prove $P\ne NP$. There are other barriers.  
> **username_10**: I think it is a nice answer.  
> **username_10**: To some extent, the critique of an answer which perhaps does not rigorously answer the question but is clearly related to its general spirit shows that rigour has some drawbacks as well. It can lead to insight and it can lead away from insight.  
> **username_10**: Dear username_2, I am not sure I agree with your analogy: Claiming that the solution for Hilbert's 10 problem relies (among other things) on the rigorous mathematical definitions of computability by Turing and others is analogous to claiming that the solution for FLT relies on Peano works. Do you really stand by this analogy?  
> **username_2**: @Gil, sorry for the late reply. It has been a while but I just saw your comment. No, I agree that I exaggerated and my analogy went too far. My problem was that I felt the answer is under-valuing the work done by Matiyasevich, Julia Robinson, and others. Turing was an important mathematician but I don't like when people credit him for works he has not done. But I guess I could point this out more politely.  

---

