Has the Gödel sentence been explicitly produced?

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.


I have once played around with this stuff myself and obtained this example of such a sentence. The long thing at the end of that page (there are in fact two long things, just minor variants if I recall it correctly).


I was searching for an explicit representation of the Gödel sentence as well, and I found one today, only after reading your question here, so I share what I found: https://web.archive.org/web/20160528092209/http://tachyos.org/godel/Godel_number.html

Unfortunately it is not mentioned, what is the precise theory, what are the coding numbers of symbols, and what are the coding/decoding functions (hopefully these are consistent with Chaitin's book mentioned on right of the page), so the number is not really meaningful in its own, but at least gives an order of magnitude (if it is correct).