If the problem statements in lean are correctly formalized, I think we can be pretty confident the proofs are correct, which does not mean their natural language counterparts are faithful representation of the proofs though.

I'm however puzzled by the number of proof claims without lean proofs. How does OpenAI have confidence in those, especially if, as noted in the blog posts, the papers are very hard to read?