"Full"-Simplification of arbitrary mathematical expressions I've come across many (classroom) problems, like Roy did, whereby the solution to a problem, $$−3(7−2x)^2−5(1+x)^2$$ is the result of simplifying that expression as much as is possible, i.e. $$−17x^2+74x−152$$. 
But I've never seen a formal proof that $−17x^2+74x−152$ is indeed the simplest form, instead I have only been told either:


*

*that it is, 

*or, (indirectly so) that it is the simplest form because we can't find a simpler form. 


The first is a non-answer, and feel that the second is a fallacy; that the inability to find solutions implies absolute non-existence of solutions. Just because you can't come up with a solution to $a^n + b^n = c^n$ does not imply that no solutions exist.
Is there a method for proving that any arbitrary mathematical expression is represented in its simplest form? Or, phrased differently: Is there a way of proving that there are no simpler forms of a given expression?

 Of course, there's also the problem of formally defining simplicity, for which I know of no such definition. If you do know of a formal definition, please include it in your answer.

 A: There is a concept in logical reasoning called a "canonical form".  Most of the time when someone says "simplest form" they are implicitly talking about a canonical form.
A canonical form is one where equivalence can be determined lexicographically.  For example, two polynomials $-4x + 5x^2 - 2$ and $(5x-4)x - 3$, when put into canonical form $5x^2 - 4x - 2$ and $5x^2 - 4x - 3$, you can see that they are not equal because a they are represented with different strings and polynomials are a canonical form.
One logic system, ACL2 software, works on the basis of rewrite rules that try to put expressions into canonical form.
From a more foundational point of view, there is a way of writing all expressions in terms of a few primitives called combinators.  It can be demonstrated that there is no canonical form for combinatory logic, so "simplest form" is not possible for all logical expressions, only for limited sets of expressions.
A: Consider a similar example. You are in an introductory physics class and the teacher asks "A train is travelling 20 miles per hour. It goes from station A to station B which is 20 miles away. How long does it take to get there."
The correct answer is of course 1 hour but some braniac student might say "Well it depends, is it 20 miles relative to the trains reference frame or the earth's?"
Your question about simplification is similar. The question you are asking is very valid and definitely important to consider. On the other hand it is perfectly valid for the teacher to say that it is in simplest form because it is a standard that while maybe not well defined is well understood.
Regarding the actual answer, I think it would be nearly impossible to define simplest form for any mathematical formula. It can certainly be done, though, for certain subsets of the formulas. For example we can simply define $a+bx+cx^2 + dx^3 +...$ to be standard (or simplest) form for all polynomials.
