People often say that the Gödel sentence G constructed in a formal system PA is true in the standard model $\mathbb{N}$ but unprovable in PA. Then when we ask how we established the truth of G in $\mathbb{N}$, I would say : by checking, in the model $\mathbb{N}$, some fact (the details of the Gödelian coding that gives us the meta-theoretic meaning of G, or the brute fact that G is true in $\mathbb{N}$).
But that checking is a mathematical proof, done in another formal system, say S (that could be some small fragment of ZFC). Of course, S cannot be PA itself.
So the truth of G in $\mathbb{N}$ (under the assumptions of the Gödel theorem) is a proven truth after all. The conclusion is : Gödel's theorems don't establish that we have an access to the truth of G without any formal proof (even if Gödel thought otherwise). On the contrary, in this case, any truth still rests on a formal proof in some system.
Is that reasoning correct ? I didn't find the precise answer in the past topics, but I could've missed something.
This is correct, but let me go into a bit more detail.
First, a remark about provability in formal systems. Any true statement is of course true in some formal system: namely, take it as an axiom! So there's no such thing as an "absolutely undecidable" statement in this sense. Of course, the real issue is whether a statement is decidable in some formal system we have reason to trust! And that's a much trickier issue, especially since we have degrees of trust: I trust ZFC, but I trust PA more.
Second, a remark about Goedel's theorem (as improved by Rosser) is actually provable in PA. What it states is:
This is outright provable in $PA$, no assumptions needed. (And, in fact, $PA$ is massive overkill in both places.)
Now let's bring those two points together. The point is that Goedel's theorem, provable in $PA$, gives us a machine for making us uncomfortable: the more we are confident in our current theory $T$, the more we believe the statement $G_T$ is true, and so the more we are impelled to move to a slightly stronger theory $T'$; and if we're not comfortable moving to a stronger theory, we are made less confident in $T$ itself. This basically yields a progression of increasingly strong theories (which has been studied very seriously). The philosophical conclusion of Goedel's Theorem is often stated as, "No single formal system is enough to decide all problems in math." While true, I think this slightly misses the point; a better version would be, "There is no degree of confidence with which we can decide all sentences, yet remain consistent." Whatever criteria you use to decide whether you trust a theory, we can use Goedel to construct sentences which are just slightly too hard to justify under those criteria - or, your criteria are too weak, and we can use them to justify anything.