In Automated conjecture making in number theory using HR, Otter and Maple, the HR program discovered the following conjecture:
Paraphrased,... if you take an integer and add up the divisors, then if the result is a prime, the number of divisors you have just added up will also be prime
all a (isprime(sigma(a)) -> isprime(tau(a)))
Where sigma(a) and tau(a) are the sum of the divisors of a, and the number of divisors of a, respectively.
They then proved that this conjecture is true. To me this seems very interesting and non-obvious. But I have no idea if this theorem is significant, or if it was totally unknown before this program discovered it.
EDIT: I'm told that specific conjecture might not be particularly interesting to mathematicians. Here are some more conjectures the program discovered, from that paper:
It conjectured (and then the author proved) that sum of the divisors of square numbers is always odd, i.e.:
issquare(a) → odd(σ (a))
Probably not new either, but still cool that it was automatically discovered.
The program also discovered (invented?) a new concept called "refactorable numbers", and then made some surprising and interesting conjectures about this new concept:
HR invented the concept of refactorable numbers, which are such that the number of divisors is itself a divisor, e.g., 9 is refactorable, because 9 has three divisors (1, 3 and 9) and 3 divides 9.
This left us with 26 open conjectures, which we present in Appendix C. We have not yet fully investigated these remaining conjectures, and it seems likely that the majority may be false. Of particular interest to us are the conjectures about refactorable numbers: amongst others, HR made the conjectures that: (i) for even numbers, if σ (a) is refactorable, then τ (a) and σ (a) will be even, (ii) for odd numbers, if σ (a) is even and refactorable, then τ (τ (a)) and σ (τ (a)) will both be prime, (iii) if τ (a) is refactorable and τ (τ (a)) is prime, then σ (τ (a)) will also be prime, and (iv) if both σ (a) and σ (σ (a)) are refactorable, then
τ (σ (a)) will be refactorable and σ (τ (a)) will be odd.
The author has a number of other papers on this program and things it's discovered. I'm just now reading through Automatic Invention of Integer Sequences, where they claim it invented 17 novel integer sequences that were accepted into OEIS. Including the refactorable numbers mentioned above.