I have a difficulty understanding Gödel's incompleteness theorems. If it is proven semantically that some problem is undecidable (such as Halting problem), does it means that such a statement is "true but unprovable"? Or does Gödel's incompleteness theorems talk about some different sense of "a statement that is true but unprovable"? If so, how mathematicians call this property of a proof to be valid in semantical sense (meaning having an informal mathematical proof) but unprovable in formal proof sense, such as Halting problem?
(note: By Halting problem I mean a proven statement by Alan Turing which says: "A general algorythm to solve the halting problem for all possible program-input pairs cannot exist.")
There are two notions of "undecidable" here: a single sentence $\varphi$ being undecidable relative to a specific theory $T$, meaning that neither $\varphi$ nor $\neg\varphi$ is provable in $T$, and a decision problem $D$ being undecidable in an absolute sense, meaning that $D$ is a set of natural numbers which is not computable.
To avoid this confusion, I'll refer to these notions as "independence over $T$" and "noncomputability" respectively.
There are similarities between the two notions, but they are still fundamentally different. In particular, while the decision problem we call "the halting problem" is noncomputable, the sentence "The halting problem is noncomputable" is quite easily provable in (say) first-order Peano arithmetic $\mathsf{PA}$. That is: Turing's theorem about the halting problem is not an example of a sentence which is independent over any of the usual theories we consider in this context.
Godel's (first) incompleteness theorem says that no "appropriate theory" can be both consistent and complete. Roughly speaking, the proof describes a procedure according to which, given an appropriate $T$, we produce a sentence $\varphi$ which is true and independent over $T$ if $T$ is consistent.
This takes us to your additional question
The crucial part is the bolded "if." Within $T$ we can define $\varphi$ and prove that if $T$ is consistent then $\varphi$ is true and independent over $T$; however, $T$ won't be able to prove its own consistency and so this conditional result is the best $T$ is able to do.
The "informal mathematical proof" that the sentence $\varphi$ associated to a theory $T$ is true does indeed correspond to a formal mathematical proof, but not a proof in the system $T$ - rather, a proof in the stronger system $T$+"$T$ is consistent."
As an aside, we can indeed prove the first incompleteness theorem via computability-theoretic means, but it's a bit harder than just observing the undecidability of the halting problem: unless we want to add an unecessary hypothesis on the theory in question ("$\Sigma^0_1$-soundness"), we have to use a somewhat more technical result. The usual one is the existence of computably inseparable c.e. sets.