I have the same questions when reading something like this. Expert verification seems more like an appeal to authority and intuition instead of a definite proof with formal rigorosity. Locally, there is always structure, but in pure mathematics even these steps require such an in depth understanding that trusting experts as an outsider seems to be impossible, it could as well be magic. As a programmer, I have a quite mechanistic understanding of the world, projects like http://us.metamath.org/index.html seem to make it much more understandable.

I'm wondering, if the longest path to the theorem "2 + 2 = 4" is 150 layers deep in this system, how deep would this proof be?