A Gödel encoding is a way of using the formal machinery of proving theorems in arithmetic to discuss that very machinery. Kurt Gödel rocked the world of mathematics in 1931 by showing that this was possible, and that it had surprising consequences for the sort of things that could ever be formally proven in a given system.

The original formulation of this self-referential framework was really messy (involving prime factorizations of huge numbers), but we can think about it more easily now by thinking about computer programs. In order to get mathematical statements that refer to themselves, we can first show that we can talk interchangeably about mathematical proofs and computer programs, and then show how to write computer programs that refer to themselves.

To be specific about the machinery of proving theorems, we'll use the formal system of Peano Arithmetic.

What kind of self-reference do we want for our computer program? We would like to be able to write a program that takes its own source code and performs computations on it. But it doesn't count for the program to access its own location in memory; we'd like something we could write directly into an interpreter, with no other framework, and get the same result.

This kind of program is known as a quine.

Gödel encoding is equivalent to an encoding of a computer program as a binary string.

If we think about any conjecture in mathematics that can be stated in terms of arithmetic, you can write a program that loops over all possible strings, checks whether any of them is a valid proof of the conjecture, and halts if and only if it finds one. In the other direction, we can imagine proving a theorem about whether a particular computer program ever halts.