alt Hacker News> 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.