My understanding is that Godel's first theorem says that there is a sentence that is in a sense true in a formal system F but cannot be derived in that system.
I then hear that Godel actually goes on to construct such a sentence.
My question is, what would this even look like?
For example, in Peano Arithmetic would it be something like:
5 + 3 * 15 ... = ...? Is it long? Is it short? Could it be written on a piece of paper?
If not what is wrong with my thinking?