Back in 1936, Kurt Gödel published his first mathematical mike-drop: “Our formal systems of logic can make statements that they can neither prove nor disprove.” In this chapter, you’ll learn what this famous theorem means, and you’ll learn a proof of it that builds upon Turing’s solution to the Halting Problem.