You seem to be asking about computers formulating conjectures later proved by humans. As one not having had much exposure to the issue, I wonder how to teach a computer (maybe with some form of heuristics?) assessing it has found a plausible conjecture: in this case computer misses the comfort of knowing a result is true for it has proven it's true, while human mathematicians can use instinct or some kind of common sense. However, I found this:
A Symbolic Finite-State Approach For Automated Proving of Theorems in Combinatorial Game Theory
