Do we know if there exist true mathematical statements that can not be proven? Given the set of standard axioms (I'm not asking for proof of those), do we know for sure that a proof exists for all unproven theorems? For example, I believe the Goldbach Conjecture is not proven even though we "consider" it true.

Phrased another way, have we proven that if a mathematical statement is true, a proof of it exists? That, therefore, anything that is true can be proven, and anything that cannot be proven is not true? Or, is there a counterexample to that statement?

If it hasn't been proven either way, do we have a strong idea one way or the other? Is it generally thought that some theorems can have no proof, or not?
Relatively recent discoveries yield a number of so-called 'natural
independence' results that provide much more natural examples
of independence than does Gödel's example based upon
the liar paradox (or other syntactic diagonalizations).
As an example of such results, I'll sketch a simple example due
to Goodstein of a concrete number theoretic theorem whose proof
is independent of formal number theory PA (Peano Arithmetic) (following [Sim]).

Let $\,b\ge 2\,$ be a positive integer. Any nonnegative integer $n$
can be written uniquely in base $b$ 
$$\smash{n\, =\, c_1 b^{\large n_1} +\, \cdots + c_k b^{\large n_k}} $$

where $\,k \ge 0,\,$ and  $\, 0 &lt; c_i  &lt; b,\,$ and $\, n_1  &gt; \ldots &gt; n_k
\ge 0,\,$ for $\,i = 1, \ldots, k.$

For example the base $\,2\,$ representation of $\,266\,$ is
$$266 = 2^8 + 2^3 + 2$$

We may extend this by writing each of the exponents $\,n_1,\ldots,n_k\,$
in base $\,b\,$ notation, then doing the same for each of the exponents
in the resulting representations, $\ldots,\,$ until the process stops.
This yields the so-called 'hereditary base $\,b\,$ representation of $\,n$'.
For example the hereditary base $2$ representation of $\,266\,$ is
$$\smash{266 = 2^{\large 2^{2+1}}\! + 2^{2+1} + 2} $$

Let $\,B_{\,b}(n)$ be the nonnegative integer which results if we take the
hereditary base $\,b\,$ representation of $\,n\,$ and then syntactically
replace
each $\,b\,$ by $\,b+1,\,$ i.e. $\,B_{\,b}\,$ is a base change operator
that 'Bumps the Base'
from $\,b\,$ up to $\,b+1.\,$ For example bumping the base from $\,2\,$ to
$\,3\,$ in the prior equation yields
$$\smash{B_{2}(266) = 3^{\large 3^{3+1}}\! + 3^{3+1} + 3\quad\ \ \ }$$

Consider a sequence of integers obtained by repeatedly applying
the operation:  bump the base then subtract one from the result.
For example, iteratively applying this operation to $\,266\,$ yields
$$\begin{eqnarray}
266_0 &amp;=&amp;\ 2^{\large 2^{2+1}}\! + 2^{2+1} + 2\\
266_1 &amp;=&amp;\ 3^{\large 3^{3+1}}\! + 3^{3+1} + 3 - 1\ =\ B_2(266_0) - 1 \\
    ~ \ &amp;=&amp;\ 3^{\large 3^{3+1}}\! + 3^{3+1} + 2 \\
266_2 &amp;=&amp;\ 4^{\large 4^{4+1}}\! + 4^{4+1} + 1\qquad\! =\ B_3(266_1) - 1 \\
266_3 &amp;=&amp;\ 5^{\large5^{5+1}}\! + 5^{5+1}\phantom{ + 2}\qquad\   =\ B_4(266_2) - 1 \\
266_4 &amp;=&amp;\ 6^{\large 6^{6+1}}\! + \color{#0a0}{6^{6+1}\! - 1}  \\
    ~ \ &amp;&amp;\ \textrm{using}\quad  \color{#0a0}{6^7\ -\,\ 1}\ =\ \color{#c00}{5555555}\, \textrm{ in base } 6 \\
    ~ \ &amp;=&amp;\ 6^{\large 6^{6+1}}\! + \color{#c00}5\cdot 6^6 + \color{#c00}5\cdot 6^5 + \,\cdots + \color{#c00}5\cdot 6 + \color{#c00}5 \\
266_5 &amp;=&amp;\ 7^{\large 7^{7+1}}\! + 5\cdot 7^7 + 5\cdot 7^5 +\, \cdots + 5\cdot 7 + 4 \\
&amp;\vdots &amp; \\
266_{k+1} &amp;=&amp; \ \qquad\quad\ \cdots\qquad\quad\ = \ B_{k+2}(266_k) - 1 \\
\end{eqnarray}$$

In general, if we start this procedure at the integer $\,n\,$ then
we obtain what is known as the Goodstein sequence starting at $\,n.$

More precisely, for each nonnegative integer $\,n\,$ we recursively define
a sequence of nonnegative integers $\,n_0,\, n_1,\, \ldots ,\,
n_k,\ldots\,$ by
$$\begin{eqnarray}
n_0\ &amp;:=&amp;\ n \\
n_{k+1}\ &amp;:=&amp;\
\begin{cases}
B_{k+2}(n_k) - 1 &amp;\mbox{if }\ n_k &gt; 0 \\
\,0 &amp;\mbox{if }\ n_k = 0
\end{cases} \\
\end{eqnarray}$$

If we examine the above Goodstein sequence for $\,266\,$ numerically
we find that the sequence initially increases extremely rapidly:

$$\begin{eqnarray}
2^{\large 2^{2+1}}\!+2^{2+1}+2\ &amp;\sim&amp;\ 2^{\large 2^3} &amp;\sim&amp;\,  3\cdot 10^2 \\
3^{\large 3^{3+1}}\!+3^{3+1}+2\ &amp;\sim&amp;\ 3^{\large 3^4} &amp;\sim&amp;\,  4\cdot 10^{38} \\
4^{\large 4^{4+1}}\!+4^{4+1}+1\ &amp;\sim&amp;\ 4^{\large 4^5} &amp;\sim&amp;\,  3\cdot 10^{616} \\
5^{\large 5^{5+1}}\!+5^{5+1}\ \ \phantom{+ 2}  \ &amp;\sim&amp;\ 5^{\large 5^6} &amp;\sim&amp;\,  3\cdot
10^{10921} \\
6^{\large 6^{6+1}}\!+5\cdot 6^{6}\quad\!+5\cdot 6^5\ \:+\cdots +5\cdot 6\ \ +5\
&amp;\sim&amp;\ 6^{\large 6^7} &amp;\sim&amp;\,  4\cdot 10^{217832} \\
7^{\large 7^{7+1}}\!+5\cdot 7^{7}\quad\!+5\cdot 7^5\ \:+\cdots +5\cdot 7\ \ +4\
&amp;\sim&amp;\ 7^{\large 7^8} &amp;\sim&amp;\,  1\cdot 10^{4871822} \\
8^{\large 8^{8+1}}\!+5\cdot 8^{8}\quad\!+5\cdot 8^5\ \: +\cdots +5\cdot 8\ \ +3\
 &amp;\sim&amp;\ 8^{\large 8^9} &amp;\sim&amp;\,  2\cdot 10^{121210686} \\
9^{\large 9^{9+1}}\!+5\cdot 9^{9}\quad\!+5\cdot 9^5\ \: +\cdots +5\cdot 9\ \ +2\
&amp;\sim&amp;\ 9^{\large 9^{10}} &amp;\sim&amp;\,  5\cdot 10^{3327237896} \\
10^{\large 10^{10+1}}\!\!\!+5\cdot 10^{10}\!+5\cdot 10^5\!+\cdots +5\cdot 10+1\ &amp;\sim&amp;\
10^{\large 10^{11}}\!\!\!\! &amp;\sim&amp;\,  1\cdot 10^{100000000000} \\
\end{eqnarray}$$

Nevertheless, despite numerical first impressions, one can prove that this
sequence converges to $\,0.\,$ In other words, $\,266_k = 0\,$ for all
sufficiently large $\,k.\,$ This surprising result is due to Goodstein
$(1944)$ who actually proved the same result for all Goodstein
sequences:

Goodstein's Theorem $\ $  For all $\,n\,$ there exists $\,k\,$ such
that $\,n_k = 0.\,$
In other words, every Goodstein sequence converges to $\,0.$

The secret underlying Goodstein's theorem is that hereditary
expression of $\,n\,$ in base $\,b\,$ mimics an ordinal notation for
all ordinals less than epsilon nought $\,\varepsilon_0 = \omega^{\large \omega^{\omega^{\Large\cdot^{\cdot^\cdot}}}}\!\!\! =\, \sup \{ \omega,\, \omega^{\omega}\!,\, \omega^{\large \omega^{\omega}}\!,\, \omega^{\large \omega^{\omega^\omega}}\!,\, \dots\, \}$. For such
ordinals, the base bumping
operation leaves the ordinal fixed, but subtraction of
one decreases the ordinal. But these ordinals are well-ordered, which allows us to conclude that a Goodstein sequence
eventually converges to zero. Goodstein actually proved his
theorem for a general increasing base-bumping function $\,f:\Bbb N\to \Bbb
N\,$
(vs. $\,f(b)=b+1\,$ above). He proved that convergence of all such
$f$-Goodstein sequences is equivalent to transfinite induction
below  $\,\epsilon_0.$

One of the primary measures of strength for a system of logic is
the size of the largest ordinal for which transfinite induction
holds. It is a classical result of Gentzen that the consistency
of PA (Peano Arithmetic, or formal number theory) can be proved
by transfinite induction on ordinals below $\,\epsilon_0.\,$ But we know
from Godel's second incompleteness theorem that the consistency
of PA cannot be proved in PA.  It follows that neither can
Goodstein's theorem be proved in PA. Thus we have an example of
a very simple concrete number theoretical statement in PA whose
proof is nonetheless independent of PA.

Another way to see that Goodstein's theorem cannot be proved in PA
is to note that the sequence takes too long to terminate, e.g.

$$ 4_k\,\text{ first reaches}\,\ 0\ \,\text{for }\, k\, =\,
3\cdot(2^{402653211}\!-1)\,\sim\, 10^{121210695}$$

In general, if 'for all $\,n\,$ there exists $\,k\,$ such that $\,P(n,k)$'
is
provable, then it must be witnessed by a provably computable
choice function $\,F\!:\, $ 'for all $\,n\!:\ P(n,F(n)).\,$'  But the
problem
is that $\,F(n)\,$ grows too rapidly to be provably computable in PA,
see [Smo] $1980$ for details.

Goodstein's theorem was one of the first examples of so-called
'natural independence phenomena', which are considered by most
logicians to be more natural than the metamathematical
incompleteness results first discovered by Gödel. Other finite
combinatorial examples were discovered around the same time,
e.g. a finite form of Ramsey's theorem, and a finite form of
Kruskal's tree theorem, see [KiP], [Smo] and [Gal]. [Kip]
presents the Hercules vs. Hydra game, which provides an
elementary example of a finite combinatorial tree theorem
(a more graphical tree-theoretic form of Goodstein's sequence).

Kruskal's tree theorem plays a fundamental role in computer
science because it is one of the main tools for showing that
certain orderings on trees are well-founded. These orderings
play a crucial role in proving the termination of rewrite rules
and the correctness of the Knuth-Bendix equational completion
procedures. See [Gal] for a survey of results in this area.

See the references below for further details, especially
Smorynski's papers. Start with Rucker's book if you know no
logic, then move on to Smorynski's papers, and then the others,
which are original research papers. For more recent work, see
the references cited in Gallier, especially to Friedman's school
of 'Reverse Mathematics', and see [JSL].

References

[Gal] Gallier, Jean. What's so special about Kruskal's theorem and the ordinal $\Gamma_0$?
A survey of some results in proof theory,
Ann. Pure and Applied Logic, 53 (1991) 199-260.

[HFR] Harrington, L.A. et.al. (editors)
Harvey Friedman's Research on the Foundations of Mathematics,  Elsevier 1985.

[KiP] Kirby, Laurie, and Paris, Jeff.
Accessible independence results for Peano arithmetic,
Bull. London Math. Soc., 14 (1982), 285-293.

[JSL] The Journal of Symbolic Logic,* v. 53, no. 2, 1988
 This issue contains papers from the Symposium "Hilbert's
 Program Sixty Years Later".

[Kol] Kolata, Gina. Does Goedel's Theorem Matter to Mathematics?
Science 218 11/19/1982, 779-780; reprinted in [HFR]

[Ruc] Rucker, Rudy. Infinity and The Mind, 1995, Princeton Univ. Press.

[Sim] Simpson, Stephen G. Unprovable theorems and fast-growing functions,
Contemporary Math. 65 1987, 359-394.

[Smo] Smorynski, Craig. (all three articles are reprinted in [HFR])
Some rapidly growing functions, Math. Intell., 2 1980, 149-154.
The Varieties of Arboreal Experience, Math. Intell., 4 1982, 182-188.
"Big" News from Archimedes to Friedman, Notices AMS, 30 1983, 251-256.

[Spe] Spencer, Joel. Large numbers and unprovable theorems,
Amer. Math. Monthly, Dec 1983, 669-675.
Euclid's fifth postulate:

Two lines are drawn which intersect a third in such a way that the sum of the inner angles on one side is less than two right angles, then the two lines inevitably must intersect each other on that side if extended far enough. This postulate is equivalent to what is known as the parallel postulate.

Euclid's fifth postulate cannot be proven as a theorem, although this was attempted by many people. Euclid himself used only the first four postulates ("absolute geometry") for the first 28 propositions of the Elements, but was forced to invoke the parallel postulate on the 29th. In 1823, Janos Bolyai and Nicolai Lobachevsky independently realized that entirely self-consistent "non-Euclidean geometries" could be created in which the parallel postulate did not hold. (Gauss had also discovered but suppressed the existence of non-Euclidean geometries.)