Look for theorems that have been, or are currently, the subject of major formalization efforts! The two highest-rated answers as I write this [[1],[2]] -- concerning the Four-Color and Feit-Thompson theorems -- don't mention a *major* point in the history of those theorems: proofs of both theorems have been *completely formalized in the Coq proof assistant* in the last ten years: the Four-Color Theorem in 2005 [[3]] and the Feit-Thompson Theorem in 2012 [[4]], with both developments led by George Gonthier [[7]] of Microsoft Research, Cambridge. I believe both of these theorems were chosen for formalization efforts precisely because the existing proofs were so large and complicated that it was considered impossible for a single individual to understand them completely and convincingly. **UPDATE**: as pointed out in the comments, I am wrong about the difficulty of the Feit-Thompson theorem. Rather, its original proof runs "only" about 250 pages and [[12]]: > “The Feit-Thompson Theorem,” Gonthier says, “is the first steppingstone in a much larger result, the classification of finite simple groups, which is known as the ‘monster theorem’ because it’s one of those theorems where belief in it resides in the belief of a few selected people who have understanding of it.” This is particularly significant for the Four-Color Theorem: while the theorem reducing the problem to finitely many cases was peer reviewed in the original 1976 computer-assisted proof [[5]], the computer code which checked the finitely many cases in the 1976 proof was not peer reviewed [[6]] -- indeed the effort to peer review was abandoned after much effort, because the code was judged too long and complex [[6]]. Contrast this with the 2005 proof: going far beyond peer review, the code has been completely formalized, meaning a specification stating what the code should do has been given -- it should check the finitely many cases correctly -- and they have proven that their code meets that specification. This is an amazing achievement! The AMS Notices article about the formalization of the Four Color Theorem -- taken from a special issue of the Notices devoted to computer-aided formal proof [[9]] -- provides a fascinating history of the proof and discussion of the formalization, along with an introduction to computer-aided formal proof for the non-specialist. The Coq proof assistant [[8],[10]] is a system for constructing and checking completely formal proofs on the computer. Another of it's major success stories is the formalization of an optimizing C compiler [[11]]. [1]: https://mathoverflow.net/a/152418/36970 [2]: https://mathoverflow.net/a/152412/36970 [3]: https://research.microsoft.com/en-us/people/gonthier/4colproof.pdf [4]: http://happyproving.blogspot.com/2012/10/georges-gonthier-completes-formal-proof.html [5]: http://projecteuclid.org/DPubS?service=UI&version=1.0&verb=Display&handle=euclid.bams/1183538218 [[6]]: http://www.ams.org/notices/200811/tx081101382p.pdf (I can't get this link to work as a footnote ???) [7]: https://en.wikipedia.org/wiki/Georges_Gonthier [8]: http://coq.inria.fr/a-short-introduction-to-coq [9]: http://www.ams.org/notices/200811/ [10]: https://en.wikipedia.org/wiki/Coq [11]: http://compcert.inria.fr/ [12]: https://research.microsoft.com/en-us/news/features/gonthierproof-101112.aspx