Incorrect. The statement in Lean can itself be wrong. Moreover, they could be exploiting a kernel bug in Lean, of which we had one published literally a week ago.

Besides for what others have mentioned, the lean proof could be proving something else. Given AI’s propensity to hallucinate, seems like someone should check the lean proof actually expresses what it’s claimed to.

We recently saw that lean itself isnt proven correct. Its not likely but i wouldnt call it verified if its only verified in lean

https://x.com/gro_tsen/status/2082483878480977959

Or they made another LLM 'read' them?

> You are an expert in the field of mathematics, with decades of experience. You are a reviewer of proofs, etc etc.etc.