> Brute searching all possible mathematical constructs, theorems, etc. to see which one fits the problem would probably take you practiacally an infinite amount of time.

That's not the kind of search which is being done. Read this paper: https://doi.org/10.1023/A:1006171315513