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.