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.

Do they say how they verified the formalizations of the theorem hypotheses? (Sorry, I haven't read it yet.)

Okay this is actually useful AI formalization. But the stacks project is basically Lean in natural language anyways, so it makes sense why its high quality.

Slightly off-topic, but how far are we from a formally verified stack for (say) a webdav or NFS server?

The fact that the description is AI slop doesn't inspire confidence in the results.