'a+(-b)'

An idea is to punish it (deduct from the metric) when it violates the basic presentation rules we all learned in primary school. E.g. superfluous bracketing. Or failing to simplify +-5 to -5. Assign to each violation a significance to be translated to a punishment number. Actually as it is, it seems that you will soon go down to negative metric. So, convert your metric to "unfitness" and keep adding the penalties. The smaller the metric the fitter the solution (aesthetically speaking). And also there could be different metrics, like aesthetics, terseness, pedantic. And you combine them, with weights, in a multidimensional overall metric.

The other idea is to use other proof checkers and see how your output compares to theirs in terms of presentation of final result. Unless yours is far superior than anything else out there and it excels in each and every metric!

Lastly, consider this idea as an addition to your project: the idea is to additionally create a Markov Chain mathematical expression generator trained on freely available mathematical expressions which are assumed to be "perfect" as far as aesthetics are concerned. So you will also need a parser which I guess you already have. I guess mathematical expressions with the best quality would be from parsing latex equations from papers in, say, https://arXiv.org. Which, !!!hail open source!!!, offer the paper source along with pdf and postscript, e.g. https://arxiv.org/src/2412.17766. So, from my comfortable sofa: latex equation parser and a markov-chain mathematical expression generator.

Along these lines there is this n-dimensional statistical analysis of DNA sequences (or text, or ...) which resulted in a package I submitted here: https://github.com/hadjiprocopis/Algorithm-Markov-Multiorder-Learner

bw, bliako