I’ve long had this dream of building a system that would allow for symbolic algebra manipulations, where the representation knows about the semantics. The idea is to replace long and tedious pen-and-paper symbolic calculations, while still having direct control over each step of the calculation. In looking for something like this I’ve found specialized proof verifiers, which are doing something different. At the other end of the spectrum there’s Mathematica, which does symbolic manipulation but doesn’t understand enough semantics.
Are these projects aiming at something like what I’m describing? Or are they more about something else like verifying proofs?