Huh. Looking at it, they have made a lot more progress than I was aware of. I will correct my opinion. https://mathoverflow.net/questions/114943/where-are-the-seco... was very informative on this.

Still they have a couple more books of proof left, and I have to wonder how carefully it will be reviewed. This will still be a massive improvement, but I'd be a lot happier if the entire proof could be formalized.

Plus there is still a possibility that there proves to be another significant hole.

If any theorem needs to be formalized, this is the one. No other theorem is this big, this hard to prove, and this important to get right.

At the moment we seem to have exactly one guy equipped to do this, and he'll be busy with something else for the next few years: https://www.reddit.com/r/math/comments/176vtju/kevin_buzzard...