If the lean proof doesn't match the natural language one (which is the one the AI generated to solve the problem), it sounds like the lean proof isn't verifying the intended claim?
From the paper:
"A third possibility is that the NL proof provides stronger statements than what the formal proof actually establishes,
with (of course) different proofs. The latter happens in OpenAI’s announced proof of blow-up of Navier Stokes equations."
From the paper: "A third possibility is that the NL proof provides stronger statements than what the formal proof actually establishes, with (of course) different proofs. The latter happens in OpenAI’s announced proof of blow-up of Navier Stokes equations."