I wonder if anyone has written out a Gödel sentence in full as a statement about numbers in English. It would be fun to see how big it gets. Also, the comment

I wonder if anyone has written out a Gödel sentence in full as a statement about numbers in English. It would be fun to see how big it gets. Also, the comment about size and diagonalization is interesting. The Gödel sentence from the first incompleteness theorem is made by diagonalizing, while the sentence from the second incompleteness theorem is just "Con(T)", so the sentence from the 2nd theorem is shorter and more natural if written out in full---making it even more disappointing that it's not provable. Indeed, if we put in more work we should be able to prove a more interesting theorem, but I never really thought about it before.