alt Hacker NewsThe problem with what you're saying is that any old random true proposition about the integers is not necessarily interesting enough to be called a theorem. GIT (or the uncomputability of the Busy Beaver problem) does not establish a limitation on proving theorems, but rather on determining whether a proposition is true or not. Most propositions are ugly and irrelevant. So GIT/Busy Beaver is irrelevant.
-----
Oh, and: All proofs are conditional on axioms. If those axioms are computably enumerable, then all of their consequences are computably enumerable too.
> Most propositions are ugly and irrelevant.
Most propositions may be ugly and irrelevant, but how do you know how many are not so and we just can't prove it? Also, what about stuff like Continuum Hypothesis, would you add it or not?