This is true, obviously, but I can reassure you that the actual proof is very technical and long. Back in college I took a logic class that spent almost the ent

This is true, obviously, but I can reassure you that the actual proof is very technical and long. Back in college I took a logic class that spent almost the entire semester going over this proof, in its shortened form i.e. using Rosser's trick. By using Rosser's trick one can prove a more general Incompleteness theorem (based on Q) and more elegantly. It ends up stating very concisely that a theory cannot be all 3 of (any 2 or 1 or 0 is fine): * axiomatizable extension of Q * consistent * complete (where Q is a minimalistic arithmetical theory that can do addition and multiplication: https://en.wikipedia.org/wiki/Robinson_arithmetic https://en.wikipedia.org/wiki/Robinson_arithmetic) It's true that the "main idea" of the proof is "everything is a natural number", which is obvious to us programmers (it possibly wasn't obvious to anyone in Godel's time). However, this is by no means the only trick that's used in the proof.