Way back in 1990 I started a Phd at Cambridge University Computer Laboratory in the area of automated theorem proving. My interest at the time was around the synthesis of functional programs from mathematical proofs of their correctness, but I remember that one of the groups at the computer laboratory was interested in implementing the real numbers in one of the programming logics that they used (HOL). Since those days, things have moved on a lot, and in 2008 Georges Gronthier published his computer checked proof of the four colour theorem. More impressively, he and a team have recently finished a proof of the Feit-Thompson Theorem, a complicated result from group theory.Of course, another long term computer proof attempt is the Flyspeck project, the formalisation of Thomas Hales’ proof of the Kepler conjecture which is also nearing completion.
There’s an interesting page here which records 100 mathematical theorems that have been proved in a range of theorem provers and it will be interesting to see how far the formalisation of mathematics will go in the coming years, and how many holes they find in the existing proofs in the process!