Mathematica's rearrangement is really the same thing (except that usually you don't see the intermediate steps or what inference rules justify them). I think th

Mathematica's rearrangement is really the same thing (except that usually you don't see the intermediate steps or what inference rules justify them). I think the particular example you mention isn't far away from being available through whatever natural language thing they have. There are lots of existing theorems about e.g. increasing sequences that rely on showing a particular quantity is positive. You can pretty much do that right now, by say, using the ratio test, or some other De Morgan-type test, and then asking your CAS to express it as as a perfect square, or symbolically find its global minimum and asymptotes. Right now I think your best bet is still to employ a student intern though.