I do not pretend to know much about mathematical logic. But my curiosity was piqued when I read Hofstadter's Gödel, Escher, Bach, which tries to explain the proof of Gödel's first incompleteness theorem by using an invented formal system called TNT--Typographical Number Theory.
Hofstadter shows how we are able to construct an undecidable TNT string, which is a statement about number theory on one level, and asserts its own underivability within TNT on another level.
My question is: Has this statement about number theory, call it the Gödel sentence, ever been explicitly found? Of course, it would be enormously long. But it seems possible to write a computer program to print it out. I know what is important is that such a string exists, but it would be fun to see the actual string, and it seems like a nice coding problem.
Forgive me if this is a naïve question.