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."

The lean proof being correct is easy to verify, whether it proves the thing we care about is much harder.

If your code compiles, are you sure it's bug free?

It doesn't look like they've found an error in the NL proof either, just that they are different?

Indeed. The natural language proof is incorrect but the Lean proof is correct.

Humans have made similar mistakes too. A human writes a specification for how things should work, the human translates that into code, the code does not work, and finally the human fixes the code and forgets to fix the original spec.

Yes — because there are many non-equivalent statements that are easier to prove.

So the Lean proves something and the question is whether that something is actually what we care about — or something similar, but ultimately not the question.

Yes, exactly. There's no real pressure on AI to get the natural language version of the proof correct, and no way to really judge it automatically.

Yes however, whether a natural language proof and a formal proof "correspond" is subjective.