For proofs and derivations, smath needs a few things. I have been using the line function to keep successive expressions in line on the right side of an equal sign. I would like a similar function, but with entry blanks on both sides of the vertical line so that I can work on manipulations in line by line lockstep on both sides for my derivations.

Also, it needs to be able to look at two symbolic expressions and figure out if they are equal or not. Part of the reason this is hard in smath is that the facility for symbolic simplification is very rudimentary and barely improves complex expressions, even when they turn out to be very simple linear summations.

Simplification of algebraic expressions is very poor in smath. I would like to see the ability to interact with the simplification process in order to help it along. For example, I could specify in a dialogue box what variables are the key variables in a linear sum so that smath knows I want the final expression to contain these two variables once each in a sum of products along with the rest of the terms whatever they turn out to be. Then smath can do all necessary algebra to accomplish this task. I could also input explicit terms that I might expect in the result for smath to shoot for. I could tell smath if I want a polynomial expression in x, a sum of products, a ratio of some kind, etc. This would go a long way toward automating many of the tedious algebraic manipulation that many problems require.

I'm sure there are other ideas that would facilitate logic proofs and derivations, such as features for predicate logic and propositional calculus, truth tables, and other symbolic logic functions and structures.