Gödel's First Incompleteness Theorem is based on the construction of a formula - a so-called Gödel formula - stating its own unprovability. Has ever such a formula led to novel insights in number theory (beside arithmetics' incompleteness)?
Intuitively, a Gödel formula would be an excellent candidate as an additional axiom which, even though not making arithmetics' axiomatization complete, would most likely result in novel and interesting theorems.
To the best of my knowledge, this path has so far not been followed. Am I right or were number theoretical results gained from exploiting a Gödel formula?
The incompleteness theorem has led to interesting discoveries such as the unprovability of the Paris-Harrington principle and similar principles in Peano arithmetic.
However, it doesn't help us much to include the Gödel sentence for PA as a new axiom, because number theorists do not limit themselves to Peano Arithmetic - they are generally interested simply in proving results, not proving them in Peano Arithmetic. For example, the Paris-Harrington theorem is simple to prove in ZFC, so number theorists would typically just view it as a particular (and simple) combinatorial theorem.
Logicians have been very interested in what is provable in systems of arithmetic, but they rarely develop genuinely "new" theorems of number theory while doing so. Part of this is because they are generally interested in theorems that are both independent of PA (for example) and also provable in general - but once a result is provable in general, non-logicians are less interested in whether it is provable in PA.
One way that we could try to prove genuinely new number theory results would be to add axioms to ZFC, rather than PA. That might increase the number of results that I am calling provable "in general".
When people do talk about adding additional axioms beyond ZFC, they typically include axioms that imply Gödel-type sentences, but are much stronger than Gödel sentences themselves. Many of these additional axioms are "large cardinal" axioms in set theory. But even these don't seem to have much practical effect on everyday number theory, etc., although they do let us prove additional statements of a more set-theoretic flavor.