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.

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

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

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

2. There are computer packages which allow more "general-purpose" forming-conjectures-and-proving-them in various (still quite restricted) areas.

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.

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

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

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

2. There are computer packages which allow more "general-purpose" forming-conjectures-and-proving-them in various (still quite restricted) areas.

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.

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

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

1. 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, checking an automated proof can be carried out (again usually using computers) with less effort compared to the effort in finding the proof.

2. There are computer packages which allow more "general-purpose" forming-conjectures-and-proving-them in various (still quite restricted) areas.

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.

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

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

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

2. There are computer packages which allow more "general-purpose" forming-conjectures-and-proving-them in various (still quite restricted) areas.