Well, the point of the _computer_ formalization is that it's checkable.

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.

In general checking that the definitions are correct isn't that hard and assuming at least one of the lean kernels you verify with is correct (which tbf is an assumption, the implementations are based on each other so could have a common bug) that's all you need to verify.

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

So, the specification of the theorem we are fairly solid on, formalising what a group is, and a simple group, have been done a long time and we are confident in the correctness of.

Assuming you do trust those, then assuming the formalisation passes lean (and lean has no bugs!), then the whole idea is you've got a proof of the theorem.

The papers describing lean and it's core operations are deliberately small. The kernel of a theorem prover is meant to be such that a human can check it for correctness. The kernel does not include things like type inference or execution. It literally checks the proof and that's all and everything needs to match exactly. It's fairly trivial to write such a thing.

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