This question sums up the distinction between syntax and semantics. Proof is a syntactic notion, truth is semantic. Syntax concerns formal theories, semantics concerns structures.
In the simplest cases, a formal theory consists of a finite set of symbols (the vocabulary), plus rules specifying when a string of symbols is syntactically correct (a so-called formula), which formulas are axioms, and when a formula follows from other formulas (rules of inference). Key point: all this should be purely mechanical, and in principle programmable. Example: $$\forall x\exists y(x\cdot y=1)$$ is an axiom in the formal theory of groups.
A formula in a formal theory is provable if there is a finite list of formulas, such that every formula in the list is either an axiom, or follows by a rule of inference from earlier formulas on the list.
To define the notion of structure, we need a bit of set-theory. A structure for a theory consists of a set called the domain (or universe) of the structure, and enough relations, functions, and individuals in this domain to give meaning to the formulas of the theory. For example, a structure for the formal theory of a group consists of a set $G$ and a function $G\times G\rightarrow G$ (an 'operation') that interprets the symbol '$\cdot$' of the theory; also an individual element of $G$ that interprets '1'.
Tarski gave a definition of 'truth' (or 'satisfaction') for a class of theories known as first-order theories. If $T$ is a first-order theory, and $S$ is a structure for it, then Tarski defined the notion of "$\varphi$ is true in $S$", where $\varphi$ is a formula of $T$ (strictly speaking, a so-called closed formula of $T$).
If all the axioms of $T$ are true in a structure $S$, we say $S$ is a model of $T$.
Tarski's definition is inductive, i.e., truth for longer formulas is defined in terms of truth for shorter formulas. For example $\varphi\&\psi$ is defined to be true in $S$ if and only if both $\varphi$ and $\psi$ are true in $S$.
I'm leaving out gobs of details, which can be found easily in a zillion textbooks (or in my notes Basics of First-order Logic at diagonalargument.com). But I should add a few more generalities.
First, it's not possible to "get off the ground" without relying on an informal level of understanding. For example, Tarski's formal definition of the meaning of '$\varphi\&\psi$' assumes you understand the meaning of the word 'and'. Likewise, a certain amount of informal set theory must be taken for granted. (Set theory itself can be formalized as a first-order theory, but that doesn't erase the issue, just pushes it one level back.)
Second, the most famous example of a "true but unprovable" statement is the so-called Gödel formula in Gödel's first incompleteness theorem. The theory here is something called Peano arithmetic (PA for short). It's a set of axioms for the natural numbers. The so-called standard model for PA is just the usual natural numbers with the usual operations of addition and multiplication and the usual individual elements 0 and 1.
The Gödel formula cannot be proved in PA (if PA is a consistent theory, which most mathematicians believe). But you can give a convincing argument that the formula is true in the standard model. This proof of this argument uses notions from set theory, and cannot be formalized in PA. It can be formalized in other formal theories, however.