Suppose that you have a nonlinear function with multiple local minima, and you want to optimize it to find the global optimum.
Suppose you have an algorithm that spends (say) 2 minutes exploring the system and then returns an answer, and the answer looks decent. You cross check a selection of other possible minima and the selected location is the best out of the ones that you try. 2 minutes computation on a complicated function, and returning what seems very reasonable... sounds like a pretty good optimizer, right?
But how do you know that you got the global minima? Can you prove it?
Now suppose that you have a second program, a symbolic mathematics program, and that program is capable of postulating new mathematical identities and proving them (or deciding they are false, or deciding they are too difficult for the program to prove.) And imagine you focus this program on the function to be optimized, and let it work on creating new mathematics with the goal of proving the properties that the global minima of the function would have, and using that to postulate the locations of potential global minima and try to prove which one is the best. And suppose this program might be able to find a proof of global minima in a mere four year — four thousand years at most.
Now if this second program runs and merely 3 years later proves that the minima is at the same location that the first 2 minute program suspected... then it follows that even though the second program was much much slower and (in this scenario) produced the same location, that this second program would be by-far the better optimization program.
The purpose of optimization is to find the most optimal result and to be certain that the result is the best. If it takes a few centuries to be certain that a proposed solution is as good as you get, then the knowledge that it is the global minima is more valuable than a fast but unproven result.
