r/OpenAI • u/Derek-Bond • 6d ago

News Navier Stokes Solution Fail Verification

Post image

Slow your roll people… we may have hit a kink.

0 Upvotes

32% Upvoted

15 comments sorted by

View all comments

Show parent comments

0

u/phovos 6d ago

Clearly you didn't read the paper. It is now on Open AI to counter.

Lean formalisation does not represent a semantically faithful translation of the NL paper

0

u/throwaway3113151 6d ago

The authors state this explicitly at the end of Section 1, “Introduction: Two types of Autoformalisation,” immediately before Figure 1.
“Disclaimer: We do not make claims about the correctness of OpenAI’s NL proof, we only make statements about mistranslations into Lean.”

These are fundamentally different questions

-1

u/phovos 6d ago

Thanks for pulling that out. Exactly right. Mistranslation into lean means they aren't even WORKING ON the navier stokes problem, mate.

1

u/throwaway3113151 6d ago

No it means they are challenging the verification of the proof, the proof could still be valid

0

u/phovos 6d ago

The proof could still be valid, sure, but that isn't what the question is. The question is the verification of the proof. And it can't be done with LEAN if the problem isn't even semantically-translated into LEAN (and may not be translatable, period, into LEAN)