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. 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]: http://mathoverflow.net/a/152418/36970 [2]: http://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 [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/