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

4more comments