For those who don't know much about computer-verified proofs, the way I'd sum it up is that there's a complexity crisis going on (similar to the "software crisis" which might not be completely solved but which has seen significant progress). And that Metamath Zero is one of the more promising projects out there aimed at this problem.