Just finished a book club for Gödel, Escher, Bach, which gives a lay -- but pretty detailed and thorough -- explanation of the proof. Here's how I'd say lay out

Just finished a book club for Gödel, Escher, Bach, which gives a lay -- but pretty detailed and thorough -- explanation of the proof. Here's how I'd say lay out the key insights as they applied to the parts I didn't understand before. You want to use pure math to say "this statement cannot be proven". To do that, you: 1) Express the concept of statements following from other strings by the axioms or other theorems. 2) Express the concept of "this is a valid chain of statements, each of which follows from the previous". (GEB calls it a proof-pair.) 3) Express the concept of "Statement A does not have such a valid chain" (there exists no such chain with A at the end). That allows you to say "Statement A cannot be proven." From that point, it's a matter of extending it to the statement (call it G): "There exists a statement S such that S has no proof and S statisfies criteria A/B/C." ...and then constructing the criteria A/B/C such that G is the one statement that can satisfy it. The details of how you construct the criteria so that you are specifying G are the Gödel numbering that the Quanta article describes.