Looks like those are new formalizations of existing proofs, not new ones
So a fair headline would be "OpenAI tried formalizing more of their proofs, and found 33% of them had a mistake".
alt Hacker News
So a fair headline would be "OpenAI tried formalizing more of their proofs, and found 33% of them had a mistake".