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].

[[6]]: http://www.ams.org/notices/200811/tx081101382p.pdf (I can't get this link to work as a footnote ???)