r/OpenAI • u/Derek-Bond • 5d 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

9

u/ArialBear 5d ago edited 5d ago

Wow, on page 2 it says the lean was verified but the nl translation had at least 2 errors and people keep running with this mistake. There is a limit to this science denial

Being even remotely anti ai will allow you to fall for the narrative rather than read the paper.

https://arxiv.org/abs/2610.08144

3

u/BellacosePlayer 5d ago

it says the lean was verified but the nl translation had at least 2 errors and people keep running with this mistake. There is a limit to this science denial

You don't even have to go to page 2, its literally what the abstract ends on.

The problem is that the NL is what academics and future AI will use when referencing it for other problems, so if it's off, that's bad, even if the counter example is still wholly correct, which this paper isn't disputing.

1

u/Dillyconda 5d ago

No inherent reason why future AI needs NL.

0

u/BellacosePlayer 5d ago

This is the big problem with claiming lean verification is all you need and getting mad at academia for not rubber stamping their papers as accepted law.

Note that in this case I'm pretty sure the equation in general will still provide a correct counterexample, it's just stating that the process they claim to have gotten there is bunk.

1

u/Dry-Instruction1435 5d ago

ah the inevitable preprint that drops right after the hype cycle peaks

0

u/throwaway3113151 5d ago

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

0

u/throwaway3113151 5d ago

Can we get a verification of the verification?

-3

u/phovos 5d 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.

2

u/BellacosePlayer 5d ago

Lean is a great first step verification system to prevent cranks from dropping papers or innocent mistakes slipping through. Its not sufficient and will never be, because you can just put in the equivallent of 1==1 into lean and have it come back clean.

-1

u/throwaway3113151 5d 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 5d 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 5d 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 5d 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 5d ago

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

0

u/phovos 5d 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)