Classification of Finite Simple Groups Formalized in Lean (cfsg.axiommath.ai)

In this case the statement is unusually complicated but still much much easier to verify than the proof itself.

An error in the formalization would be a bug in lean. Which, as we know, certainly seems plausible (I've mused on if these giant proofs are incentivizing LLMs to find lean bugs to exploit), but at least it's a smaller surface area.

Humans have to establish trust in this.

After that, the rest of the language is written. Yes it is possible the type inference engine is broken but in that case the kernel will reject it

The article refers to its use of the "first-generation proof". It would seem this proof is too large to be truly known by one person, and the group of people who "collectively knew" it grew old and started to die. Since its original formulation, mathematicians began to compile, consolidate, and revise the proof into a 2nd generation digested form (estimated to be 5000 pages instead of tens of thousands). But that effort was still so monumental in its own right that a 3rd gen proof project began to digest the 2nd gen proof before the 2nd gen proof was even finished. I believe both the 2nd and 3rd gen projects are still ongoing.

It will be interesting to see how small the proof gets once we finish learning how to obtain these results "efficiently" with the benefit of hindsight.

Also don't discount the fact that people would learn how to do this kind of project, currently no one really knows how to decide what definitions work best, what should be reducible, what should be part of a public api and what should be local to a module, etc.