Difference between 'true' and 'provable'
Solution 1:
The usual way to define truth is due to Tarski. Given a structure $M$ (i.e. a set with operations and relations), we recursively define $M \models \phi$, meaning $\phi$ is true in $M$. For concreteness, let's consider the natural numbers $N = (\mathbb N, +, \times, 0, 1, <)$:
-
$N \models a + b = c$ if it the output of the binary function $+$ on input $(a,b)$ is $c$. Similarly for $N \models a \times b = c$.
$N \models a < b$ if $(a,b)$ is in the set $\mathord< \mathbin{\subseteq} \mathbb N^2$.
$N \models \phi \land \psi$ if $N \models \phi$ and $N \models \psi$ and $N \models \phi \lor \psi$ if $N \models \phi$ or $N \models \psi$.
$N \models \neg \phi$ if it is not the case that $N \models \phi$.
$N \models \exists x \phi(x)$ if there is some $a \in \mathbb N$ so that $N \models \phi(a)$ and $N \models \forall x \phi(x)$ if for all $a \in \mathbb N$ we have $N \models \phi(a)$.
In other words, truth is defined exactly how you would expect; symbols in the language correspond to certain constants, functions, and relations in the structure and truth is based upon that connection.
Provability, on the other hand, isn't a property of structures. Instead, it's a property of theories. If $T$ is a theory, meaning a set of sentences in some fixed language, then we can define a provability relation $T \vdash \phi$. There are many ways to do the details here to match with our intuitive notion of provability. But the important things are that the provability relation should be closed under valid inference rules (e.g. if $T \vdash \phi$ and $T \vdash \phi \rightarrow \psi$, then $T \vdash \psi$), that the axioms of $T$ are provable (if $\phi \in T$ then $T \vdash \phi$), and that logical validities (statements true in any structure) are provable.
We can now ask about how provability and truth relate. Any definition of provability worth a damn will be sound. This means that if $M$ is a model of $T$ (i.e. every axiom of $T$ is true in $M$, when interpreted appropriately), then $T \vdash \phi$ implies $M \models \phi$. In other other words, if we have proved something, then we know it is true. Moreover, as Gödel showed, first-order logic is complete. This means that if every model $M$ of $T$ has $M \models \phi$, then $T \vdash \phi$.
On a final note, it's very common to see people refer to truth without indicating a structure they are working in or refer to provability without indicating a theory they are working from. In the former situation, it's usually clear what structure is implicitly being used. For instance, the statement "17 is prime" is referring to the natural numbers, and can be translated to a formal statement something like $N \models \forall x < 17\, \exists y \le 17 \ (x \times y = 17 \rightarrow x = 1)$.
In the latter situation, when referring to provability, some implicit background of commonly accepted mathematics is assumed. When we say that the intermediate value theorem is provable, we mean that there is a proof of the IVT from some commonly accepted basic principles.
Solution 2:
In math you need to start with a language with which to describe the objects of study. You can use set theory, type theory, etc. Then there will be a rigorous way to define "prime number". For example, "A number $x$ is prime if whenever $y$ divides $x$, $y$ must be $1$ or $x$." Then it is true that $17$ is prime. But, if we don't have a formalization of rules for deduction, we cannot prove that the number $17$ satisfies the definition we have for "prime".
Moreover, there are things we can state using the language of math that cannot be proven even given a formalized system of deduction. Since we can state them using the language of math, they must be true or false. We just can't deduce that truth value.