> There have been efforts to reprove it with a more easily verified proof, but they've gone nowhere.

My understanding was that the so called "second generation proof" of the classification of finite simple groups led by Gorenstein, Lyons, Solomon has been progressing slowly but steadily, and only the quasithin case had a significant (but now fixed) hole. Are there other significant gaps that aren't as well known?

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.