> However, checking that a given Lean repository actually proves the claimed statement is somewhat non-trivial, especially for an audience which is not expert in the use of Lean

Isn’t this kind of a recursive problem where you now have to prove your proof that their proof proves their claimed statement?

It's not a proof. You check that the mathematical ideas expressed in the claimed statement are the same as the mathematical ideas expressed by the Lean repository.