State of the progess of the automated proof checking
The mechanics of verifying proofs by computer is pretty much a solved problem. We have a good solid understanding of what a valid proof step is and how to recognize its validity by machine.
What is holding up the entire enterprise is that even though we have a good theory of the structure of proofs, computers cannot understands English, so the proofs we want them to check need to be translated into the formal language that the proof checker works with. The result often looks more like program source code than mathematical prose. This translation is not yet quite routine, but not an impenetrable black art either.
A problem is that there is a very large body of background knowledge that is generally assumed already known by mathematicians working at the research frontier. Before the proof checkers can begin dealing with contemporary results, all of that has to be transcribed. And the transcribing has to be done by people with a quite solid understanding of logic and mathematics -- who could easier find more interesting things to use their time for.
For some time, it has been possible to earn a Ph.D. by grabbing a suitable chunk of undergraduate mathematics and formalizing that in a computer proof system. But the novelty of that is going to wear off and eventually stop impressing Ph.D. committees (this may already have happened, for all I know). And then motivating people to do the work is going to be a real problem. It is not high-profile enough that funding bodies are likely to pay anyone to do the drudgery, not for a sufficient amount of work.
I think the general hope is that the development of result libraries will eventually be done through some kind of crowdsourcing, like open-source software. But what kind of reward structure would make that work is still to be seen.
Some complicated proofs have been verified by computer, the well known example in mathematics are:
the 4-colors theorem by Georges Gonthier and Benjamin Werner.
the Feit-Thompson theorem by Gy Georges Gonthier and its team.
the Kepler conjecture (Tomas Hales' theorem) by the flyspeck team.
There are other examples in Computer Science:
a C compiler: CompCert by Xavier Leroy
the functional correctness of a general-purpose operating system kernel by NICTA
As Henning explained the proof theory has already been well explored and it is quite clear how to check a formal proof.
But there are still many challenges:
how to exchange proofs between different systems
how to edit proof and check proof in wikipedia like environment
what is the best way to formalize some given concept
how to modify the proof assistant to allow a language closer to the usual mathematical language: overloaded notations, implicit steps in the proof, implicit coercions, how to deal with proofs by analogy or symmetry, ...
how to mix efficient computations and proofs
how to automate proofs
...