Experimental mathematics leading to major advances I would like to ask about examples where experimentation by computers has led to major mathematical advances.
A new look
Now as the question is five years old and there are certainly more examples of mathematical advances via computer experimentation of various kinds, I propose to consider contributing new answers to the question.
Motivation
I am aware about a few such cases and I think it will be useful to gather such examples together. I am partially motivated by the recent polymath5 which, at this stage, have become an interesting experimental mathematics project. So I am especially interested in examples of successful "mathematical data mining"; and cases which are close in spirit to the experimental nature of polymath5. My experience is that it can be, at times, very difficult to draw useful insights from computer data.
Summary of answers according to categories
(Added Oct. 12, 2015)
To make the question a useful resource (and to allow additional answers), here is a quick summery of the answers according to categories. (Links are to the answers, and occasionally to an external link from the answer itself.)
1) Mathematical conjectures or large body of work arrived at by examining experimental data - Classic
The Prime Number Theorem;  Birch and Swinnerton-Dyer conjectures; Shimura-Taniyama-Weil conjecture; Zagier's conjectures on polylogarithms; Mandelbrot set; Gosper Glider Gun (answer), Lorenz attractor;  Chebyshev's bias (answer) ; the Riemann hypothesis; the discovery of the Feigenbaum constant; (related) Feigenbaum-Coullet-Tresser universality and Milnor's Hairiness conjecture; Solving numerically the so-called Fermi--Pasta--Ulam chain and then of its continuous limit, the Korteweg--de Vries equation
2) Mathematical conjectures or  large body of work arrived at by examining experimental data - Current
"Maeda conjecture"; the work of Candès and Tao on compressed sensing; Certain Hankel determinants; Weari-Phelan structure; the connection of multiple zeta values to renormalized Feynman integrals; Thistlethwaite's discovery of links with trivial Jones polynomial; The Monstrous Moonshine; McKay's account on experimentation leading to mysterious "numerology" regarding the monster.  (link to the answer); Haiman conjectures on the quotient ring by diagonal invariants
3) Computer-assisted proofs of mathematical theorems
Kepler's conjecture ; a new way to tile the plane with a pentagon: advances regarding bounded gaps between primes following Zhang's proof; Cartwright and Steger's work on fake projective planes; the Seifert-Weber dodecahedral space is not Haken; the four color theorem, the proof of the nonexistence of a projective plane of order 10; Knuth's work on a class of projective planes; The search for Mersenne primes; Rich Schwartz's work; The computations done by the 'Atlas of Lie groups' software of Adams, Vogan, du Cloux and many other; Cohn-Kumar proof for the densest lattice pacing in 24-dim; Kelvin's conjecture; (NEW) $R(5,5) \le 48$ and $R(4,5)=25$;
4) Computer programs that interactively or automatically lead to  mathematical conjectures.
Graffiti
5) Various computer programs which allow proving automatically theorems or generating automatically proofs in a specialized field.
Wilf-Zeilberger formalism and software; FLAGTOOLS
6) Computer programs (both general purpose and special purpose) for verification of mathematical proofs.
The verification of a proof of Kepler's conjecture.
7) Large databases and other tools
Sloane's  online encyclopedia for integers sequences; the inverse symbolic calculator.
8) Resources:
Journal of experimental mathematics; Herb Wilf's  article: Mathematics, an experimental science in the Princeton Companion to Mathematics, genetic programming applications a fairly comprehensive website experimentalmath.info
; discovery and experimentation in number theory; Doron Zeilberger's classes called "experimental mathematics":math.rutgers.edu/~zeilberg/teaching.html;
V.I. Arnol'd's two books on the subject of experimental mathematics in Russian, Experimental mathematics, Fazis, Moscow, 2005, and Experimental observation of mathematical facts, MCCME, Moscow, 2006
Answers with general look on experimental mathematics: 
Computer experiments allow new avenues for productive strengthening of a problem (A category of experimental mathematics).

Bounty:
There were many excellent answers so let's give the bounty to Gauss...
Related question: Where have you used computer programming in your career as an (applied/pure) mathematician?, What could be some potentially useful mathematical databases? Results that are easy to prove with a computer, but hard to prove by hand ; What advantage humans have over computers in mathematics? Conceptual insights and inspirations from experimental and computational mathematics
 A: Computer experiments (in the early 1960s!) led Birch and Swinnerton-Dyer to the formulation of their conjecture, which stimulated the development of much of arithmetic geometry.
A: If I am not mistaken, the connection of multiple zeta values to renormalized Feynman integrals was discovered through computations (by David Broadhurst). Here is a survey of ongoing computer research around this field (from 1996).
A: Recently Burton, Rubinstein and Tillmann proved the conjecture that the Seifert-Weber dodecahedral space is not Haken.
https://arxiv.org/abs/0909.4625
Quite a bit of experimentation led up to their algorithms, as you would see by reading their paper.
A: The paper by Mark Haiman: Conjectures on the quotient ring by diagonal invariants
J. Algebraic Combin. 3 (1994), no. 1, 17-76 starts with:
It has recently been discovered, mainly on the basis of evidence obtained using the computer algebra system MACAULAY, that there seem to be unexpected and profound connections between a certain natural ring and some fundamental and much-studied aspects of combinatorics and algebraic geometry.
Haiman's conjecture that he discovered by a computer was eventually proved by himself using (human) but deep algebraic geometry.
A: A fake projective plane is a smooth compact complex surface with the same Betti numbers as $\mathbb{P}^2(\mathbb{C})$. Mumford (MR0527834) built the first one in the late 70s using $p$-adic uniformization. Klingler (MR1990668) and, independently, Yeung (MR2128300 with erratum MR2559112), showed that they necessarily corresponded to arithmetic lattices in $\mathrm{PU}(2,1)$. (That they live in $\mathrm{PU}(2,1)$ follows from Yau's Theorem MR0451180; they do the arithmeticity.) Prasad and Yeung (MR2289867) then gave the list of arithmetic constructions which could possible create such a beast.
Using a computer experiment, Cartwright and Steger gave presentations for all the fundamental groups, giving a complete classification. They have recent announcement in Comptes Rendus #348, 11-13. Their presentations also allow one to show that the congruence subgroup property doesn't hold for certain commensurability classes of lattices for which it was previously unknown. In fact, these lattices are a few of the `simplest' examples for which the congruence subgroup problem remained mysterious. (Serre conjectures in his paper on $\mathrm{SL}_2$, MR0272790, that it fails for all $\mathbb{R}$-rank one groups.)
A: According to this obituary of Edward Lorenz in Plus Magazine, he discovered the seemingly chaotic behaviour of the Lorenz attractor when a small change (due to rounding) in the boundary conditions in a numerical simulation gave rise to hugely different solutions.
A: The Shimura-Taniyama-Weil conjecture (now a theorem) and the Birch and Swinnerton-Dyer conjectures were based on examples.
A: Some of the advances regarding bounded gaps between primes following Zhang's proof were using computers and computations quite substantially. This applies to progress in polymath8, to Meynard's paper, and to progress in polymath8b. See this paper for a general perspective of these advances.
A: Graffiti is a computer program which makes conjectures in various subfields of mathematics, particularly graph theory. (And also in chemistry.) It was written by written by Siemion Fajtlowicz. Here is a 1989 article about it.
A: I was recently at this workshop at Fields on 'discovery and experimentation in number theory': you can get audio and slides from many of the presentations here although the one I wanted to recommend - David Bailey's talk - appears to be audio only. It depends what you mean by 'major mathematical advance' but there certainly seem to be many problems in number theory where even if the proof doesn't depend on heavy computation, gaining insight into what to set about proving did. I personally logged several CPUweeks trying to get to grips with my own thesis topic.
A: Weaire-Phelan structure provides a counterexample to Kelvin's conjecture that the minimal area partition of space is realized by an appropriately curved bitruncated cubic honeycomb tesselation. It was discovered by computer simulations of foam in 1993. The problem of finding the minimizing partition is still open, but nowadays you can easily toy with it yourself using Surface Evolver. Who knows, maybe you will discover a better solution!
A: The results on Chebyshev's bias is a great example. Chebyshev in 1853 noted that primes congruent to 3 modulo 4 seem to predominate over those congruent to 1. This is called Chebyshev's bias. Littlewood proved in 1914 that this bias   exists and also that it gets violated infinitely often, if you go far enough. The distance to be covered for the violation seemed to grow rapidly with each step.
Rubinstein and Sarnak proved in 1994 that the violations have nonzero density. Here the density means the "logarithmic density", as defined in that paper.
This was a quite interesting result guided at each step from considerations of experimental mathematics and computation. For more information have a look at the Rubinstein-Sarnak paper.
A: In a remarkable article from 1989, "Self-similarity and hairiness in the Mandelbrot set", Milnor formulates a number of conjectures (related to Feigenbaum universality). Citing Lisa Goldberg and Tony Phillips in the preface to Topological Methods in Modern Mathematics (Milnor's 60th birthday Festschrift, 1993),

OF special note is an unconventional article entitled Self-similarity and hairiness in the Mandelbrot set, where he presents some of his numerical experiments in holomorphic dynamics and uses them as evidence for a set of conjectures. ... The resulting data are so compelling as to suggest not only what the conjectures should say, but how they can be proved.

Lyubich later proved some of these conjectures in a groundbreaking article (Feigenbaum-Coullet-Tresser universality and Milnor's Hairiness conjecture, Annals of Mathematics, 1999), which also, for the first time, gave a conceptual proof of the Feigenbaum scaling law.
A: A direct search on CDC 6600 led to a  ctrx counterexample for a conjecture of Euler. Following an answer by Will Brian to a question about tweetable mathematics. 

A: The Prime Number Theorem was conjectured by Gauss from looking (very hard, one can presume...) at a table of the primes $\leq10^6$. It is not with too much effort that one can read his Disquisitiones as a set of tricks to determine primality with as little work as possible, and one can understand the motivation: he was his own computer, in a way :P
(I don't know where Legendre got the statement from, but he must surely have had tables of primes too!)
A: There's also a fairly comprehensive website experimentalmath.info where, I guess, some further examples of EM in action can be found.
A: I think there may be an additional category, though relatively little-known outside my own field (design automation): genetic programming applications, or more generally the application of metaheuristics. Spector et al's "Genetic Programming for Finite Algebras" (2008) is a good example of the methodology, which seems to me to be much less about the automation of proof as such, and more about enhancing mathematicians' capacity for well-defined combinatorial searches.
That said, you may want to include it, and the growing number of other GP papers in this domain, in your survey categories under (4) or (5).
A: Computer experiments are necessary in order to understand the classical Laver tables and related structures. In fact, Randall Dougherty developed the most efficient algorithm for computing the classical Laver tables as a direct result of computer calculations (here is a case of experimental mathematics leading to more experimental mathematics).
Recall that the classical Laver table $A_{n}$ is the unique structure $(\{1,\ldots,2^{n}\},*_{n})$ such that $x*_{n}(y*_{n}z)=(x*_{n}y)*_{n}(x*_{n}z)$ and $x*_{n}1=x+1\mod 2^{n}$ whenever $x,y,z\in\{1,\ldots,2^{n}\}.$
Let me quote Dougherty in this paper concerning Theorem 4.1 from which Dougherty's algorithm is based.

The history of this result is interesting. Weaker versions of it,
  formulated in terms of critical points and embeddings in
  $\mathcal{A}_{j}$, were conjectured as early as 1986, before the
  finite algebras $A_{n}$ had been discovered; but attempts to prove
  these results by induction were not successful. Much later, computer
  experiments displaying bit patterns occurring in period sequences in
  $B_{\infty}$ related to these conjectures led to the statement of the
  stronger theorem.

From the corollaries of Theorem 4.1, Dougherty developed an algorithm for computing the Laver table $A_{48}$. Dougherty's algorithm for computing $A_{48}$ relies on a look-up table consisting of all values $x*_{48}y$ where $x\leq 2^{16}$. This look-up table takes about 2.5 megabytes and it took my computer about 10 minutes for my computer to calculate this look-up table. Once this look-up table is created, my computer has been able to calculate about 57000
random values for $x*_{48}y$ a second. As I have mentioned in other places, using Dougherty's algorithm and good data compression, I suspect that it is currently possible to compute up to $A_{96}$ using a compressed look-up table much less than a gigabyte. When one uses a basic algorithm instead of Dougherty's algorithm, a modern computer is only able to compute about $A_{28}$ or so before running out of memory. 
I personally have used the technique behind Dougherty's algorithm to make my own algorithms for quickly computing in generalizations of Laver tables.
See this question for further discussions.
A: In some simple cases it is even possible to both guess some results and prove them too experimentally.  I have done this with some Hankel determinants.  Suppose you want to compute the Hankel determinant  $\det \left( {a_{i + j} } \right)_{i,j = 0}^{n - 1} $ of a sequence $(a_n )$ .  If no Hankel determinant vanishes then you can compute polynomials  $p_n (x)$ which are orthogonal with respect to the linear functional $F$  on the polynomials defined  by  $F(x^n ) = a_n .$  By Favard's theorem there exist numbers   $s_n ,t_n $ such that  $p_{n + 2} (x) = (x - s_{n + 1} )p_{n + 1} (x) - t_n p_n (x).$  In some cases it is easy to guess a formula for these numbers after computing  some of them. Thus also  the Hankel determinant can be computed.
In order to show that this guess gives the correct answer we can do the following:  Define  $a(n,j) = a(n - 1,j - 1) + s_j a(n - 1,j) + t_j a(n - 1,j + 1)$ with  $a(0,j) = \delta _{j,0} .$  By the underlying theory it suffices to show that $a(n,0) = a_n .$  In order to do this we again compute   $a(n,j)$  for small values and try to guess a closed formula for them.  In many cases we succeed. Then it suffices to verify that $a(n,j) = a(n - 1,j - 1) + s_j a(n - 1,j) + t_j a(n - 1,j + 1)$ holds for the conjectured formula.
A: First, a brief story, then the punchline.
Elsewhere  I mention a series of 0-1 matrices used for a combinatorial matrix result.  This came about because of an aspiring undergraduate (Roger House) who was using a computer to search for 0-1 matrices of certain orders and determinant values.
He showed me a printout where he listed the first representative of each class (major key order, minor key absolute determinant value).  He chose a lexicographical ordering of class members to pick this representative: this choice revealed a set of matrices with few differing entries, and those in just the first two or three columns.  I would not blame someone else for saying it was a pattern screaming to be found.
Many a time since then, I think about how to organize computer-generated data (specifically, pick an explanatory set of representatives) that reveal patterns and structure.  I think that experimental mathematics should not just include results, or even data analysis techniques, but heuristics on "how to make choices" so that patterns of note jump to the human eye.  In the case above, lexicographic order was a choice made by one person that revealed a pattern of similarity to another person.
Gerhard "At Least, Raise Their Voices" Paseman, 2015.10.12
A: 
$R(5,5) \le 48$

Is a title of a remarkable recent paper by Vigleik Angeltveit and  Brendan D. McKay. More than 20 years ago McKay and Radziszowski proved that $R(5,5) \le 49$ and  in this paper they showed that $R(4,5)=25$. 
A: A lot of Rich Schwartz's work begins with computer experiments.
Perhaps most notably is his proof that a triangle whose largest angle is less than 100 degrees has a periodic billiard trajectory.
A: I think that Zagier's conjectures on polylogarithms were based on considerable amount of numerical evidence (this has led to impressive work by Beilinson-Deligne, Goncharov...).
Serre's conjecture on modularity of mod $p$ $2$-dimensional Galois representations was also made precise thanks to simultaneous theoretical advances and numerical computations (this has paved the way to the proof of Fermat's last theorem...).
To come back to the prime number theorem, I think that Euler already "proved" it long before Gauss conjectured it by differentiating $\sum_{p\leq x}\frac{1}{p}\sim \log\log x$.
A: Hida and Maeda's article "Non-abelian base change for totally real fields" in the pacific journal of mathematics, volume 181(3) in 1997 explains how the experimental data lead to the "Maeda conjecture" (which you'll find mentioned in a few questions on MO).
A: In March 2019, Andrew Booker in the paper Cracking the problem with 33 showed that 33 is a sum of 3 cubes in $\mathbf Z$. This is a striking example of a case where checking the solution is very easy while finding it is hard. Indeed Booker showed that $$33=8866128975287528^3+(-8778405442862239)^3+(-2736111468807040)^3.$$
The paper describes the algorithm and its implementation and concludes with "The total computation used approximately 15 core-years over three weeks of real time."
Update 2019-09-12: A team led by mathematicians from the University of Bristol and Massachusetts Institute of Technology proved that $$(−80538738812075974)^3+80435758145817515^3+12602123297335631^3=42.$$
A: In 2003 Cohn and Elkies devised linear programming upper bounds for the density of optimal sphere packings in Euclidean space. They observed that by optimizing over functions in the bound it seemed one could get arbitrarily close to the densities achieved by the conjecturally optimal $\text{E}_8$ and Leech lattice in dimensions $d=8$ and $d=24$ (this appears true for $d=2$ also, where the hexagonal lattice is well-known to be optimal). This served as a promising method of solving the conjecture in these dimensions, but optimizing functions were hard to pin down.

In 2016 Viazovska explained this mystery (proving optimality of the $\text{E}_8$ lattice) by constructing a suitable function for the linear programming problem, and within the week, the argument was generalized to $24$ dimensions by Cohn, Kumar, Miller, Radchenko, and Viazovska.
A: The Robbins conjecture from 1933, asked whether two sets of Boolean algebras were equivalent. The solution has been found only in 1996 by William McCune, using the automated theorem prover EQP.
A: Another thing you might like to check out is Herb Wilf's very nice article: Mathematics, an experimental science in the Princeton Companion to Mathematics, in which he talks about the interplay between theory and experiment, and the many forms it can take. To give one of his examples (or rather classes of examples), if you generate a sequence of integers, you can plug it into Sloane's database and you may find that it is a known sequence, but generated in a completely different way. In that case, you have an instant interesting conjecture -- that there is a connection. But he discusses several other kinds of example. Another one that deserves to be mentioned is the Bailey-Borwein-Plouffe amazing formula for pi.
(Update: link to the paper added.)
Answer by Tim Gowers
A: Boolean Pythagorean triples Theorem (Heule, Kullmann, Oliver 2015) —  The set $\{1, \dots , 7824\}$ can be partitioned into two parts, such that no part contains a Pythagorean triple, while this is impossible for $\{1, . . . , 7825\}$.
See Wikipedia. The proof uses heavy computation. See this Nature article.
A: Another famous example is Harald Helfgott's 2013 proof that every odd integers greater than five  is the sum of three primes.  "The ternary Goldbach conjecture is true". arXiv:1312.774
A: You asked for a classification of types of experimental mathematics. I would like to mention just one class that interests me greatly (which is the class that predominates in polymath5). There are many examples of mathematical statements that become easier to prove when you strengthen them, because you have much more of a clue of what sort of proof is appropriate. To give one example, consider the following two statements.


*

*For every k there exists n such that every real sequence of length n has a monotonic subsequence of length k.

*Every real sequence of length mn+1 has an increasing subsequence of length m+1 or a decreasing subsequence of length n+1.
Even though 2 is a stronger statement, it is much easier to come up with the correct proof, because the nature of the bound gives you a big clue (particularly after you check easily that this bound is best possible).
In research mathematics, we often find ourselves with problems like 1, and we want to convert them into problems like 2. And a fantastic way of doing that, which was not available to our mathematical forebears to anything like the same extent, is to program a computer to solve the problem by brute force (or better still, with the help of clever algorithms) in small, but not too small, cases. Right now in polymath5 we are trying to find a proof using semidefinite programming, which involves coming up with a quadratic form with certain properties. Both finding the form and proving that it has the required properties seem to be difficult, but the first task is much easier than it might have been, because for pretty large n one can use a computer to find the best possible quadratic form, and one can then find out a lot from that about which forms are likely to be good and which less good.
A: The proof of the four color theorem, the proof of the nonexistence of a projective plane of order 10, the proof of the Kepler conjecture, the search for Mersenne primes, the discovery of the Lorenz attractor and the Feigenbaum constant among others are examples. These are in the wikipedia article on experimental mathematics with other examples. There is also a journal of experimental mathematics. Also there are some videos here from June and July of 2008 about experimental mathematics. Many of them are about the Landen transformation.
A: Donald Knuth comments in one of his papers on the key role of the use of computers in making his paper possible.
D. E. Knuth, A class of projective planes. Transactions of the American Mathematical Society 115 (1965) 541–549. 
Basically what happened was that Knuth used a computer to study an example and once he saw how that example worked he was able to see what was going on in general.
This is a common way that "experimental" mathematics can work.  Doing experiments can lead to examples that provide the proof of how some general construction can be implemented.
A: I have one personal experience with experimental mathematics. It started with a computer assisted simple proof of a result that every five dimensional polytope contains a 2-dimensional face which is a triangle or a quadrangle. It turns out that the negation of this theorem implies a certain number of inequalities for the so called flag numbers which together with known inequalities lead to a contradiction. At the end the proof can be checked easily by hand.
The next step was with Gunter Meisinger and Peter Kleinschmidt (see this paper), and we made a computer program called FLAGTOOLS that was able to prove automatically theorem of a similar type. At a later stage we tried to let the program test systematically for such theorems. Among the theorems we proved is the following: that there is a finite list of 3-polytopes so that every 9-polytope has a face from that list. Some similar work for quasisimplicial polytopes which had additional features of automations were carried out by Shahar Lovett.
Overall, it was difficult to use the automatic systems to obtain unanticipated "meaningful" or "interesting" results, and this had become harder the higher the level of automation was.
(Update:) One theorem proved by Gunter Meisinger, Peter Kleinschmidt and me was that every 9-polytope has a 3-face with at most 77 facets. The proof was transformed into art by artist Bernard Venet.

A: There is a 1982 book by Ulf Grenander: "Mathematical experiments on the computer", Academic Press.   He advices to use APL as programming language. While the practical computing advice and software part of the book might be obsolete, it has many examples from various fields.  This examples could maybe be used in a course.
The list of examples are:


*

*From statistics

*From linear algebra

*An energy minimization problem

*Neural networks (static problem)

*Limit theorems on groups 

*Pattern restoration

*Modeling language acquisition

*Study of invariant curves

*Neural networks (dynamic problem)

*High-dimensional geometry

*Strategy of proofs.

A: I submit for the third criterion Lewin's work on polylogarithm ladders, which culminates into a paper by Zagier, Lewin, Cohen using numerical evidence and (a desire for) an algorithm to compute relations (p. 6).
A: Also V.I. Arnol'd is quite enthusiastic about the experimental mathematics. In particular, he wrote two books on the subject in Russian, Experimental mathematics, Fazis, Moscow, 2005, and Experimental observation of mathematical facts, MCCME, Moscow, 2006, where, I guess, one could find a number of examples of the kind you ask for. Unfortunately, to the best of my knowledge, neither of these books was translated into English so far.
A: I'm surprised that no one has mentioned the Mandelbrot set yet, arguably the
most famous new mathematical object of the last 30 years, at least among the
general public. Benoit Mandelbrot discovered it in 1979 as a result of
computer experiments. He says that when he first saw it he was so surprised by
its appearance that he thought it must be the result of a computer
malfunction. In his book Fractals and Chaos, Mandelbrot argues that his
discovery of the Mandelbrot set contributed to the revival of experimental
mathematics and led to a general change in the attitude of mathematicians to
experiments in mathematics. On page 25 he writes:
"The culture of mathematics during the 1960s and 1970s
Within that culture the Mandelbrot set could not have been discovered. Hence its discovery marked a historical departure. Today -- but not yesterday -- only a minority among mathematicians would agree with the opinion due to someone who did not discover that set, that the study of M reflects "a rather infantile and somewhat dull mathematical sensibility" (Brooks 1989)."
A: The Monstrous Moonshine relationships between the Monster group (the largest sporadic finite simple group) and modular functions were investigated after observations of several numerical coincidences:
Several of the lowest coefficients of the Fourier expansion of the $j$ modular function are small sums of the smallest dimensions of irreducible representations of the Monster group. For example, the linear term is $196884q$, and the two smallest irreducible representations of the Monster group have dimensions $1$ and $196883$. The quadratic coefficient is the sum of the dimensions of the three smallest irreducible representations. This led to the conjecture of the existence and then the construction of an infinite graded vertex algebra on which the Monster acts whose pieces have dimensions equal to the Fourier coefficients of $j$.
I'm not sure whether computers were involved historically, but this was a shocking pattern of numerical coincidences of a type which is much easier to find now with tools like Sloane's online encyclopedia of integer sequences.
Also, it was noted that the primes $p$ such that $\mathbb H^2/\Gamma_0(p)^*$ has genus zero are precisely the primes dividing the order of the Monster group.
A: A fairly classical (and pretty dated at that) example is the study of solitons which was to a large extent triggered by solving numerically the so-called Fermi--Pasta--Ulam chain and then of its continuous limit, the Korteweg--de Vries equation. It would not be much of exaggeration to say that the whole modern theory of integrable systems grew out of this. For more details see e.g. the Wikipedia entry on solitons and the first chapter of the book Solitons in Mathematics and Physics by Alan Newell.
A: John Conway initially thought that his cellular automata game of Life could not lead to an unlimited number of active cells starting from a finite number of cells.
Computer experimentation by Bill Gosper led to the discovery in 1970 of the Gosper Glider Gun, a finite collection of cells which leads to a recurring state which continues to emit "spaceships" or "bullets" which continue out into the periphery infinitely.  I can't find a link to the specifics of the discovery beyond the remark that Gosper won a 50$US reward from Conway for making this finding.
The glider gun was also used in constructions involving the manipulations of the "bullets" in such a way as to form a computational apparatus, ultimately proving the Turing-completeness of Conway's Life.
I do know that a lot of random configuration discovery was done for the Life cellular automaton and for other CA by creating random patterns, then masking the lattice with a pattern which blanked out the peripheral cell values and left the random pattern alone in the center of the screen, and then allowed the CA rules to run.  Escapees such as gliders would continue their motion into the blanked areas and be easily discerned in a simulation.
The first glider-type pattern was discovered by tracing the evolution of the finite starting patterns.
David Eppstein also appears to have written a program that helps in finding these spaceship types of pattern, which should also count as mathematical discoveries and exploration via computer programs.

:gfind A program by David Eppstein which uses de Bruijn graphs to search for new spaceships. It was with gfind that Eppstein found the weekender, and Paul Tooke later used it to find the dragon. It is available at http://www.ics.uci.edu/~eppstein/ca/gfind.c (C source code only).

A: Thistlethwaite's discovery of links with trivial Jones polynomial (MR1831681) should be mentioned here.  He apparently discovered them "during the course of a routine computer ennumeration."  Later he and Eliahou and Kauffman (MR1928648) were able to recognize these links as part of an infinite family of links with trivial Jones polynomial.  Further, it's my impression that the calculation that these Jones polynomials are trivial doesn't use computers.
A: One should surely also mention the Riemann hypothesis since Riemann computed a few zeros of the zeta function by hand and observed that they were on the critical line. I guess that
this contributed to his statement, together with the functional equation, of course. (I hope that I did not overlook this response in the many previous answers, sorry otherwise).
Another experimental result with a happy ending is the birth of random matrix theory by Wigner who guessed the circular law after computer experiments if I am not mistaken.
Both subjects have been recently linked experimentally.
A: The re-launching of this question is quite timely, as experimental math was behind a beautiful recent discovery of a new way to tile the plane with a pentagon. Previously only 14 such tilings were known. The new and 15th tiling announced a few weeks ago was discovered by Casey Mann, Jennifer McLoud and David Von Derau using a computer search:
https://www.theguardian.com/science/alexs-adventures-in-numberland/2015/aug/10/attack-on-the-pentagon-results-in-discovery-of-new-mathematical-tile
https://en.wikipedia.org/wiki/Pentagonal_tiling
A: I am familiar with a few more examples of various types. I think that in order to be useful we can think about various different types of "computer aided experimental mathematics".
A) Conjectures obtained from computer experimentations.

*

*A famous example is Feigenbaum's discovery: (Quote from the wikipedia article) "Some mathematical mappings involving a single linear parameter exhibit the apparently random behavior known as chaos when the parameter lies within certain ranges. As the parameter is increased towards this region, the mapping undergoes bifurcations at precise values of the parameter. At first there is one stable point, then bifurcating to an oscillation between two values, then bifurcating again to oscillate between four values and so on. In 1975, Dr. Feigenbaum, using the small HP-65 calculator he had been issued, discovered that the ratio of the difference between the values at which such successive period-doubling bifurcations occur tends to a constant of around 4.6692... He was then able to provide a mathematical proof of that fact, and he then showed that the same behavior, with the same mathematical constant, would occur within a wide class of mathematical functions, prior to the onset of chaos. For the first time, this universal result enabled mathematicians to take their first steps to unravelling the apparently intractable "random" behavior of chaotic systems. This "ratio of convergence" is now known as the first Feigenbaum constant."


*There are various mathematical packages with more "general-purpose" experimentation in various fields and some of those have led to interesting conjectures.
B) Computerized proof

*

*Also here there are several examples of different nature. In some cases (like Hales proof of the density packing conjecture) verifying the proof requires full replication of the experiment. In some other cases, like the proof of Cohn and Kumar for the densest lattice in 24 dimensions, in Optimality and uniqueness of the Leech lattice among lattices (Annals, 2009),  checking an automated proof can be carried out (again usually using computers) with less effort compared to the effort in finding the proof.


*There are computer packages which allow more "general-purpose" forming-conjectures-and-proving-them in various (still quite restricted) areas.
A: When I was an undergrad, Jon Borwein showed me the inverse symbolic calculator.  You type in a number, and the inverse calculator tells you what it 'thinks' your number is, for example $\pi^2$. I thought it was a useful tool for experimenting.  For example, if you have a series or integral which you can't evaluate exactly, you can evaluate it numerically and plug it into the inverse calculator to see if it spits out a 'meaningful' answer.  You then have something that you can actually try to prove.
This isn't a very deep application, but there is more information on this page for experimental mathematics. 
Edit. My original link to the inverse symbolic calculator appears to be dead.  Here is a link to another working version (thanks to Houshalter for the pointer).  
A: Didn't the work of Candès and Tao on compressed sensing begin by a computer experiment by Candès that gave results "too good to be true"?
See: http://www.ams.org/samplings/math-history/hap7-pixel.pdf
A: The solution of the Kepler's conjecture by Hales deserves a special answer since it gives an important example both for a proof to  a mathematical theorem massively using computers, and 15 years later by an impressive project for demonstrating a formal proof for the conjecture that could be automatically verified.
The problem and the first project which in part was carried out by Hales with Ferguson is described in the Notices AMS paper "Cannonballs and Honeycombs" Another reference is
a 2002 ICM survey A Computer Verification of the Kepler Conjecture.
The published account of the second project - The Flyspeck project can be found in the paper A formal proof of the Kepler conjecture.
For more information and links, see Hales homepage.

A: Thurston's geometrization program began with Bob Riley's computer experiments - Thurston's intuition was actually initially the opposite (he did not believe that the figure eight knot could be hyperbolic until he saw the experimental result).
A: I don't think any precise theorems have fallen out yet, but the computations done by the 'Atlas of Lie groups' software of Adams, Vogan, du Cloux and many others has "completely changed the way [they] look at the field"
Edit: Jeff Adams agreed to give a lecture this semester where he would outline what surprising facts have been discovered, what conjectures have been made, what statements have been proved, etc. by looking at Atlas data. If this happens I'll post some kind of summary here.
A: (Answer by John Mckay:) That the product of two conjugate (type 2A) involutions of the monster, M
lies in 9 conjugacy classes with order given  by the coefficients of the highest root in affine E8, namely {1,2,3,4,5,6,4,2,3} -- and similarly for
E7 and E6 with 2.Baby and 3.F24' respectively -- was experimental with very
little evidence. See my note in Nature  305,  672, 20th Oct 1983 on numerology.

(GK: Indeed this is a very important example in the history of mathematics. Here is the Nature's paper)

A: I will add two examples of conjectures from quantum topology based on computer data.

*

*The slope conjecture: Quantum topology associates a sequence of rational numbers to a rational homology sphere $M$ as coefficients of an invariant called the Ohtsuki series. The slope conjecture states that the ratios of adjacent coefficients of powers $(q+1)^n$ in the Ohtsuki series of a rational homology sphere (except $S^3$) asymptotically grows linearly in $n$ and that the slope satisfies certain conditions. I believe it is still wide open. It was discovered by Lawrence and Jacoby in this paper by examining computer-generated plots such as the following:




*Mysterious fish-like graph: Let $v_2$ and $v_3$ denote the $\mathbb{R}$-valued Vassiliev invariants of knots of degree $2$ and $3$ respectively, normalized appropriately. Willerton, following Okuda, plotted the values of $\left(\frac{v_2}{n^2},\frac{v_3}{n^3}\right)$ for certain families of knots with fixed crossing number, and obtained the following mysterious "fish-like graph":


This led to a slew of results and conjectures, as described in Ohtsuki's problem list. To the best of my knowledge, the although there are partial results, the appearance of the fish-like graph is still a mystery.
