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

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.

-

closed as not a real question by quid, Henry Cohn, Suvrit, Daniel Moskovich, Bill JohnsonMay 5 '12 at 15:45

It's difficult to tell what is being asked here. This question is ambiguous, vague, incomplete, overly broad, or rhetorical and cannot be reasonably answered in its current form. For help clarifying this question so that it can be reopened, visit the help center.If this question can be reworded to fit the rules in the help center, please edit the question.

I'm curious what the 'very short program' looks like. –  Stopple May 2 '12 at 15:35
The question is somewhat vague to me: what about the computer proven claim that the gazillionth digit of $\pi$ is 4---this certainly is not doable by hand (in practice). Or any of the other heavy computation related claims. Maybe you want to refine your question / title to exclude such answers... –  Suvrit May 2 '12 at 17:25
Vote to close, mainly for the reason Suvrit gives. –  quid May 2 '12 at 22:39
@Suvrit: poster explicitly wrote "I am aware that one can always construct artificial examples. That is not what I want." –  danseetea May 3 '12 at 5:29
@danseetea: without wanting to be too s(n)arky, but just that some caveat is thrown in does not make the question good. For instance, it is not really apparent to me how the example in the question is 'nonartificial'. Say, why 2? Seems because this can be not done by hand but with a computer. Nothing against that investigation, which I find curious, but if you admit things like this there'll be an endless supply of combinatorial (to be understood broadly) results where the general case is unknown, some small cases can be done by hand and some slightly bigger ones by comp. –  quid May 3 '12 at 10:48

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

-
I'm not sure if this should count as "easy to prove with a computer"... –  Simon Rose May 2 '12 at 20:47
... or as "hard to prove by hand". The truth is, we just don't know. –  Daniel Moskovich May 3 '12 at 7:07
Indeed, a "simple proof by hand" is not unlikely to appear one day, albeit in the relatively trivial way, as 4CT follows immediately from conjectures such as Hadwiger's or Colin de Verdière's. –  Felix Goldberg May 3 '12 at 9:40

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.

-
Sound like a great example to me. –  Felix Goldberg May 3 '12 at 9:41

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

-
This is also not something that's easy to prove with a computer. –  Zsbán Ambrus May 3 '12 at 7:23
Well what means "easy"? –  Martin Brandenburg May 3 '12 at 7:38