[noamyoungerm]

This is the type of question that quickly runs into problems wrt incompleteness, but there are a few key points that show that there are infinitely many theorems

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.

[grkvlt]

Since each theorem has a Gödel-number, there must be a function f(x) -> {0,1} where, when x is the number of an 'interesting' theorem, f(x) is 1, and otherwise it is 0. So, we just need to find this function (or rather, its Gödel number) and then we can iteratively feed all the integers to it, translating the interesting ones back into theorems.

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

and we're done!

I'll collect my Fields medal later, thanks.

[JadeNB]

Your condition `f(F) = 1` doesn't seem to do anything to distinguish your meta-theorem `F` from any other interesting theorem.

[digama]

You just defined a subset of the natural numbers, and asserted it has a Godel number. Sorry, there are uncountably many subsets of natural numbers and countably many Godel numbers, so there is no guarantee that this is possible. More subtly, you can consider many "natural" classes of functions, such as computable functions, recursively enumerable functions, etc. and for each such enumeration there will be a "natural" function that escapes the class. Functions to do with definability or (in this case) 'interestingness' are especially susceptible to this. See also "Tarski's theorem on the undefinability of truth".