I often read that the proof of the first incompleteness theorem works by exhibiting a true statement (more precisely one that states its own unprovability) that is not provable. However, this is different from what I read in my textbook by Cori and Lascar.
In the textbook, the first incompleteness theorem is a consequence of the following results:
Corollary 6.27 If the theory $T$ is complete and recursive, then it is decidable.
Theorem 6.28 Let $T$ be a consistent theory that extends $\mathcal{P}_0$; then $T$ is undecidable.
The first incompleteness theorem is stated as:
Theorem 6.30 Let $T$ be a consistent recursive theory that includes $\mathcal{P}_0$, then $T$ is not complete. In particular, $\mathcal{P}$ is incomplete.
After reading the proofs, I am only convinced that $T$ satisfying the hypothesis in Theorem 6.30 is incomplete, but I do not know how to construct any specific formula that is not provable in $T$. There is a formula $G$ contructed in the proof of Theorem 6.28 that states $G[\#G]$ is not derivable, however, this is part of the proof by contradiction. Such a formula $G$ exists under the hypothesis that $T$ is decidable. And therefore it is not an example of a unprovable formula in a theory $T$ that satisfy the conditions of Theorem 6.30.
Yes, lots of books prove this theorem without explicitly constructing such a sentence. If you want an explicit sentence, the idea is to come up with a sentence $G$ such that $$ T\vdash G\leftrightarrow \lnot Pr_T(\ulcorner G\urcorner),$$ where $Pr_T$ is the provability predicate for $T.$ This is an instance of the diagonal lemma, which says that for any arithmetical predicate $F$ there is a sentence $S$ such that $T\vdash S\leftrightarrow F(\ulcorner S\urcorner).$ The diagonal lemma is constructive (see the proof), so you actually do get an explicit sentence.
If $T$ is a consistent extension of Robinson arithemetic, $T$ does not prove $G,$ since if it proved $G,$ then there would be an explicit proof that could be used within $T$ to prove $Pr_T(\ulcorner G\urcorner).$ But also, $T\vdash \lnot Pr_T(\ulcorner G\urcorner),$ since $T\vdash G$ and $T\vdash G\leftrightarrow \lnot Pr_T(\ulcorner G\urcorner),$ so $T$ is inconsistent. And if $T$ is an $\omega$-consistent extension of Robinson arithmetic, $G$ is not disprovable since if $T\vdash \lnot G,$ then $T\vdash Pr_T(\ulcorner G\urcorner)$ which means it proves there is a witness to a computable property (i.e. a number that is the Godel number of a proof of $G$) when there is in fact no such witness (since $T$ is consistent and proves $\lnot G$), and thus $T$ is $\omega$-inconsistent.
Needing to assume $\omega$-consistency was one of the drawbacks of Gödel's original proof. It can be improved to plain consistency by diagonalizing a slightly more complicated formula, something known as Rosser's trick.