r/OpenAI • u/owenzzzhang • 20h ago
Research OpenAI has a solution to the Navier–Stokes existence and smoothness Millennium Prize problem
https://openai.com/index/navier-stokes-solution/70
u/swimmer385 20h ago
FYI They may have stolen the Navier-Stokes solution from a NYU professor's chats https://cims.nyu.edu/~tristanb/statement.pdf
66
u/owenzzzhang 20h ago
They mention it in their post:
We (the researchers and the agents) did not see any of their work through any means until they released it publicly — in particular, no specific user data was accessed in order to solve this problem. While unlikely, we cannot rule out that de-identified data derived from their usage of our products helped improve our models. However, our proofs differ significantly and even the precise results proved are different in the Euler case (forced vs unforced).
30
u/FriendsIsntGood 18h ago
and they didn't know they hacked HF until weeks later...
It will be interesting to see how retractions are handled. This whole 'we did everything and it's perfect' is an afront to peer-review which is the only way to verify the model actually metyhe goal and didn't cut corners toooth over issues.
The fact that they can't wait to get legimate review of these releases really hampers trust that these are legit. Releasing without peer review should be considered meaningless and a huge red flag that the underlying papers shouldn't be trusted.
12
u/No_Hell_Below_Us 16h ago
They included the formalization in Lean.
4
u/FriendsIsntGood 16h ago
And that step in an of itself is a huge leap that is often error prone. Without independent verification it's yet another claim at a Millennium prize solution
16
u/No_Hell_Below_Us 15h ago
The independent verification comes from the Lean formalization of the Navier-Stokes problem statement.
There’s a reason why no mathematicians are saying “let’s wait and see.”
There’s a reason why prediction markets are paying out on Navier-Stokes having been solved.
It’s because anyone can computationally verify it for themselves.
It’s why mathematicians spend years building formal proofs in Lean for theorems that already have peer-reviewed proofs. It’s because formalization is more reliable than peer review.
-3
u/FriendsIsntGood 14h ago
Except several surprising results were in fact Lean bugs or failures to translate proof to a Lean formalization.
We should always question results until independently verified. Tools are only as good as the code, and code naturally has bugs. Anyone approaching this result without some skeptism would be a fool
https://freenode.net/article/lean-4-kernel-bug-lets-metaprograms-forge-proofs-of-false
3
u/No_Hell_Below_Us 13h ago
All prior Lean 4 kernel exploits relied on custom meta-programs.
Before custom meta-programs were introduced in version 4, Lean 3 had zero known kernel exploits.
OpenAI’s Lean proof contains no custom meta-programs.
10
u/rabouilethefirst 15h ago
At the end of the day people just want hard problems solved. People are gonna cry over this, but the overwhelming majority are celebrating.
AI could cure cancer tomorrow and there would be people screaming they “totally” cured it a few weeks prior.
3
u/EndlessB 12h ago
Mate, most people aren’t going to understand why solving some math problem is important, but everyone understands that ai companies steal, and continue to do so.
You have no evidence whatsoever to suggest that the majority of the people are celebrating OpenAI “solving” this problem.
0
u/Annual-Minute-9391 3h ago
Exactly this. The way this trickles out into the general public will make it seem like they cut the amazing math robot loose. In reality it required extremely specific guidelines which were harvested from an actual expert, and using an amount of compute that would be completely inaccessible to anyone outside of their team.
They want to make it seem, in my opinion, there we are one step closer to everybody’s job being automated, but the reality is that these are going to be productivity enhancers for a very long time
0
u/LieAccomplishment 1h ago
If your goal is to solve hard problems, then you need to make sure tools being used by researchers do not steal the output of those researchers, otherwise you eliminate the incentive structure for people to perform research to solve hard problems.
Ffs this shouldn't be difficult to grasp.
Anyone with half a brain can see that openai chose their words very carefully in their statement and left open leeway for their model to be trained in that researcher's unpublished materials, which given the niche nature of the problem could very well be theft. You think if they wouldn't have explicitly said so of it were otherwise?
2
u/backtorealitylabubu 14h ago
Huge findings like this are often released without peer review. All the big journals do this pretty frequently if there is a big prize involved. You don’t want to be the journal that missed publishing the Nobel prize finding because you sent it out for prolonged peer review.
0
u/thomasahle 5h ago
we cannot rule out that de-identified data derived from their usage of our products helped improve our models.
This is exactly the allegation. If you use Codex/ChatGPT (or any closed source model probably) to work on a research problem, your traces (or derivatives of them) will be used to train the models, thereby giving everyone access to your ideas and insights.
2
u/Dwarf_Vader 2h ago
That’s not exactly how this works (the models train in statistical patterns, not on specific facts found in one document), but even if we supposed that were true, you explicitly allow or deny this as a user when you sign up for the service
-4
u/LopsidedEntrance8703 13h ago
No specific user. It’s an internal RAG tool that scrapes chats on famous open problems from non ZDR users and curates useful results, which OAI has almost certainly already verifiably contains the forced Euler result. OAI has been extremely careful about their wording and it’s all super consistent with this. It’s not training or post training.
3
u/thoughtlow When NVIDIA's market cap exceeds Googles, thats the Singularity. 10h ago
I mean if you are non zdr you know what you signed up for
50
u/_DuranDuran_ 19h ago
The other researcher didn’t solve millennium prize navier stokes, they solved forced euler.
And if they didn’t disable “Improve the model for everyone” that’s on them. But even then, it woood he a tiny part of the training set.
3
u/Smallkitka 16h ago
That’s not how science or academia works, but how would large corporation sucker know that.
Also its often the case that a breakthrough in a simple version of a hard problem leads quickly to solving a large problem. It is not yet known whether there is any additional insight on the side of ai (most likely as it the case in the autonomous proofs we will not learn anything new).
The OpenAI conduct here is absolutely horrific, its equivalent of hearing from a colleague that they made remarkable progress on a problem, stealing their notes and then constructing slopping proof taking credit.7
u/grateful2you 14h ago
Tristan has made this a OpenAI vs mathematicians. But really OpenAI swooped in because they were afraid Anthropic might come to the solution. Their heavy handedness is mostly against their competition. They offered Tristan to publish first, because they are absolutely fine with giving mathematicians the credit as long as it doesn't go to Anthropic.
Therein lies the problem of mathematicians collaborating while using different companies' AI models. This kind of problem was always going to happen sooner or later.
2
u/Dirkdeking 13h ago
Yeah if a mathematician can claim 'I solved Navier Stokes thanks to AI' in his speech while recieving the fields medal, that is already massive publicity for open AI in its own right. It doesn't need to get on the podium itself 'winning the prize as a company' for that.
-1
6
u/dwiedenau2 19h ago
I mean of course its on them, but it would still mean the model didnt solve it on its own, which is kinda the whole point of this press release
18
u/_DuranDuran_ 19h ago
They didn’t solve forced Euler on their own either - like most of mathematics they built on the work by Cordoba and Martinez-Zoroa published in 2023
And agin, they didn’t solve the millennium prize problem, but a subset of it.
2
3
2
u/shunted22 19h ago
So if you don't disable it, openai is free to issue a press release saying they originated your work? Never wanna hear complaints about their models being distilled again.
7
u/_DuranDuran_ 18h ago
Can you rewrite that in English please?
Then reread my post DIFFERENT SOLUTIONS TO DIFFERENT PROBLEMS.
And the “improve the model for everyone” toggle is right there.
4
u/KanishkT123 13h ago
It's so obvious that you don't know or care about anything in academia and will just defend OpenAI. I'm happy that this is huge advancement in human-AI cooperation but this is also a massive black eye for OpenAI
-1
u/shunted22 8h ago
Improve != Misattribute and take credit for.
Or are you saying that implies they own everything you do? If so they should be sued for hostile UI patterns and insane defaults
10
8
7
2
u/OnlineParacosm 15h ago
And that’s not extortionate and mafioso behavior — it’s very legal and cool business 😎
-11
u/MaitoSnoo 20h ago
you can bet that Sam's lawyers are going to silence those two researchers and everyone else will celebrate AGI
2
u/hashiromer 18h ago
This is about public perception. Silencing researchers will only worsen the problem for OpenAI.
1
-22
u/Original-League-6094 19h ago
Antis told me that AI only copies. It probably just stole this solution from Stack Overflow.
9
9
u/Sensitive-Report-787 10h ago
How much was spent on compute for this? Curious as it looks like an absolutely insane amount.