I wanted to code something like this twenty years ago. It would have been cumbersome in C but I think a lot more do-able in a reasonable effort in Perl.

The task is really just a bunch of simple text (or tree) transforms, and a set of rules on how to apply them. It has very little to do with math itself.

There are several symbolic math engines out there, but they usually skip the step-by-step proof production. They simplify the expression as far as possible, and stop. If you have source code to these engines, it should be trivial to break it up into an iterative process, returning a set of proof production steps.

Each rule would have a pattern it looks for, and a replacement pattern. Rules should be simple and ordered. Rules should be scanned in the order they are asserted. (Hey, this is sounding more like Prolog now.) Each time you apply a rule successfully, you should start at the top again to see if it can be simplified further.

For maximum benefit, each production in the proof should also explain the mathematical rule it applied. For instance:

(a*(b+c))
(a*b + a*c)      -- distribute a to terms b and c
[download]

(Sheepishly, I tried to look up an official name for that simple transform on Wolfram's site, but came up empty. Apparently, if it's not some tensor product of primoral eigenvalues, it's too simple for Wolfram to discuss.)