Question: Given an arbitrary powerful computer, is the nature of mathematics such that in principle we could exhaust the points in theorem space by brute force?
E.g. is there in principle a finite amount of math?
For any given statement P and any given theorem T, P OR T is a theorem, meaning you can generate infinitely many theorems from one.
More worryingly, there are infinitely many theorems that are true but impossible to prove. From Gödel's first incompleteness theorem, we know at least one such theorem must exist. Any theorem of the form Unprovable AND TRUE can be proved only if you can prove the unprovable theorem.
From a more general perspective, it's worth remembering that theorems can always be described as a finitely-long string of symbols in some formal logic system, and so running out of theorems to try and prove is like running out of strings.
This job is made much easier by the fact that the proof of this 'interestingness' theorem has a Gödel-number of its own; call it F. And, proving that something is interesting is obviously also interesting. So, just find the situation where:
f(F) = 1
I'll collect my Fields medal later, thanks.