I've been messing around with a computer algebra simplifier in Lean: https://github.com/dharmatech/symbolism.lean https://github.com/dharmatech/symbolism.lean

I've been messing around with a computer algebra simplifier in Lean: https://github.com/dharmatech/symbolism.lean https://github.com/dharmatech/symbolism.lean Lean is astonishingly expressive.