Results that are easy to prove with a computer, but hard to prove by hand [closed]

Question

Consider the assertion:

There is no completely multiplicative function $f:\mathbb{N}\rightarrow \{\pm 1\}$ with $\left|\sum_{n\leq x}f(n)\right|\leq 2$ for all $x\geq 0$.

One can write a very short program to show that things go wrong for $x\geq 247.$ Doing this by hand with current technology requires an unmanagable amount of cases (cf. http://michaelnielsen.org/polymath1/index.php?title=Human_proof_that_completely_multiplicative_sequences_have_discrepancy_greater_than_2). I wonder whether you have encountered similar situations. I am aware that one can always construct artificial examples. That is not what I want. Rather that you consider some special case of a theorem you try to prove, such that you can prove this with a computer, but not by hand.

Btw. a short proof of the above would also count as an answer.

Answer 1

One example of a theorem that you can prove with a computer, but not by hand is the Four color theorem, see e.g. Wikipedia: http://en.wikipedia.org/wiki/Four_color_theorem.

The theorem: "The four color theorem, or the four color map theorem states that, given any separation of a plane into contiguous regions, producing a figure called a map, no more than four colors are required to color the regions of the map so that no two adjacent regions have the same color. Two regions are called adjacent if they share a common boundary that is not a corner, where corners are the points shared by three or more regions."

The proof: "Using mathematical rules and procedures based on properties of reducible configurations, Appel and Haken found an unavoidable set of reducible configurations, thus proving that a minimal counterexample to the four-color conjecture could not exist. Their proof reduced the infinitude of possible maps to 1,936 reducible configurations (later reduced to 1,476) which had to be checked one by one by computer and took over a thousand hours. This reducibility part of the work was independently double checked with different programs and computers. However, the unavoidability part of the proof was verified in over 400 pages of microfiche, which had to be checked by hand (Appel & Haken 1989).

Appel and Haken's announcement was widely reported by the news media around the world, and the math department at the University of Illinois used a postmark stating "Four colors suffice." At the same time the unusual nature of the proof—it was the first major theorem to be proven with extensive computer assistance—and the complexity of the human verifiable portion, aroused considerable controversy (Wilson 2002).

In the early 1980s, rumors spread of a flaw in the Appel-Haken proof. Ulrich Schmidt at RWTH Aachen examined Appel and Haken's proof for his master's thesis (Wilson 2002, 225). He had checked about 40% of the unavoidability portion and found a significant error in the discharging procedure (Appel & Haken 1989). In 1986, Appel and Haken were asked by the editor of Mathematical Intelligencer to write an article addressing the rumors of flaws in their proof. They responded that the rumors were due to a "misinterpretation of [Schmidt's] results" and obliged with a detailed article (Wilson 2002, 225–226). Their magnum opus, a book claiming a complete and detailed proof (with a microfiche supplement of over 400 pages), appeared in 1989 and explained Schmidt's discovery and several further errors found by others (Appel & Haken 1989)."

Answer 2

I think this example fits the question nicely (but it concerns a paper I coauthored, so if there is some feeling that this is shameless self-promotion please say it frankly in the comments and I'll delete the answer).

We were trying to classify all bilinear estimates in $\mathbb{R}^3$ for spaces of wave-Sobolev type. The precise definition of the spaces is pointless here, let's say they are some sort of Sobolev spaces with weights measuring the amount of mass close to the light cone in Fourier variables; they are characterized by two indices $H^{s,b}$ and are an essential tool in the theory of nonlinear waves. A bilinear estimate is a product estimate of the form $$H^{s_1,b_1}\cdot H^{s_2,b_2}\subset H^{s_3,b_3}$$ and one is interested in finding all the 6-tuples $(s_1,s_2,s_3,b_1,b_2,b_3)$ for which the estimate is true. There is a long list of counterexamples (21 plus symmetries; some of the trickiest ones were found by Terry Tao when he was young :) which bound a polyhedron with a large number of faces in the space of 6-tuples $\mathbb{R}^6$. Now the problem is: if a 6-tuple is inside the polyhedron, is the corresponding bilinear estimate true? in other words, is the list of counterexamples exhaustive?

In order to solve the problem we had to compute the vertices of the conjectured polyhedron (and then prove the estimates at the vertices, or near the vertices). Usually, one manages to do this kind of computation by hand with some neat tricks. But in this case, just writing the complete set of inequalities by hand takes a good 20 minutes. We had to admit, reluctantly, that this was physically impossible to do with pencil and paper. Of course this is a trivial problem for a computer and a simple algorithm gave us the answer.

Answer 3

Every position of Rubik's cube can be solved in at most 20 moves. This has been proven in 2010 with computer assistence and a little bit of group theory:

God's number is 20