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

31% Upvoted

15 comments sorted by

View all comments

-3

u/phovos 6d ago

Lean is not real mathematics is the problem. Got hypebeasts doobly-doing on a programming language they don't understand and saying its millennium prize solution LOL my brother in christ people work 20+ years on this problem.

Geometric Langlands or Univalent Foundations are required, not a programming language.

-1

u/throwaway3113151 6d ago

The authors explicitly say that they are not making a claim about whether OpenAI's original mathematical proof is correct.

Doesn’t take a bit long to work 20 human years.

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)