Let $S$ be a "rich enough" theory such as Peano arithmetic or ZFC ; assume that we have a complete formalization of the theory of $S$ so that we may talk about Godel numbers and the length of a proof.
Godel's sentence is constructed so that it says "I am not provable from S". Now let $n$ be a fixed integer, and consider a sentence $\phi_n$ formed likewise that says "I am not provable in at most $n$ steps from S". Then $\phi_n$ is a true statement, and if $\phi_n$ has a proof from $S$ this proof has length at least $n$. What is not clear is whether $\phi_n$ is provable from $S$. Does the answer to that question depend on the formalization we initially choose ?