Who checks that the formal proof matches the claim?

OpenAI’s math release has 722 manuscripts, and many come with Lean formalizations. The part I want to understand is how reviewers check that the formal theorem matches the claim in the paper.

A proof can check out under its stated assumptions, while novelty and what the result means still need a human explanation. Is there a good example in this batch where you can follow all three?