[theresistor]

> They're comparing their algorithm's accuracy (solution correctness vs. incorrectness), with Mathematica's ability to find the correct solution in less than 30 seconds. This is a very important distinction!

I had the same initial reaction as you, but then I realized that this is still extremely useful. In a ton of examples, only one direction of differentiation/integration is hard while the other direction is easy. You could build a system that attempted to solve it directly, and failing that attempted to guess-and-verify using this approach. My intuition is that such an overall system would be strictly superior to Mathematica's approach as it exists today.

[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)