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.