Regardless of what you think of the priority dispute issue discussed on sibling threads, I’m highly skeptical of the closing quote that this Navier Stokes result means that the same approach of casually spending a few million on agentic computation is going to solve end to end materials design or drug development.
Those problems can’t be formally verified with an automated theorem prover. We have a lot of physics based simulation tools, but they tend to focus on small subsets of the full design problem and they make limiting approximations because otherwise they’d be too computationally expensive, or we just don’t have the right data to parameterize them beyond describing qualitative behavior. Agents are helping accelerate research in these fields but I think it’s mostly a different class of problem that’s a lot harder to specify and verify
Yeah, I think you can't just throw money randomly at problems and expect results unless you know a line of attack that can get you all the way. OpenAI chose the line of attack only after it became known to them via rumors. They "front-ran" the researchers.
>We have a lot of physics based simulation tools, but they tend to focus on small subsets of the full design problem and they make limiting approximations
Do you think it is possible that better math will lead to better physics models?
I’m pretty sure that OpenAI has some of the best mathematicians prompting the models and analysing the results. While they are marketing as if the model solves problems themselves.
> However, communications quickly became contentious. According to Buckmaster, OpenAI offered to give him sole authorship on the Navier-Stokes solution—but only if Alpöge’s name was removed from the work and if the write-up would acknowledge the problem had been resolved by an internal OpenAI model. Buckmaster refused, in part because he was troubled by the question of what OpenAI's system had actually seen. For example, Buckmaster said the company did not initially give him a clear answer about whether its agents had access to the pair's logs on Codex (which is an OpenAI product).
> OpenAI executives have denied that any employee or AI agent saw the pair’s work before the researchers released it publicly on 7 September. But there still remains a separate question: Could the pair's work have reached OpenAI's models through its training data?
> OpenAI’s blog announcing the Navier-Stokes solution does not dismiss the possibility: “While unlikely, we cannot rule out that de-identified data derived from [Buckmaster and Alpöge’s] usage of our products helped improve our models .”
So, this company wants everyone and every organization on Earth to use their software, and reserve the right to then tell anyone how the resulting work can be published and credited?
Real solid business model there, how could it ever fail?
That's not what the comment you're replying to or the article says. I feel like I'm going crazy reading comments here and elsewhere, am I not reading the same articles as everyone else?
There's a lot of unverified hearsay but the crux of the problem is that there is controversy around using this company's tools, the attribution of the resulting work, and the company for some reason competing with its users. The whole thing reeks and my point is: people won't ask for the chromatography spectrum of the turd, they will walk away.
Paying for an account doesn't opt you out by itself, right? Has he stated anywhere that he actually opted out? But if not, then I also don't understand why OpenAI's communications about this have been so vague, they could've just said that he didn't opt out, using those chats in training data follows their ToS and that's it (whether that's "fair" is a separate discussion).
There has been no statement either way, as far as I could find beyond them only using commercially available models, though given Alpöges employer, I'd be surprised if they didn't opt out. In any case, for such work, ZDR or self-hosting seem to be an absolute must now.
Unless OpenAI can show that training was permitted, this will erode the limited trust that many users have had in such toggles and may lead to further, uncomfortable inquiries.
IIUC, the accusation was not to try to remove Alpöge from the paper he wrote with Buckmaster solving the "easier" conjeture, but to exclude Alpöge in the followup paper where Buckmaster review the OpenAI solution of the "full" conjeture.
For comparison, if you offer me to collaborate in a paper about Algebra I may agree to go alone, but if the paper is about Quantum Chemistry I have to piggyback a few coworkers because we are collaborating in that topic for a long time and I already discussed may of the topics and I may even discuss the new paper too.
Because he works for Anthropic. Supposedly this project was not part of his official capacity as an employee of theirs.
However, if they had published first, it's hard to imagine Anthropic not taking the opportunity to claim "our employee solved this Millennium prize problem using our AI".
I think it was a pretty questionable thing to do by trying to front-run these researchers even if they didn’t make use of their techniques. The fact that they may have inadvertently “borrowed” their work via training data makes it much worse.
OpenAI’s behavior here — even if you only consider [their] side of the story — was (at best) in bad taste.
Strongly agree. And as one of the major AI companies, this is extremely tone deaf. If they saw a human (even if assisted) was making great progress on a major problem then you give them space. You don’t swoop in with millions in token spend to scoop them. There are tons of important problems where humans aren’t making traction - please go solve those.
> “I certainly don't expect the industry to continue to spend millions of dollars to solve problems in mathematics, because there is no profit in it,” Columbia University mathematician Michael Harris wrote in an email to Science. But he worries the highly publicized achievement will be “extremely damaging to mathematics; it convinces decision makers that human mathematicians are obsolete, and it convinces young people that their passion for mathematics has no future.”
LLMs seem particularly suited toward these existence-proof problems. Working mathematicians seem absolutely essential for universally quantified results, still. I strongly doubt, for example, that if Fermat's Last Theorem hadn't been proven three decades ago, that an LLM would be able to do work equivalent to inventing the mathematics as Andrew Wiles did to solve the problem. I have similar doubts about P vs NP, the twin prime conjecture, even the Riemann Hypothesis (unless the latter has at least one counterexample).
And I want to be clear: I'm not downplaying the achievements of these models. This is remarkable! I simply think that the pattern of success is in existence proofs or finding counterexamples, which makes sense based on how LLMs function and are trained.
It would be good if someone made a list of allresults obtained with AI so far just to see what kinds of problems AI excels at. Are there any that aren't of the existence-proof type?
Reductively, math can be said to be either problem solving or theory building - it seems the latter is a much harder thing to do right now.
Regardless of the end result, OpenAI's behavior would be a career-ending ethics scandal for a human mathematician. This bit alone would be a career-ender.
> According to Buckmaster, OpenAI offered to give him sole authorship on the Navier-Stokes solution—but only if Alpöge’s name was removed from the work and if the write-up would acknowledge the problem had been resolved by an internal OpenAI model.
I wonder if an appropriate response from the mathematical community would be a good old-fashioned shunning. Mathematicians are allowed to use OpenAI's tools as much as they want, but no one with any current or prior OpenAI affiliation gets published in a reputable journal, ever.
And according to that team OpenAI only started asking their own model these questions after those submissions had occurred. So OpenAI had these critical clues and info before they started. If OpenAI did or did not use that to produce their own “proof” is an open question, but OpenAI hasn’t definitely denied it.
>For the past year, Buckmaster and Alpöge had been using a variety of AI tools, including OpenAI’s Codex, to tackle the Navier-Stokes problem. Last month, their AIs had at long last found a solution to the Euler equations and verified it in Lean.
I have started to feel the sense lately, that first with the HF breach and now this plagiarism scandal, it is the straw that has broken the camel's back (so to speak). We have turned the corner and clearly entered the endgame - everything is going to unravel astonishingly quickly.
Other than the undeniable breakthrough in math, the important point is the ability to orchestrate 10k agents to productively work on a single problem, which creates options:
> OpenAI, meanwhile, says its experience with Navier-Stokes could open the door to solving puzzles with more practical relevance. “We are now able to spend millions of dollars on a problem that we really care about and that really matters: developing new materials, finding cures to diseases,” Bubeck said. “All of those things that we have been talking about for a long time—now they seem to be at our fingertips.”
Your local trailer park was never going to be able to afford sponsoring high energy particle physics experiments projects that hollow out a mountain and use up a ton of xenon to try to detect a stray particle. High end science has required deep pockets for a long time.
But given the cost of a college textbook this is a pretty silly complaint to lobby against a subscription that's $200 a month, in the context of the cost of a variety of other materials and tools out there. (If you think that's expensive you've clearly been lucky enough to never have to deal with commercial software costs) Also not sure how quickly this stuff uses up limits; $100 or even $20 subs might be enough for students. And if a student is scrappy and figures out that Luna can meet their needs then I'd imagine Luna is effectively unlimited on some of these subs. Luna Max scores pretty high.
OpenAI has messed up big time here by competing with their customers. It would have become the norm for humans and mathematicians to use the tools and publish bigger results any way. If OpenAI didn’t run for credit, this theorem itself may have been proven by Buckmaster OR others in maybe a year or two.
But now the bigger issue than AI solving problems is the issue of chat privacy, at the end of the day.
"Breakthrough" to me would be like Isaac Newton inventing calculus to calculate pi. This feels more like $12MM in tokens was spent to add another digit to pi using the old way.
Personally this is a watershed moment for researchers and grad students I know. All of them are close sourcing WIP repos, not putting their progress in LLMs, or have lab level initiatives to self host models.
I am building a federated hosting platform that I plan to opensource for this exact reason for our company and similar users. I would love to talk to these teams (we are a small team at Duke and a health care company).
I'm a mathematician. I have a lot of trepidation about these tools and what they mean for the future of the profession.
That said... most of us are not working on problems as famous as Navier-Stokes. Even if OpenAI could scoop me based on my back-and-forth with ChatGPT, which I presume they could if they threw $15 million worth of compute at it, I highly doubt they'd bother.
I think they spent millions pursuing strategies to attack that particular problem? I don't think it takes 15 million for their model to get trained on your chat logs. This is probably all automated internally. If they did scoop your ideas, it would likely get incorporated into their model without any conscious decision making. And if you're not a high profile academic, nobody will hear about it.
The fact that anyone has to make that trade off with that through process shows a company and culture that is untrustworthy. OpenAI isnt open, isnt a non-profit, isnt for the benefit of humanity, and isnt even for the benefit of users at this point, its users are vassals providing training data so their models can reach ASI first.
I am going all in on sovereign ai even if its worse, these companies have shown they not only dont deserve trust but are actively stealing past and present intellectual property from humanity and users.
But consider they could decide that they want to scoop more regular research work too. They could automate it with just a few LoC. Even if you opted out in the ToS, you'd have to file a massive lawsuit just to enforce it. And the actual fine would be inconsequential to OpenAI.
I think going forward, any researcher should consider anything submitted to an LLM to be copied/stolen.
If you mean move to products with ZDR policies, OK, very fair and I agree. If you're talking the equivalent of carpenters should give up pneumatic air guns because hammers are more authentic, then that's silly. These are tools, and like any tool how effective they are can come down to how well you use them.
Should they give up pneumatic air guns if the company that supplies then can then control what you build with them, how you build with them, and secretly copies all your designs for their own use. Sure its a good tool, but its also becoming a trap.
Are you asking if it uses additional axioms of `sorry` in the proof? It's easy to check that it doesn't by compiling it and telling lean to list the axioms.
Is it? Clicking around the code it looks like a pretty mechanical translation of the statement on the millennium problem website. Assuming of course that you are willing to trust that e.g. the real numbers definition and API included in MathLib4 is correct, but that feels very safe to me.
I'm not claiming to be an expert on Lean4 (although I have contributed tactics) but this is one of the most direct formalisations I've seen of a serious result (second only to FLT of course, which has a horrible proof but it is trivial to verify the statement)
This right here, or at least the thought of this, is why in the not so far future, businesses can't (won't?) be using these LLMs services.
You cannot risk companies like Anthropic, OpenAI or their business partners like Microsoft having unfettered access to proprietary data on your company/businesses.
It it likely that they or rogue employees will use the information to make a profit? It's pure speculation, but I'd say more than likely, and we will never hear about it or read it on the news unless there's whistleblowers in high enough positions to know about it.
Assuming you and your employees aren't careful with what data you share, they will have intimate knowledge about your company from files and conversations logs. Likely personal user data too which they'll gladly create databases to link to and create extensive profiles on you, your employees and your businesses.
It's not far-fetched to see them leveraging insider information shared with LLMs to play the stock market, leveraging data against competing businesses in other markets they might want to explore, and likely a bunch of other things that are escaping me right now as I write this.
At the end of the day it's on those people for sharing such sensitive data, but it's not like these AI companies are innocent and won't gladly exploit every little byte of data without telling you, we know it happens.
Its not "in the future", its already here, right now. Sensitive IP gets processed on rented or local GPUs running open weight models. Sometimes its required due to data privacy laws, sometimes its because the people running those shops are not trusting OpenAI/Anthropic ZDR policies being observed. Normal, boring, US and EU-domiciled enterprises do this on a regular basis, and there is an industry of companies helping said boring companies set things up.
It is even worse. Just them knowing or having an inkling that someone is close to achieving a solution might be enough for them to spawn a team of thousands of agents and outrun you.
> OpenAI, meanwhile, says its experience with Navier-Stokes could open the door to solving puzzles with more practical relevance. “We are now able to spend millions of dollars on a problem that we really care about and that really matters: developing new materials, finding cures to diseases,” Bubeck said. “All of those things that we have been talking about for a long time—now they seem to be at our fingertips.”
Eh? There's no connection at all between the Navier-Stokes work and those things.
He may be hinting that solving these complex mathematical problems will boost OpenAI clients' confidence and encourage them to spend millions of dollars on solving other complex problems.
I would think it would have the exact opposite effect.
Why would anyone use OpenAI models for anything commercially valuable, or where secrecy is important, when it appears that if OpenAI "becomes aware" that you are doing so they may try to compete with you?
Not only did OpenAI, by their own admission, rush to re-solve Navier-Stokes once they heard the rumor a week ago that it has been solved (the rumor being that it was Anthropic that had done it), but they are leaving the door open ("we cannot rule out that") as to whether the model they used to do it had been trained on the anonymized date from the researchers who's approach they ended up copying.
Terrance Tao has recently said as much for mathematics - that there appears to be a trend (not just this Navier-Stokes incident) of the AI companies going after math problems wherever there is an "rumor" of progress, and that he thinks this may sadly result in breakthrough mathematics being conducted in secret to avoid this.
The rush to steal another researcher's thunder is bad enough, but it also appears that one of OpenAI's employees acted in a very thuggish manner to try to threaten the professor who had been working on this not to publish and to co-operate with their telling of the story.
They represent different AI usage patterns. OpenAI wants everyone to believe that it was done with a practically autonomous network of thousands of agents with little to no human intervention for 88 hours, while Buckmaster/Alpöge were using AI in a more guided way for months. If OpenAI actually used anything from Buckmaster/Alpöge work they would be misleading the public.
Agree! Not sure I believe that Buckmaster/Alpöge were guiding the AI.
This is just their way of saying that they had something in the process and deserve merit.
Asking the question in the right way may be 99% of the work. And the fact that openAI is effectively snooping on users and then outspending them to announce a break through is just gross.
Is it really?
If I ask my swarm of agents to read about every relevant stuff about NS problem online might me more than what any researcher can prompt the machine these days.
I do. But the difference is: do I go around bragging that my agent worked for 88h to solve a problem? Where is the credit coming from? Is it coming from the: I was the first one to think about throwing a prompt: "Solve Riemann Hypothesis" and it turns out that by luck of the non-deterministic behavior of the agent, it got right? Wow, that is a lot of merit really. Congrats...
Sorry the sarcasm, but really your point makes absolutely no sense.
It is completely different to design something with AI and then execute, validate, evolve vs just prompt it machine-g-brrrr style and get a result.
This brings an important question. Nowadays I don't write code, I review code, I review systems behavior and get paid for it. Will that be the same for math researchers? Their prompt/problem is already well-posed out there. Ours, in the day-to-day, are not. Will the first one to verify AI work get the credit? or is it going to be the dumdum that types a simple prompt and has the compute to run it for 21321 hours? I absolutely don't get your point here. Or you are just rage baiting
If you take OpenAI at face value, they claim they threw a relatively simple prompt at the problem on a whim and boom presto, a swarm of "agents", 15 million dollars and 90 hours later they disproved the hypothesis. Wow, look at how powerful our AI is, you don't even need to be a world-class mathematician, you just tell it to solve a problem and it does!
By contrast, what the world-class 2 mathematicians did was sat down and started working on their proof for over a year, using AI along the way to help with their research. A much more grounded and realistic use of these tools, but one that doesn't generate nearly as much hype as the alternative.
The cracks in OAI's story has been immediately disproven, and they seemingly plagiarized the work of the 2 and then threw the team of researchers and the 15 million dollars at the problem after the fact. It doesn't exactly bode well for their hype machine when you consider the chain of events here, which is why people care about this, as OAI's constant and incessant lies they spew every minute of every day is finally hopefully catching up to them, and right before their big IPO too.
Editing to add: And I think it's all such a shame. We live in a time with genuinely insanely cool technology that is doing some truly incredible, ground-breaking stuff, but it's all tainted by a gaggle of greedy sociopaths and reprobates whose only goal in life is to have the largest number in their bank accounts. LLMs could've been such an amazingly neutral and cool and useful tool had more level-headed people been at the wheel, but instead we're stuck with this childish bullshit and giving the likes of Sam Altman real power to enact societal collapse.
Ergo, they can't prove any theorem whatsoever. How do people at OpenAI expect that we believe in claims like that? This is yet another before-the-IPO stunt in my opinion..
Personally, I won't believe any of these claims until the community of mathematicians says otherwise.
Regardless of what you think of the priority dispute issue discussed on sibling threads, I’m highly skeptical of the closing quote that this Navier Stokes result means that the same approach of casually spending a few million on agentic computation is going to solve end to end materials design or drug development.
Those problems can’t be formally verified with an automated theorem prover. We have a lot of physics based simulation tools, but they tend to focus on small subsets of the full design problem and they make limiting approximations because otherwise they’d be too computationally expensive, or we just don’t have the right data to parameterize them beyond describing qualitative behavior. Agents are helping accelerate research in these fields but I think it’s mostly a different class of problem that’s a lot harder to specify and verify
Yeah, I think you can't just throw money randomly at problems and expect results unless you know a line of attack that can get you all the way. OpenAI chose the line of attack only after it became known to them via rumors. They "front-ran" the researchers.
Working with AI on science (not LLMs though), couldn't agree more.
For any practical application, numerical solvers for Navier-Stokes already exist and do a good job.
This proof is just checking the boxes for mathematicians.
>We have a lot of physics based simulation tools, but they tend to focus on small subsets of the full design problem and they make limiting approximations
Do you think it is possible that better math will lead to better physics models?
It might but the math results from GenAI so far have been limited to finding counterexamples to known conjectures, not building new mathematics.
I’m pretty sure that OpenAI has some of the best mathematicians prompting the models and analysing the results. While they are marketing as if the model solves problems themselves.
The core section:
> However, communications quickly became contentious. According to Buckmaster, OpenAI offered to give him sole authorship on the Navier-Stokes solution—but only if Alpöge’s name was removed from the work and if the write-up would acknowledge the problem had been resolved by an internal OpenAI model. Buckmaster refused, in part because he was troubled by the question of what OpenAI's system had actually seen. For example, Buckmaster said the company did not initially give him a clear answer about whether its agents had access to the pair's logs on Codex (which is an OpenAI product).
> OpenAI executives have denied that any employee or AI agent saw the pair’s work before the researchers released it publicly on 7 September. But there still remains a separate question: Could the pair's work have reached OpenAI's models through its training data?
> OpenAI’s blog announcing the Navier-Stokes solution does not dismiss the possibility: “While unlikely, we cannot rule out that de-identified data derived from [Buckmaster and Alpöge’s] usage of our products helped improve our models .”
So, this company wants everyone and every organization on Earth to use their software, and reserve the right to then tell anyone how the resulting work can be published and credited?
Real solid business model there, how could it ever fail?
The site should have a disclaimer at the bottom: "A Sam Altman Production."
99% of the world (maybe more) have 0 idea of who Sam Altman is.
Add "We might take credit for things you figure out, if we can infer it from your prompts" and it might actually affect people's usage of these tools.
That's not what the comment you're replying to or the article says. I feel like I'm going crazy reading comments here and elsewhere, am I not reading the same articles as everyone else?
There's a lot of unverified hearsay but the crux of the problem is that there is controversy around using this company's tools, the attribution of the resulting work, and the company for some reason competing with its users. The whole thing reeks and my point is: people won't ask for the chromatography spectrum of the turd, they will walk away.
You are. Most people have just long decided to forgo nuance for the simplicity of snark and hate as a default response
> While unlikely, we cannot rule out that de-identified data derived from [Buckmaster and Alpöge’s] usage of our products helped improve our models.
Well yeah, if you use the free product they train on your data, ... I thought this was widely understood?
If you read Buckmasters statement, he specifically notes that they used the paid subscriptions, iirc.
Paying for an account doesn't opt you out by itself, right? Has he stated anywhere that he actually opted out? But if not, then I also don't understand why OpenAI's communications about this have been so vague, they could've just said that he didn't opt out, using those chats in training data follows their ToS and that's it (whether that's "fair" is a separate discussion).
There has been no statement either way, as far as I could find beyond them only using commercially available models, though given Alpöges employer, I'd be surprised if they didn't opt out. In any case, for such work, ZDR or self-hosting seem to be an absolute must now.
Unless OpenAI can show that training was permitted, this will erode the limited trust that many users have had in such toggles and may lead to further, uncomfortable inquiries.
The paid subscriptions have opt-out for sharing data for training purposes. I think it's on by default.
They did pay [0] and substantially by the sound of things:
> I pay for the tools my group uses out of my own research funds, including footing a large bill to OpenAI.
[0] https://cims.nyu.edu/~tristanb/statement.pdf
> but only if Alpöge’s name was removed
This is blatant scientific misconduct.
IIUC, the accusation was not to try to remove Alpöge from the paper he wrote with Buckmaster solving the "easier" conjeture, but to exclude Alpöge in the followup paper where Buckmaster review the OpenAI solution of the "full" conjeture.
For comparison, if you offer me to collaborate in a paper about Algebra I may agree to go alone, but if the paper is about Quantum Chemistry I have to piggyback a few coworkers because we are collaborating in that topic for a long time and I already discussed may of the topics and I may even discuss the new paper too.
Any idea why OpenAI cared about this name removed from the paper?
Because he works for Anthropic. Supposedly this project was not part of his official capacity as an employee of theirs.
However, if they had published first, it's hard to imagine Anthropic not taking the opportunity to claim "our employee solved this Millennium prize problem using our AI".
Ah, I missed that part, thanks!
He works for Anthropic nowadays.
I think it was a pretty questionable thing to do by trying to front-run these researchers even if they didn’t make use of their techniques. The fact that they may have inadvertently “borrowed” their work via training data makes it much worse.
OpenAI’s behavior here — even if you only consider [their] side of the story — was (at best) in bad taste.
Borrowing the work of others to replace them without crediting is the model of current AI companies.
They just used that occurrence as a PR stunt but it isn't worse than the others done at scale every second.
This is the take I agree.
It is mean spirited but nevertheless sold their model
Strongly agree. And as one of the major AI companies, this is extremely tone deaf. If they saw a human (even if assisted) was making great progress on a major problem then you give them space. You don’t swoop in with millions in token spend to scoop them. There are tons of important problems where humans aren’t making traction - please go solve those.
Yea, strongly agree. I think this is going to back-fire spectacularly. They better start preparing an apology...
Extensive discussion on OpenAI's blog post on Navier-Stokes: https://news.ycombinator.com/item?id=49613262 .
Quanta Magazine article that also discusses some of the controversy: https://www.quantamagazine.org/ai-has-solved-one-of-maths-1-...
> “I certainly don't expect the industry to continue to spend millions of dollars to solve problems in mathematics, because there is no profit in it,” Columbia University mathematician Michael Harris wrote in an email to Science. But he worries the highly publicized achievement will be “extremely damaging to mathematics; it convinces decision makers that human mathematicians are obsolete, and it convinces young people that their passion for mathematics has no future.”
LLMs seem particularly suited toward these existence-proof problems. Working mathematicians seem absolutely essential for universally quantified results, still. I strongly doubt, for example, that if Fermat's Last Theorem hadn't been proven three decades ago, that an LLM would be able to do work equivalent to inventing the mathematics as Andrew Wiles did to solve the problem. I have similar doubts about P vs NP, the twin prime conjecture, even the Riemann Hypothesis (unless the latter has at least one counterexample).
And I want to be clear: I'm not downplaying the achievements of these models. This is remarkable! I simply think that the pattern of success is in existence proofs or finding counterexamples, which makes sense based on how LLMs function and are trained.
It would be good if someone made a list of allresults obtained with AI so far just to see what kinds of problems AI excels at. Are there any that aren't of the existence-proof type?
Reductively, math can be said to be either problem solving or theory building - it seems the latter is a much harder thing to do right now.
> Navier-Stokes is one of six “Millennium Problems” on a list compiled by the Clay Mathematics Institute in 2000.
Seven, not six. One is solved already, but is still a millennium problem.
I see the six seven reference there mate
Yes, that's a strange mistake to make.
One of the other millennium problems is counting to 7.
Regardless of the end result, OpenAI's behavior would be a career-ending ethics scandal for a human mathematician. This bit alone would be a career-ender.
> According to Buckmaster, OpenAI offered to give him sole authorship on the Navier-Stokes solution—but only if Alpöge’s name was removed from the work and if the write-up would acknowledge the problem had been resolved by an internal OpenAI model.
I wonder if an appropriate response from the mathematical community would be a good old-fashioned shunning. Mathematicians are allowed to use OpenAI's tools as much as they want, but no one with any current or prior OpenAI affiliation gets published in a reputable journal, ever.
OpenAI apparently used Buckmaster and Alpöge‘s work w/ Codex to bootstrap “their” dis-proof. https://cims.nyu.edu/~tristanb/statement.pdf
And according to that team OpenAI only started asking their own model these questions after those submissions had occurred. So OpenAI had these critical clues and info before they started. If OpenAI did or did not use that to produce their own “proof” is an open question, but OpenAI hasn’t definitely denied it.
>For the past year, Buckmaster and Alpöge had been using a variety of AI tools, including OpenAI’s Codex, to tackle the Navier-Stokes problem. Last month, their AIs had at long last found a solution to the Euler equations and verified it in Lean.
Their AIs?
I have started to feel the sense lately, that first with the HF breach and now this plagiarism scandal, it is the straw that has broken the camel's back (so to speak). We have turned the corner and clearly entered the endgame - everything is going to unravel astonishingly quickly.
Other than the undeniable breakthrough in math, the important point is the ability to orchestrate 10k agents to productively work on a single problem, which creates options:
> OpenAI, meanwhile, says its experience with Navier-Stokes could open the door to solving puzzles with more practical relevance. “We are now able to spend millions of dollars on a problem that we really care about and that really matters: developing new materials, finding cures to diseases,” Bubeck said. “All of those things that we have been talking about for a long time—now they seem to be at our fingertips.”
My impression: the re-aristocratization of scientific research seems inevitable.
Your local trailer park was never going to be able to afford sponsoring high energy particle physics experiments projects that hollow out a mountain and use up a ton of xenon to try to detect a stray particle. High end science has required deep pockets for a long time.
But given the cost of a college textbook this is a pretty silly complaint to lobby against a subscription that's $200 a month, in the context of the cost of a variety of other materials and tools out there. (If you think that's expensive you've clearly been lucky enough to never have to deal with commercial software costs) Also not sure how quickly this stuff uses up limits; $100 or even $20 subs might be enough for students. And if a student is scrappy and figures out that Luna can meet their needs then I'd imagine Luna is effectively unlimited on some of these subs. Luna Max scores pretty high.
> Your local trailer park was never going to be able to afford sponsoring high energy
taxes.
What do you mean?
In any case mathematics is humanity's oldest open source project going on for millenia, it never belonged to a single country, institution or class.
Only the idle and curious rich
Ramanujan was dirt poor.
Ramanujan was a phenomenon
OpenAI has messed up big time here by competing with their customers. It would have become the norm for humans and mathematicians to use the tools and publish bigger results any way. If OpenAI didn’t run for credit, this theorem itself may have been proven by Buckmaster OR others in maybe a year or two. But now the bigger issue than AI solving problems is the issue of chat privacy, at the end of the day.
"Breakthrough" to me would be like Isaac Newton inventing calculus to calculate pi. This feels more like $12MM in tokens was spent to add another digit to pi using the old way.
Inventing calculus to calculate pi? I don't think that ever happened...
Trust me bro that's how things went down
I'm not sure if you meant it this way, but this is more an insult directed at mathematics, not openAI.
That would be an incorrect interpretation
Yeah solving a Millennium Problem is totally equivalent to calculating another digit of pi.
Its called an analogy
It's one of the seven most important problems in mathematics.
Pick a better analogy.
If anything I'm diminishing the importance of calculus and pi by comparing it to this bullshit
GP is saying it’s not a very good one.
Who should get credit? All the humans who ever worked to create the data.
And the AI company for making the search program that searched through the data and found the solution.
Who should get credit? Sam Altman, and we should give him a couple hundred billion more as well.
Snark aside, the researchers working on this, who built the foundation, should get credit, and they are.
Moving forward, I can't imagine other mathematicians wanting to have this kind of experience. So there has to be a shift away from these services.
Personally this is a watershed moment for researchers and grad students I know. All of them are close sourcing WIP repos, not putting their progress in LLMs, or have lab level initiatives to self host models.
I am building a federated hosting platform that I plan to opensource for this exact reason for our company and similar users. I would love to talk to these teams (we are a small team at Duke and a health care company).
I'm a mathematician. I have a lot of trepidation about these tools and what they mean for the future of the profession.
That said... most of us are not working on problems as famous as Navier-Stokes. Even if OpenAI could scoop me based on my back-and-forth with ChatGPT, which I presume they could if they threw $15 million worth of compute at it, I highly doubt they'd bother.
I think they spent millions pursuing strategies to attack that particular problem? I don't think it takes 15 million for their model to get trained on your chat logs. This is probably all automated internally. If they did scoop your ideas, it would likely get incorporated into their model without any conscious decision making. And if you're not a high profile academic, nobody will hear about it.
The fact that anyone has to make that trade off with that through process shows a company and culture that is untrustworthy. OpenAI isnt open, isnt a non-profit, isnt for the benefit of humanity, and isnt even for the benefit of users at this point, its users are vassals providing training data so their models can reach ASI first.
I am going all in on sovereign ai even if its worse, these companies have shown they not only dont deserve trust but are actively stealing past and present intellectual property from humanity and users.
But consider they could decide that they want to scoop more regular research work too. They could automate it with just a few LoC. Even if you opted out in the ToS, you'd have to file a massive lawsuit just to enforce it. And the actual fine would be inconsequential to OpenAI.
I think going forward, any researcher should consider anything submitted to an LLM to be copied/stolen.
If you mean move to products with ZDR policies, OK, very fair and I agree. If you're talking the equivalent of carpenters should give up pneumatic air guns because hammers are more authentic, then that's silly. These are tools, and like any tool how effective they are can come down to how well you use them.
Should they give up pneumatic air guns if the company that supplies then can then control what you build with them, how you build with them, and secretly copies all your designs for their own use. Sure its a good tool, but its also becoming a trap.
So in some very weird way, this is similar to right to repair vs John Deere.
Or is it just capitalism doing capitalism stuff?
I don't think there are any pneumatic air gun "provider"s that come with an associated risk of them claiming your carpentry work.
Universities should soon start having own-hosted AI based off open models
… which would only exacerbate the computational disparity they're operating under.
Like SaaS companies who don’t feed all their stuff to Anthropic, OpenAI and Cursor?
Hmm, is the formal verification through? Lean just asserts no errors in the proof, but like can prerequisites not be fullfilled?
Are you asking if it uses additional axioms of `sorry` in the proof? It's easy to check that it doesn't by compiling it and telling lean to list the axioms.
It's highly non-trivial to confirm that the theorems written in Lean are actually the same as the Navier–Stokes (non-)theorem.
Is it? Clicking around the code it looks like a pretty mechanical translation of the statement on the millennium problem website. Assuming of course that you are willing to trust that e.g. the real numbers definition and API included in MathLib4 is correct, but that feels very safe to me.
I'm not claiming to be an expert on Lean4 (although I have contributed tactics) but this is one of the most direct formalisations I've seen of a serious result (second only to FLT of course, which has a horrible proof but it is trivial to verify the statement)
This right here, or at least the thought of this, is why in the not so far future, businesses can't (won't?) be using these LLMs services.
You cannot risk companies like Anthropic, OpenAI or their business partners like Microsoft having unfettered access to proprietary data on your company/businesses.
It it likely that they or rogue employees will use the information to make a profit? It's pure speculation, but I'd say more than likely, and we will never hear about it or read it on the news unless there's whistleblowers in high enough positions to know about it.
Assuming you and your employees aren't careful with what data you share, they will have intimate knowledge about your company from files and conversations logs. Likely personal user data too which they'll gladly create databases to link to and create extensive profiles on you, your employees and your businesses.
It's not far-fetched to see them leveraging insider information shared with LLMs to play the stock market, leveraging data against competing businesses in other markets they might want to explore, and likely a bunch of other things that are escaping me right now as I write this.
At the end of the day it's on those people for sharing such sensitive data, but it's not like these AI companies are innocent and won't gladly exploit every little byte of data without telling you, we know it happens.
Its not "in the future", its already here, right now. Sensitive IP gets processed on rented or local GPUs running open weight models. Sometimes its required due to data privacy laws, sometimes its because the people running those shops are not trusting OpenAI/Anthropic ZDR policies being observed. Normal, boring, US and EU-domiciled enterprises do this on a regular basis, and there is an industry of companies helping said boring companies set things up.
It is even worse. Just them knowing or having an inkling that someone is close to achieving a solution might be enough for them to spawn a team of thousands of agents and outrun you.
> OpenAI, meanwhile, says its experience with Navier-Stokes could open the door to solving puzzles with more practical relevance. “We are now able to spend millions of dollars on a problem that we really care about and that really matters: developing new materials, finding cures to diseases,” Bubeck said. “All of those things that we have been talking about for a long time—now they seem to be at our fingertips.”
Eh? There's no connection at all between the Navier-Stokes work and those things.
He may be hinting that solving these complex mathematical problems will boost OpenAI clients' confidence and encourage them to spend millions of dollars on solving other complex problems.
I would think it would have the exact opposite effect.
Why would anyone use OpenAI models for anything commercially valuable, or where secrecy is important, when it appears that if OpenAI "becomes aware" that you are doing so they may try to compete with you?
Not only did OpenAI, by their own admission, rush to re-solve Navier-Stokes once they heard the rumor a week ago that it has been solved (the rumor being that it was Anthropic that had done it), but they are leaving the door open ("we cannot rule out that") as to whether the model they used to do it had been trained on the anonymized date from the researchers who's approach they ended up copying.
Terrance Tao has recently said as much for mathematics - that there appears to be a trend (not just this Navier-Stokes incident) of the AI companies going after math problems wherever there is an "rumor" of progress, and that he thinks this may sadly result in breakthrough mathematics being conducted in secret to avoid this.
The rush to steal another researcher's thunder is bad enough, but it also appears that one of OpenAI's employees acted in a very thuggish manner to try to threaten the professor who had been working on this not to publish and to co-operate with their telling of the story.
Yes it is they all require intelligence.
Navier Stokes is a test of how high the intelligence is.
Does it matter who gets the credit at this point? Both used AI to do 99%+ of the work. So... do machines have ego?
They represent different AI usage patterns. OpenAI wants everyone to believe that it was done with a practically autonomous network of thousands of agents with little to no human intervention for 88 hours, while Buckmaster/Alpöge were using AI in a more guided way for months. If OpenAI actually used anything from Buckmaster/Alpöge work they would be misleading the public.
Agree! Not sure I believe that Buckmaster/Alpöge were guiding the AI. This is just their way of saying that they had something in the process and deserve merit.
So you believe they're like "solve navier-stokes make me rich make no mistakes" despite being mathematicians of top ability? Occam's Razor for sure.
Asking the question in the right way may be 99% of the work. And the fact that openAI is effectively snooping on users and then outspending them to announce a break through is just gross.
Is it really? If I ask my swarm of agents to read about every relevant stuff about NS problem online might me more than what any researcher can prompt the machine these days.
I guess, you don't use AI for work? Otherwise, why should you be paid for it? Should you only be paid for the code you actually wrote yourself?
I do. But the difference is: do I go around bragging that my agent worked for 88h to solve a problem? Where is the credit coming from? Is it coming from the: I was the first one to think about throwing a prompt: "Solve Riemann Hypothesis" and it turns out that by luck of the non-deterministic behavior of the agent, it got right? Wow, that is a lot of merit really. Congrats...
Sorry the sarcasm, but really your point makes absolutely no sense. It is completely different to design something with AI and then execute, validate, evolve vs just prompt it machine-g-brrrr style and get a result. This brings an important question. Nowadays I don't write code, I review code, I review systems behavior and get paid for it. Will that be the same for math researchers? Their prompt/problem is already well-posed out there. Ours, in the day-to-day, are not. Will the first one to verify AI work get the credit? or is it going to be the dumdum that types a simple prompt and has the compute to run it for 21321 hours? I absolutely don't get your point here. Or you are just rage baiting
If the machine is highly non-deterministic, it is a matter of luck to get to the result, therefore using agentic swarms to optimize chance.
Machine owners have stocks which valuation must increase to satisfy their debts.
Sad reality
If you take OpenAI at face value, they claim they threw a relatively simple prompt at the problem on a whim and boom presto, a swarm of "agents", 15 million dollars and 90 hours later they disproved the hypothesis. Wow, look at how powerful our AI is, you don't even need to be a world-class mathematician, you just tell it to solve a problem and it does!
By contrast, what the world-class 2 mathematicians did was sat down and started working on their proof for over a year, using AI along the way to help with their research. A much more grounded and realistic use of these tools, but one that doesn't generate nearly as much hype as the alternative.
The cracks in OAI's story has been immediately disproven, and they seemingly plagiarized the work of the 2 and then threw the team of researchers and the 15 million dollars at the problem after the fact. It doesn't exactly bode well for their hype machine when you consider the chain of events here, which is why people care about this, as OAI's constant and incessant lies they spew every minute of every day is finally hopefully catching up to them, and right before their big IPO too.
Editing to add: And I think it's all such a shame. We live in a time with genuinely insanely cool technology that is doing some truly incredible, ground-breaking stuff, but it's all tainted by a gaggle of greedy sociopaths and reprobates whose only goal in life is to have the largest number in their bank accounts. LLMs could've been such an amazingly neutral and cool and useful tool had more level-headed people been at the wheel, but instead we're stuck with this childish bullshit and giving the likes of Sam Altman real power to enact societal collapse.
AI models and in particular LLMs are not capable of logic reasoning. See for example this paper:
https://arxiv.org/abs/2506.06941
Ergo, they can't prove any theorem whatsoever. How do people at OpenAI expect that we believe in claims like that? This is yet another before-the-IPO stunt in my opinion..
Personally, I won't believe any of these claims until the community of mathematicians says otherwise.