I would just add that Mathematica-style term rewriting (e.g. analytical integration, or equation solving) is done with _semantics-preserving_ symbolic solvers,

I would just add that Mathematica-style term rewriting (e.g. analytical integration, or equation solving) is done with _semantics-preserving_ symbolic solvers, which are hand-made and human-reviewed to guarantee correctness. LLM style pattern matching and rewriting does not preserve semantics, except accidentally due to an overwhelming amount of examples.