[wwalker3]

That's a good point. Guess-and-verify could be a handy additional heuristic method if Mathematica's other methods came up empty on a problem. I've also heard of machine learning being used to choose between internal algorithms available in formal proof systems, to try to pick the algorithm that's most likely to work instead of just trying them all sequentially.

[andrepd]

The person opposite my desk is working on precisely that! (And I'm making more algorithms for him to feed to his model :p)