I've been messing around with a computer algebra simplifier in Lean:

https://github.com/dharmatech/symbolism.lean

Lean is astonishingly expressive.