@tao I have some naive questions: is there a field of math that studies applying calculus-based methods to expressions like you describe (gradient flow on expression complexity)? I guess this would fall under algorithms for symbolic equation solving.
Do people study spaces of expressions equipped with equational rewrites as geometric spaces?
Is there a study of the extent that the sort of strategies you described can be formalized and automatically applied? Why are humans seemingly still much more effective at solving equations than computers?