The incompleteness theorem can be proved in a few lines given the right definitions up front. It's basically the same as the undecidability of the halting prob

The incompleteness theorem can be proved in a few lines given the right definitions up front. It's basically the same as the undecidability of the halting problem, which has a proof that is written as a poem: https://introcs.cs.princeton.edu/java/54computability/halting-poem.html https://introcs.cs.princeton.edu/java/54computability/haltin... There is a wonderful book by Torkel Franzén about the incompleteness theorem that is 100+ pages, but it is not purely about the proof. It's a popularization that discusses bogus ways philosophers have interpreted the theorem, and stuff like that. It is called "Gödel's Theorem: An Incomplete Guide to its Use and Abuse". Meanwhile Aschbacher and Smith's proof of the classification of quasithin groups really is a book of 1200+ pages: https://books.google.com/books?id=SbO2irSQHMEC https://books.google.com/books?id=SbO2irSQHMEC And of course the proof of the classification of finite simple groups has afaik never been published all in one place, though there are some book-length expositions of it referring back to the original papers. It is a set of papers spanning around 20 years and adding up to around 10,000 pages. It is sometimes called "the enormous theorem": https://en.wikipedia.org/wiki/Enormous_theorem https://en.wikipedia.org/wiki/Enormous_theorem