I remember reading the proof of his incompleteness theorem (or the portion of it that I had time to between classes). It's surprisingly approachable. AFAIR, he came up with a way to encode proofs as symbol sequences. Proofs that actually exist have finite representations. He then proved the theorem with that somehow. (Granted, I read it over a decade ago...)
You're thinking of Gödel numbering which is an elegant technique used extensively throughout that proof. He uses it to map logical symbols, statements and entire proofs to natural numbers and then proceeds to prove things about those statements and proofs by referring to them via their Gödel numbers.
