After they announced the formalization of the classification of Finite Simple Groups, I immediately wondered "What would happen if you tried to formalize the Stacks Project?" Despite also being very long, it's the opposite of the CFSG: instead of a poorly organized set of results that contribute to proving one big theorem, it's instead a carefully-organized set of results that cover a broad area.

The Stacks Project was the model for how mathematics should be done (at least for the pre-LLM era). Algebraic geometry had lots of poorly organized foundational results that were not really created for themselves, but in order to solve problems in the field. One person, Aise Johan de Jong, set out to fix it by organizing a project to write out the proofs of all of the results in a carefully organized fashion. He's led the project since, though of course there are multiple contributors. The whole thing is thousands of pages.

I would be interested in hearing more about the gaps they uncovered in the existing results, and how they fixed them.

I actually believe that this isn't the way to go when proof is cheap. Due to the straitjackets of type theory sharing proofs across domains is painful for most human readers to consume. With AI it's much easier to specialize theories. It's just not worth the cognitive cost to build on top of broad and shallow theories. To have any hope in keeping up with AI we need to instead better appeal to the largest component of our brain - namely our visual cortex.