You asked for a classification of types of experimental mathematics. I would like to mention just one class that interests me greatly (and 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.

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

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

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.

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

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