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.