Best known theory for proving statements about natural numbers Gödel's incompleteness theorems imply that there is no consistent theory that can be effectively generated and contains all true statements about the natural numbers.
Well, what known consistent theory with recursively enumerable theorems can prove the most true statements about the natural numbers as defined by true arithmetic (or perhaps some other similar theory)? What's the best we can do?
 A: For brevity's sake, say that a theory $T$ is nice if $T$ is a consistent theory that can interpret Peano Arithmetic and admits a recursively enumerable set of axioms. For any such $T$, the statement "$T$ is consistent" can be coded as an arithmetic statement (saying that no number codes a proof of a contradiction from the axioms of $T$). What Gödel's theorem actually shows is that this statement is not provable in $T$.
This shows that there is no "best" theory or one that can do "the most" in the sense you describe, as given any true nice theory $T$ ("true" in the sense that all arithmetic consequences of $T$ are true in the standard model of arithmetic), $T$ +"$T$ is consistent" is also true and nice, and proves more arithmetic statements.
One could think of perhaps iterating this procedure and taking a limit. For any recursively enumerable sequence of true nice theories, however, one can find another theory $T$ that is also nice and true, and proves all the arithmetic statements that the theories in the sequence prove, so we can again go beyond this "limit" as in he previous paragraph.
(A good reference for these topics is "Aspects of Incompleteness" by Per Lindström.)
In fact, note how frustrating (?) the situation is, in that the sentence we found that the theory cannot prove is $\Pi^0_1$, as simple as possible in the natural complexity hierarchy. As explained in the book "Metamathematics of first-order arithmetic" by Petr Hájek and Pavel Pudlák, even adding to PA all its true $\Pi^0_1$ consequences (and therefore losing that it is r.e.) does not give us a complete theory. Many natural (combinatorial) examples of independent statements (on hydra games, Goodstein sequences, etc) are independent of this theory, and are $\Pi^0_2$, as simple as possible.
Gödel proved some very nice speed-up theorems, discussed in detail by Samuel Buss, see the relevant papers on his page: "On Gödel's theorems on lengths of proofs I: Number of lines and speedups for arithmetic", Journal of Symbolic Logic 39 (1994) 737-756; and "On Gödel's theorems on lengths of proofs II: Lower bounds for recognizing k symbol provability", in Feasible Mathematics II, P. Clote and J. Remmel (eds), Birkhauser, 1995, pp. 57-90.
What these theorems say is that not only the theory $T$+"$T$ is consistent" proves more arithmetic statements, but there are proofs in $T$ that require an absurd number of steps and can be proved very quickly in the new theory, so even if we cannot find a "best" theory, there is a point in looking for "better" ones.
In the comments to the question I see that large cardinals are suggested. Any particular large cardinal axiom we adopt beyond ZFC (that does not result in an inconsistent theory) will result in a theory to which Gödel's theorem applies, and so it can be transcended just as before. But there is a point to the program of extending ZFC with large cardinals. For example, we have deep theorems explaining how the arithmetic consequences of a large cardinal axiom $A$ are extended by those of a large cardinal axiom $B$ precisely if $B$ is in "consistency strength" stronger than $A$. These theorems (for the large cardinals studied so far) suggest clear lines along which to continue research on large cardinals (for example, we expect this feature to be continued by all further large cardinal axioms people may suggest in the future). There are much stronger "absoluteness" and "correctness" results associated with large cardinal axioms as well. Some of them are discussed at length in some questions at MO, see for example this one.
