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.
Yes. What the headlines hailed as an AGI discovery the facts show more to be someone spending years mining for gold, rumor gets to OpenAI that there might be gold in this specific place, they mine there and instantly discover gold, then tell the world they’ve developed the worlds best gold finding/mining machine.
Separate from all the allegations of more nefarious actions and ethical issues, that’s the most charitable version of what happened here.
they threw it on all the millenial math problems (I think there are 6 at this point unsolved, well, 5 now).
And according to them at some point they saw that one was close to being solved, so they pointed all the agents at it.
The same thing happens to humans - at this time there are no simple problems left, so solving the hard ones requires using prior knowledge and attempts at solving things.
Yeah but the one they decided the AI was close to solving may have been so because the researchers' progress on this problem became part of the training data for that AI...
Almost but not quite I think. You can throw money at parts of problems. I think it's helpful to think it kind of like supercomputer MD/MC or electronic structure calculations. A tool that can get you valuable answers but not necessarily aid understanding. Simulations can be used to aid understanding also, and are integral to theory development. In the same way the approach to this result is.
Plausible deniability - The line of attack is in their sessions/prompts data. Just make the prompt pointed enough that the search space is tractable and use your ginormous compute.
> "Of course we don’t know whether that is true"
Yep. Who is verifying these claims? We all know how trustworthy Altman & Co are.
“relying on” is misleading here relative to what the researchers have said.
If I write a book and pass it through a spelling and polish checker, I still wrote the book and its core IP. I didn’t “rely on” the tool to create the IP.
it’s much more like you come up with the premise and someone else writes the book. the released prompts for other foundational problems (like unit distance) prove that.
The tools the researchers used though was much more than an spellchecker, because spellcheckers don't come up with chains of reasoning for the arguments in the book. The LLMs did in the case of the Navier-Stokes problem.
The researchers were driving prompts and trying to actually do math.
The OpenAI effort was a pure brute force attempt. I'm not even sure an LLM was actually involved. I think they just used their hardware to run the matrix multiplies required by the search for a counter example. Perhaps some clever approach guided the search but that seems to be about it.
that's not how AI was used in this case. It's more like a professor with assistants.
Professor says the assistants - why don't you dig in this direction, I have a hunch it might produce something valuable. And AI assistant does just that, proving or disproving a hunch. This would take the professor a lot of time if doing by themselves.
Yes, and keyboards also save a lot of time over handwriting. Numerical methods and proof engines save even more time. LLMs are just another tool in the kit.
Keyboards don't suggest chains of reasoning or words to type. When I press the K key, I know exactly what will happen. It's just a translation layer that gives an output known ahead of time and thus does not impinge upon the creativity of putting words together.
A better example would be playing chess against a player slightly stronger than me and using a chess computer to suggest some good moves. I could win, but it certianly wouldn't be just my brain that wins. It would be an amalgamation of my brain with a machine that suggests good moves.
This is straight up misleading. When you press your K key on a touchscreen, your keyboard program may decide you meant to press the neighboring L key (by dynamically inflating the collision geometry on it) because it was statistically far more likely that you meant to press the L key next.
This likely doesn't happen exactly on an analog keyboard, but then many text-processing environments that do the same thing in post. My keyboard just edited 'yuor' to 'your' even though I successfully input the prior string.
You can’t do anything novel with these models from scratch and let it fly. I’ve observed something over the past few months
Work on something novel -> llm is kinda useless and low value-add -> Keep at it and in the process feed it more information -> keep doing this periodically -> a few months go by and you realise the model outputs are almost like-for-like regurgitations of what was inputted in some prior period.
Once it’s accumulated new info can it produce something automated that is somewhat useful? Sure.
But by itself - absolutely not.
I clearly see humans will be needed - the best ones that is. For ‘rote work’ and stuff that is not IP sensitive firms will be ok with employees putting that as inputs into models.
But I’d wary about trusting the labs. They will push the letter of the law to the max.
Personally I’ve stopped doing anything novel with these models. If I do use a model on something adjacent but not totally novel I have to craft the inputs in a strategic way not to give much away.
I’d wager firms will soon realise this and that growth rate of revenues of the frontier labs will become questionable. The economic cost that firms have brought out thus far is only financial. There’s a whole bunch of other costs people aren’t talking about.
Agree all. And as the revenues become questionable, the frontier labs practices will necessarily become (more) questionable. Vicious cycle.
To avert that dynamic, the frontier labs must deflect and otherwise act to prevent this controversy from breaking through. Both to the general public, but also more specifically to the firms' decision-makers. All of whom are generally aware of the IP issues, and some of whom are aware of what happened with Cursor and Figma, but with few exceptions have not yet themselves acted to protect their property.
This doesn't follow for me. There are what, Dozens or Erdos tier problems that got solved with no progress for decades? How does that factor in to your view?
IIUC the argument is that while unsolved there was much work done on them that shows up in the training data. The idea being that the LLM is limited to a small amount of inference over externally supplied data.
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.
Prompting them yes, suggesting potentially fruitful research directions and so on, but the actual research was conducted by hundreds of agents swapping millions of messages and using billions of output tokens over 88 hours. The result being a huge Lean proof: https://github.com/openai/NavierStokesAndEuler. It's not just possible for humans to manually guide such a process in a meaningful way. They can set the direction and attempt to understand the result, but they solution itself must emerge (or not) from the agent swarm.
So yes, the models do seem to be "solving" the problems themselves, but not necessarily in the way we think of mathematical discoveries happening. Academic mathematics has historically been resource constrained: There are a limited number of top-level mathematicians, and they only have so much time and brain power to spend. So when approaching a problem, they are essentially forced to be as efficient as possible, not just searching for a solution, but for one that can be achieved within their cognitive budget. This induces them to develop novel techniques and abstractions, and it is actually those techniques and abstractions that tend to be the valuable part for further research, not the proof itself.
An agentic swarm is like getting a single skilled mathematician, cloning them a hundred times, then locking them in a room with the single objective of solving a problem. No longer constrained by time or brain power, they can approach it differently, using pre-existing techniques to gradually build their way to a solution. This process might not require a single intuitive leap or new discovery, and the solution will not be simple or elegant, but they will probably get there. It is more like a process of intelligently guided search than invention.
The OpenAI team didn't make a Lean proof. They brute forced a counter example. The "other" team was doing what you described but they haven't "finished" their work yet. Also, their Lean proof was for a simpler version of the problem, not the full NS.
Also, OpenAI wanted the actual mathematician taken off the resulting paper. I'm not sure I would describe what OpenAI did as research. What the other team was doing does seem to be more like research but the hardware was still in those cases mostly brute forcing things and then doing something like a genetic algorithm to compose an actual proof based upon the results of a large set of brute force attempts.
Didn't OpenAI make a Lean proof?
https://github.com/openai/NavierStokesAndEuler/tree/main/Nav...
"This repository contains Lean 4 formalizations of the results presented in “Finite time blowup for Navier–Stokes” and “Finite time blowup for the Euler equation” by OpenAI."
The efficacy of applied NS was never in doubt. "Checking the box" is downplaying the magnitude of the discovery quite a bit as it has been unsolved for almost 100 years. Yes, this particular problem with NS no real-world applications, but that's true for 99.9% of math research.
Agreed, but i think this underscores my point. We have numerical simulations in materials science too, but that doesn’t mean formally verified theorems about the underlying equations automatically translate to formal (or even informal) verification of simulation results. That’s not to say you can’t make progress with agents, but I think it’s less well defined how you write the goal and progress assessment for an agent
OpenAI (claim to) show the existence of *a* finite time singularity. It could stimulate more research in PDE solving, and maybe physics, but it has zero impact on practical applications, that I can see. The Millenium problems were chosen based on hardness not practical relevance.
> same approach of casually spending a few million on agentic computation is going to solve end to end materials design or drug development."
you're not actually spending that money. it's sunk cost, as you already bought the hardware. at least for the big pharmaceutical companies for drug development. then you run your own local model, trained on special data, with special etc, etc... to the end of buying GPUs for what, 3.5-6.5M/rack or so (GB300 NVL72, Google AI summary pricing quote) becomes a bargain (vs the double digit billions you need to spend on a new drug R&D).
Solve for how to implement and synthesize physically? Not likely.
Humans solved for launching rockets to the Moon on paper decades before it happened.
Pareto type thing; the logical work is the easy 80%. The last 20% is fighting physics.
There is no beating physics but there is still plenty of room for us to improve our understanding of it.
Which we weren't focused on at all sitting millions primates at well understood physical computers searching for Shakespeare Python and Ruby code yet merely getting same old contemporary software outputs.
It does, yes. So designing objections functions and making sure you can afford the training rollouts becomes really important in defining which problems are tractable. It will be really interesting to see how that shapes the kinds of problems people choose to work on
>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?
Yes, definitely! There’s a long history of this and I think there’s tons of opportunities for more. Both for improving the exactness/physical fidelity of models and for developing new approximate theories and simulation methods
I think a lot of people don't understand, with respect to a mathematical theory, the relation between a carefully stated conjecture requiring formal proof vs. using the objects in the theory effectively. Could better understanding of NS lead to better practical tools? Almost certainly, even if only to give us bounds on performance. Has its unresolved status stopped us from using NS? No. Almost no one using it cares. Resolving it is valuable, especially if it comes with mathematical and/or physical insight leading to greater understanding. But it is not this is grand result that like instantly unlocks 100+ day weather forecasts.
It would be like saying proving ergodicity more generally for physical systems would unlock condensed matter physics, ignoring how well stat mech has served us regardless.
I am not anti-AI and I don't think we should stop throwing them at conjectures. I'm against this fundamentally misleading type framing that's become prominent. Millennium prize problems are important. Treating this specific aspect of NS as the one missing piece is just harmful. If we just throw compute at formal conjectures voila cancer and fusion.
I think the better example of "AI" usefulness toward solving problems is AlphaFold, and immensely powerful tool. But also suffering from a false framing/marketing problem as "solving protein folding". It feels like the right use of compute. Considering many factors that we can't hold in our head at once. "Solving" something that was already "solved" via computation (simulation) but now much more efficiently. The output is a valuable tool itself, it was not about "solving the protein folding problem", which it didn't do. It is a tool to solve problems requiring a sequence->ground state calculation. Which is a very broad set.
Formal verification of a conjecture we set up as a benchmark we set to test human understanding is not valuable in the same way.
I'm failing to make multiple points and gotta run, but i think that final point is important. The millennium prizes are not about technological/practical value, at least not intentionally. They're about shit that seems fundamental to us, things that feel[1] to us based on our understanding are important AND feel like they should be solvable in a human-comprehensible way. So formally resolving them with pure compute is not really the point. It seems closer to that story about one of those prime conjectures where some guy just ran brute force enumerations to find a counterexample. Valuable for sure, time-saving. And knowing the answer makes it a lot easier to solve a problem.
TL:DR science and math are more than formally resolving conjectures, they're about building up understanding and tooling that you can then build more on. AI should be an increasingly big part of it, but declaring "AI will solve fusion because it's smart" is like the rest of the fucking owl meme. I have no doubt it will help, most likely via simulations/quicker testing/calculations and verification. Maybe partly via reactor designs. Maybe partly being fed conjectures about bounds/limits that would be useful as inputs for the next iteration. And maybe even in the form of resolving some formally stated conjectures (I don't know enough plasma physics to name any).
[1] obviously to the mathematicians it's more than a feeling..
> 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.
>he specifically notes that they used the paid subscriptions, iirc.
Where are you seeing that? He only says "We used several LLMs throughout: Anthropic’s Claude, OpenAI’s Codex, especially with GPT-5.6 Sol and, more recently, Astra. The latter was only used for writeups and auditing our arguments."
I might be missing something, but he doesn't seem to confirm that he opted out, at least in the written writeup, maybe he has on social media? He also likely had early access to Astra given the timing, and I thought early access customers couldn't opt out? (Am I wrong about that?)
API or consumer subscription? And did he share drafts of the work with anyone who fed it back in on a consumer subscription without disabling training?
I have reason to believe OpenAI doesn't respect training opt outs, but there is a good chance they let something get through without an opt-out too.
> And did he share drafts of the work with anyone who fed it back in on a consumer subscription without disabling training?
To this, the statement does have the following:
"... the one Levent and I had quietly chosen to attack"
Note his collaborator (Levent) works at Anthropic, so presumably he knows about opt ins/outs, etc.
> I have reason to believe OpenAI doesn't respect training opt outs, but there is a good chance they let something get through without an opt-out too.
I believe that, at this point in time, OpenAI's reputation speaks for itself. The stakes for success are already enormous, and the CEO has been repeatedly described by those around him as a pathological liar.
People who choose to expose anything remotely sensitive can surely be expected to know the risks of doing so.
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).
We don’t need to guess, OpenAI pretty much indirectly they had the chats in their data set. OpenAI responses are the most suspicious part of that whole controversy, the fact they do not provide straight answers is not a sign of a good faith actor here
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.
Then OpenAI should acknowledge that they can't prove they solved the problem independently, and credit the external researchers. It cuts both ways: if OpenAI really needs to access user data, even anonymised, to improve its models, they have to waive any pretention to solve "independently" any problem other people worked on with its tools. Otherwise they (OpenAI) have to firewall/cleanroom themselves.
I could see their comment on user training data as a bit of a CYA statement, but removing Alpoge from the paper is awful. Has really soured what could have been a huge moment for AI progress.
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.
Yeah I think the verb "removed" is not the right verb here, because the paper in question is OpenAI's hypothetical paper which Alpöge is not on in the first place.
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".
> [the Open AI rep] twice asserted that he wanted Levent removed from authorship, and said it would all be simple if only it were not the case that, and it was so annoying that, Levent works at Anthropic.
Later on the author claims that the OpenAI rep threatened to ruin his career if he didn't go along with them.
Worth noting that there were two versions of the problem:
- the proof in the equations with viscosity (which OpenAI claims to have solved), and
- the proof with no viscosity (which Tristian and Levent solved)
What is confusing is that if OpenAI can prove their independence from Levent and Tristian, they could take full credit for proving the viscous version of the problem. Offering to give one author credit for something they proved seems like a strange choice: if nothing else it seems obvious that it would drive a very deep wedge between the two authors of the non-viscous version.
It seems very hard for OpenAI to prove that independence. Since they seem unable to exclude the possibility that their model was trained on transcripts by the two mathematicians.
They didn't want his name removed from any paper. The invitation was to write a new joint paper between Buckmaster and OpenAI. An invitation Alpoge couldn't accept and OpenAI wouldn't make since he worked for a competitor.
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.
Isn’t that how research works? You build on what others have done. I don’t understand the big deal. I’d rather have the result available sooner than later just to assuage some egos
The whole thing reeks of the desperation of an unprofitable venture-backed startup looking for its next PR win to keep the wind in the sails.
But I think what’s being overlooked in the race to claim absolute credit is that both sides ultimately relied on a LLM (and one of OpenAI’s at that). Either a human researcher made a breakthrough discovery with the help of Codex, or the latest GPT model made a breakthrough with the help of human training data, or a little of both… either way it is undeniable that LLMs have quickly become an integral part of R&D workflows and are accelerating research.
This would be a major win for any normal company. You could even build a bigger collaboration with this guy, give him a big budget and push for extensions to this preliminary result, and in return do a write up on how he uses your model in his workflow. Huge PR win. What this says to me is that their valuation is so astronomical that they feel the only way to justify it is to demonstrate a fully autonomous discovery bot… which it simply is not.
If you transplant a world class mathematician into a chemistry lab, do you expect similarly ground breaking results? Do you expect a top chemist to make major advances in mathematics?
The frontier labs are likely betting on lay observers (read: investors) confusing headline-grabbing results in abstract mathematics with phenomenal profitability in more grounded endeavours. There is an implicit fallacy that "If our models can solve mathematics they can do everything else."
1. They are massively unprofitable. It is a statement of fact. Nowhere did I say “can’t ever”.
2. Even their pursuit of this problem was itself unprofitable - $15M in compute to solve a problem with a $1M prize. Not that that was the point, but still.
> “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.
I only have an undergrad in math, so very little understanding, but I'd be pretty surprised if it couldn't do forall just as well. Like, say it found this counterexample which relies on axial stretching or whatever approach. Then it already knows how that made the proof work, and can use it to try to prove NS has smooth solutions modulo this particular kind of defect (so it could make some statement about cohomology, or some additional constraining equation). Or if that doesn't work, then it can find a counterexample, which we've established it's good at. Then repeat until you've characterized what does work. The various defects, along with being defect free, become definitions. Now you have a theory.
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.
And yet you still posted this dupe. That quanta piece more duplication. Everything already well discussed in the OpenAI and the Tristan Buckmaster threads! Do better.
I don't think you add value to this conversation, or any of the many conversations in which you do this, by simply pointing out duplicate threads. You'd probably be better off (and less annoying) by simply emailing the mods about the duplication.
Welcome. That's the point tho isn't it: the conversation isn't/wasn't here. It's over there on the source(s). And there's plenty of it. This is a duplicate discussion.
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.
Maybe? But then the parent comment doesn’t make sense either. (There are 2 solved.) Like I said, take the charitable view. To a lot of readers this will be “announcing” the closure of the second of 7 problems so is internally consistent.
FYI: The problem at hand is an existence problem. No real construction of any real formula for the solution is provided, only a singular perturbation expansion.
In short: The problem is about whether a solution (of the NS Equations with external driving force) can be found that blows up in finite time. i.e. exhibits infinite velocity at a point even for a viscous flow.
The solution: Take a circular curl ansatz which shrinks in xy-direction and elongates in z-direction and see whether you can find linearized waves so that these waves show a blow up when propagated on the curl. Then prove that the higher orders of the perturbation are regular before the T0 singularity time and you have solved the problem. The external force is just the remainder of the NS-Equation right hand side.
It is a lot of tedious formula juggling of all the higher orders and some singular perturbation expansions. Perfectly suited for algebra systems. OpenAI was using probably python sympy for the formula work and the researchers had to guide the LLM what to do in higher mathematical language.
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.
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.”
Even in the past a lot of “aristocrats” had to earn a living. Among scholars, many worked as teachers or had sinecures that paid the bills, or held clergy posts with minimal responsibilities.
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.
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.
>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.
Question for the maths people please: Is this solution related to strange attractors? Looking at the visualization my mind can’t help but see a resemblance. I would really appreciate anyone’s 2-cents :)
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.
> 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.
Or they can simply turn off the setting that allows OpenAI to use their chats to improve the model. Or they can use the API where it is off by default.. If the advantage of using OpenAI models will be significant enough for the business in question, these are the options.
>You cannot risk companies like Anthropic, OpenAI or their business partners like Microsoft having unfettered access to proprietary data on your company/businesses.
You do realize that businesses that have contracts with them can specify if they want their data used for training or not right?
"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.
I thought as much- my point is that as AI capabilities continue to expand, AI skeptics inadvertently and ironically end up belittling the humans they presumably hold in high esteem vs. the "cold machines" that aren't capable of true thought or creativity. When one says that solving a Millennium prize problem is not impressive, one is essentially demeaning practically all mathematicians and the field of mathematics itself.
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.
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.
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.
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.
It is capitalism doing capitalism stuff, but more fundamentally technology is allowing for more centralized control of more things by fewer people. Regardless of ideology, increasing concentration of power has bad outcomes for people (except the ones in power).
What can be done to prevent hostile take over of scientific research from humans by AI ? I hear lot of complaints and hue and cry (fair enough) but are there positive ideas on what to do about this ? (Regressing back to being secretive about one’s scientific endeavor is not the answer)
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.
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)
> 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 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.
>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.
This is just lawyer speak. Maybe there was a small reward from a possible thumbs up on any of the chat sessions. Open AI have no way of knowing if that happened or not and the chances that, if this did happen, that it had anything to do with their solution of Navier Stokes is extremely unlikely.
>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.
There was never a threat to not publish their own work with whatever credit to whoever. This was about the offer to be a lead author on the paper that Open AI authored, an invitation that was not extended to Levant.
Yes they know the timelines, which they've explained. No they don't know exactly what they train on. Even I don't, and my little experiments are nowhere near OpenAI scale. This is par the course for ML. Plus it would kind of defeat the purpose of de-anonimization if they could.
Perhaps the question should not be "Is OpenAI trustworthy?" but instead "Is any company trustworthy? What does vast amounts of capital do to the trustworthiness of an entity?"
You know, everyone's focused on the math and the human drama aspects, but to me the real story should be about this accusation that they somehow read the stream of data these guys were generating and then reacted to it at all on a human level is pure poison for their hopes for enterprises to be using their software.
Even if these two mathematicians were using the AI services under a clause that nominally allows OpenAI to train on their data, it is still another level above for there to exist some pathway within OpenAI to know that someone is doing something very valuable and important with their AI and to swoop in to try to steal the value of that work. It doesn't matter exactly what that pathway is, just that it exists is a big deal. Today it's a Millennium Prize, but tomorrow, is it the next hot new product category? Is it the patent someone is working on? Does OpenAI constitutionally believe that you may be using their product but whatever you produce really belongs to them and you are just borrowing it? Can we trust contracts that promise that they don't believe that if this is how they act?
Even people who are consciously aware that their sessions are being used to train the AI don't expect the AI companies to be in some way scanning the stream of what AI is working on for high-value propositions to snipe. That changes the relationship between these companies and enterprises, and anyone who thinks they may be doing this sort of work, deeply and fundamentally.
It isn't just that OpenAI is now something we should be suspicious about for math. It's all high-value science. Is there anyone trying to figure out how to develop a next-generation AI architecture using OpenAI? Better stop, OpenAI could see it and scoop you out of who knows how much value.
There is an old story attached to many historical figures that goes:
Churchill: Madam, would you sleep with me for a million pounds?
Woman: My goodness… well, I suppose I would.
Churchill: Would you sleep with me for a pound?
Woman: Certainly not! What kind of woman do you think I am?
Churchill: Madam, we’ve already established that. Now we are
just haggling over the price.
If this accusation is true, which I'm not completely confident about, but if it is true, that is the situation we would be in... we would have established that OpenAI is willing to steal from its customers, the only question is where the line is now, and where the line might be in the future.
Honestly the human drama, while the compelling story, is in monetary terms orders of magnitude less important than the question of whether OpenAI has a mechanism to steal ideas from its customers. Has this happened before and they just successfully covered it up? Or maybe the people stolen from thought it was innocent and just a coincidence that they were scooped? If it established that there is a price, I have a lot of questions about that price.
How ironic that academic institutions, that became outrageously expensive on purpose, are now complaining that academic research is too expensive. This is coming from universities with already incredible endowments. They made science pay-to-play but now don't like that their own rules are being applied to them. Maybe instead of giving money as a bribe to get your kid into a good college, you can give the college some GPU's?
This article reads like it was written by someone who has done less research than the average HN poster. Not a single word of OpenAI threatening people or apologizing for threatening people.
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.
LLMs pattern match based on the prompt. Go ask for medical with my tummy hurts and patient presents with intestinal cramps and see how asking a question as an expert changes the interaction
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.
>what the world-class 2 mathematicians did was sat down and started working on their proof for over a year
If they were not related to anthropic I'd probably agree with you.
OpenAI is much more for science than they are imo.
Anthropic culture is all about "machine go brrrr" more than all of the other labs.
If they had access to better models they'd probably would've one-shotted the solution.
When the creator of bun was just "vibe-sciencing" it was ok. There is little to no evidence that they've been working using AI in this problem for over a year. Maybe they've been working on the problem for decades. So many other scientist have. Are they better because they threw a prompt and let it go brr??
When we put this in the perspective of how agents are changing the landscape of math/science, true it is shitty and weird. When folks are saying these scientists by anthropic that vibe-science'd the solution are victims, just because they did it with a smaller model, it is not defensible imo. And credit loses meaning here.
The credit is shared with all the scientists that contributed somehow with the data in the AI pre-pos/training and not the prompter.
> If they were not related to anthropic I'd probably agree with you.
What does the company they work for (only 1 of them, mind you) have anything to do with the topic at hand? They were using both Anthropic & OAI models during their research, and they were doing it separate to their work as independent researchers rather than as employees of any specific company. In fact, this makes OAIs actions even worse because they tried a bribe in order to slice the Anthropic employee out of the deal.
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.
They didn't write a traditional proof, but a lean program, which can be used to validate proofs formally, using a computer. It's still up to humans to check wether the formalization is sensible, but the proof is correct.
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.
Yes. What the headlines hailed as an AGI discovery the facts show more to be someone spending years mining for gold, rumor gets to OpenAI that there might be gold in this specific place, they mine there and instantly discover gold, then tell the world they’ve developed the worlds best gold finding/mining machine.
Separate from all the allegations of more nefarious actions and ethical issues, that’s the most charitable version of what happened here.
they threw it on all the millenial math problems (I think there are 6 at this point unsolved, well, 5 now).
And according to them at some point they saw that one was close to being solved, so they pointed all the agents at it.
The same thing happens to humans - at this time there are no simple problems left, so solving the hard ones requires using prior knowledge and attempts at solving things.
Yeah but the one they decided the AI was close to solving may have been so because the researchers' progress on this problem became part of the training data for that AI...
Almost but not quite I think. You can throw money at parts of problems. I think it's helpful to think it kind of like supercomputer MD/MC or electronic structure calculations. A tool that can get you valuable answers but not necessarily aid understanding. Simulations can be used to aid understanding also, and are integral to theory development. In the same way the approach to this result is.
Worth noting they claim they did not choose the line of attack. Of course we don’t know whether that is true.
Plausible deniability - The line of attack is in their sessions/prompts data. Just make the prompt pointed enough that the search space is tractable and use your ginormous compute.
> "Of course we don’t know whether that is true"
Yep. Who is verifying these claims? We all know how trustworthy Altman & Co are.
Yeah, they didn't choose the line of attack, the person they copied it from did..
but the researchers were also largely relying on AI
“relying on” is misleading here relative to what the researchers have said.
If I write a book and pass it through a spelling and polish checker, I still wrote the book and its core IP. I didn’t “rely on” the tool to create the IP.
it’s much more like you come up with the premise and someone else writes the book. the released prompts for other foundational problems (like unit distance) prove that.
The tools the researchers used though was much more than an spellchecker, because spellcheckers don't come up with chains of reasoning for the arguments in the book. The LLMs did in the case of the Navier-Stokes problem.
If this were the case the problem would not have remained unsolved for this long. A new spell checker is not what cracked the problem.
The researchers were driving prompts and trying to actually do math.
The OpenAI effort was a pure brute force attempt. I'm not even sure an LLM was actually involved. I think they just used their hardware to run the matrix multiplies required by the search for a counter example. Perhaps some clever approach guided the search but that seems to be about it.
In the same way you rely on a keyboard or touchscreen to type this comment. It doesn't mean the tool is the brain behind the work.
that's not how AI was used in this case. It's more like a professor with assistants.
Professor says the assistants - why don't you dig in this direction, I have a hunch it might produce something valuable. And AI assistant does just that, proving or disproving a hunch. This would take the professor a lot of time if doing by themselves.
Yes, and keyboards also save a lot of time over handwriting. Numerical methods and proof engines save even more time. LLMs are just another tool in the kit.
Keyboards don't suggest chains of reasoning or words to type. When I press the K key, I know exactly what will happen. It's just a translation layer that gives an output known ahead of time and thus does not impinge upon the creativity of putting words together.
A better example would be playing chess against a player slightly stronger than me and using a chess computer to suggest some good moves. I could win, but it certianly wouldn't be just my brain that wins. It would be an amalgamation of my brain with a machine that suggests good moves.
One cannot simply reason by analogy.
> Keyboards don't suggest chains of reasoning or words to type
My iPhone keyboard does
I was talking about regular old keyboards. But you're just being pedantic.
This is straight up misleading. When you press your K key on a touchscreen, your keyboard program may decide you meant to press the neighboring L key (by dynamically inflating the collision geometry on it) because it was statistically far more likely that you meant to press the L key next.
This likely doesn't happen exactly on an analog keyboard, but then many text-processing environments that do the same thing in post. My keyboard just edited 'yuor' to 'your' even though I successfully input the prior string.
frankly don’t know how to reply to these sorts of comments anymore
That's usually a good sign you are on shaky ground!
Obvious false analogy in your earlier argument.
No so obvious to this guy.
it is truly not obvious to you why keyboard isn’t a good analogy for LLM?
You can’t do anything novel with these models from scratch and let it fly. I’ve observed something over the past few months
Work on something novel -> llm is kinda useless and low value-add -> Keep at it and in the process feed it more information -> keep doing this periodically -> a few months go by and you realise the model outputs are almost like-for-like regurgitations of what was inputted in some prior period.
Once it’s accumulated new info can it produce something automated that is somewhat useful? Sure.
But by itself - absolutely not.
I clearly see humans will be needed - the best ones that is. For ‘rote work’ and stuff that is not IP sensitive firms will be ok with employees putting that as inputs into models.
But I’d wary about trusting the labs. They will push the letter of the law to the max.
Personally I’ve stopped doing anything novel with these models. If I do use a model on something adjacent but not totally novel I have to craft the inputs in a strategic way not to give much away.
I’d wager firms will soon realise this and that growth rate of revenues of the frontier labs will become questionable. The economic cost that firms have brought out thus far is only financial. There’s a whole bunch of other costs people aren’t talking about.
Agree all. And as the revenues become questionable, the frontier labs practices will necessarily become (more) questionable. Vicious cycle.
To avert that dynamic, the frontier labs must deflect and otherwise act to prevent this controversy from breaking through. Both to the general public, but also more specifically to the firms' decision-makers. All of whom are generally aware of the IP issues, and some of whom are aware of what happened with Cursor and Figma, but with few exceptions have not yet themselves acted to protect their property.
[dead]
I think you stopped at the wrong time with the wrong perspective. Why can't that info accumulation part also be made more self-contained?
I guess I'm having trouble unraveling your experience and personal usage vs. what you're concluding about the labs.
[dead]
This doesn't follow for me. There are what, Dozens or Erdos tier problems that got solved with no progress for decades? How does that factor in to your view?
IIUC the argument is that while unsolved there was much work done on them that shows up in the training data. The idea being that the LLM is limited to a small amount of inference over externally supplied data.
[dead]
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.
Prompting them yes, suggesting potentially fruitful research directions and so on, but the actual research was conducted by hundreds of agents swapping millions of messages and using billions of output tokens over 88 hours. The result being a huge Lean proof: https://github.com/openai/NavierStokesAndEuler. It's not just possible for humans to manually guide such a process in a meaningful way. They can set the direction and attempt to understand the result, but they solution itself must emerge (or not) from the agent swarm.
So yes, the models do seem to be "solving" the problems themselves, but not necessarily in the way we think of mathematical discoveries happening. Academic mathematics has historically been resource constrained: There are a limited number of top-level mathematicians, and they only have so much time and brain power to spend. So when approaching a problem, they are essentially forced to be as efficient as possible, not just searching for a solution, but for one that can be achieved within their cognitive budget. This induces them to develop novel techniques and abstractions, and it is actually those techniques and abstractions that tend to be the valuable part for further research, not the proof itself.
An agentic swarm is like getting a single skilled mathematician, cloning them a hundred times, then locking them in a room with the single objective of solving a problem. No longer constrained by time or brain power, they can approach it differently, using pre-existing techniques to gradually build their way to a solution. This process might not require a single intuitive leap or new discovery, and the solution will not be simple or elegant, but they will probably get there. It is more like a process of intelligently guided search than invention.
The OpenAI team didn't make a Lean proof. They brute forced a counter example. The "other" team was doing what you described but they haven't "finished" their work yet. Also, their Lean proof was for a simpler version of the problem, not the full NS.
Also, OpenAI wanted the actual mathematician taken off the resulting paper. I'm not sure I would describe what OpenAI did as research. What the other team was doing does seem to be more like research but the hardware was still in those cases mostly brute forcing things and then doing something like a genetic algorithm to compose an actual proof based upon the results of a large set of brute force attempts.
Didn't OpenAI make a Lean proof? https://github.com/openai/NavierStokesAndEuler/tree/main/Nav... "This repository contains Lean 4 formalizations of the results presented in “Finite time blowup for Navier–Stokes” and “Finite time blowup for the Euler equation” by OpenAI."
[dead]
Theres a reason those same mathematicians did not solve the problem on their own. Minimizing the impact the model made here seems unjustified.
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.
The efficacy of applied NS was never in doubt. "Checking the box" is downplaying the magnitude of the discovery quite a bit as it has been unsolved for almost 100 years. Yes, this particular problem with NS no real-world applications, but that's true for 99.9% of math research.
There is no NS proof here. Its just a counter example. There is another team working on a proof but they aren't associated with OpenAI.
Agreed, but i think this underscores my point. We have numerical simulations in materials science too, but that doesn’t mean formally verified theorems about the underlying equations automatically translate to formal (or even informal) verification of simulation results. That’s not to say you can’t make progress with agents, but I think it’s less well defined how you write the goal and progress assessment for an agent
you're as sure of what you say as wrong about it.
Note that your reply has exactly 0 value for anyone who doesn’t already know where and how the parent poster is wrong.
fair enough
which part is wrong?
> For any practical application, numerical solvers for Navier-Stokes already exist and do a good job.
or
> This proof is just checking the boxes for mathematicians.
If that were true you could explain it. There are lots of solvers for navier stokes simulations and they do a good job.
I was referring mostly to
> This proof is just checking the boxes for mathematicians
There are already quite a lot of summaries of the story that lead to the solution, and the impact that the intermediate results have had.
True, this is just a much bigger one with a vastly larger amounts of hardware.
The same could be said of your post.
OpenAI (claim to) show the existence of *a* finite time singularity. It could stimulate more research in PDE solving, and maybe physics, but it has zero impact on practical applications, that I can see. The Millenium problems were chosen based on hardness not practical relevance.
I was referring to the "it's just mathematicians checking boxes" claim
[dead]
> same approach of casually spending a few million on agentic computation is going to solve end to end materials design or drug development."
you're not actually spending that money. it's sunk cost, as you already bought the hardware. at least for the big pharmaceutical companies for drug development. then you run your own local model, trained on special data, with special etc, etc... to the end of buying GPUs for what, 3.5-6.5M/rack or so (GB300 NVL72, Google AI summary pricing quote) becomes a bargain (vs the double digit billions you need to spend on a new drug R&D).
Solve logically? Sure.
Solve for how to implement and synthesize physically? Not likely.
Humans solved for launching rockets to the Moon on paper decades before it happened.
Pareto type thing; the logical work is the easy 80%. The last 20% is fighting physics.
There is no beating physics but there is still plenty of room for us to improve our understanding of it.
Which we weren't focused on at all sitting millions primates at well understood physical computers searching for Shakespeare Python and Ruby code yet merely getting same old contemporary software outputs.
[dead]
> Those problems can’t be formally verified with an automated theorem prover.
It certainly seems like any problem that is amenable to reinforcement learning will be solved.
It does, yes. So designing objections functions and making sure you can afford the training rollouts becomes really important in defining which problems are tractable. It will be really interesting to see how that shapes the kinds of problems people choose to work on
>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.
> results from GenAI so far have been limited to finding counterexamples
Not all.
Ehrhart’s volume conjecture
Quantum parallel repetition for general two-player quantum games
Erdős Problem #183 on multicolor Ramsey numbers
Erdős–Sárközy Problem #12(i)/(ii)
Erdős Problem #125
Log-concavity of codimension-3, type-2 pure O-sequences
Optimal O(1/t) last-iterate convergence for Anchored Gradient Descent-Ascent
True, these results are from last month. My info was a little out of date.
Prior updated :)
Yes, definitely! There’s a long history of this and I think there’s tons of opportunities for more. Both for improving the exactness/physical fidelity of models and for developing new approximate theories and simulation methods
Working with AI on science (not LLMs though), couldn't agree more.
The TL;DR is still "AI helpful, but not end of the line". The live discussion about these matters is always ridiculously inflated by hyperbole.
I think a lot of people don't understand, with respect to a mathematical theory, the relation between a carefully stated conjecture requiring formal proof vs. using the objects in the theory effectively. Could better understanding of NS lead to better practical tools? Almost certainly, even if only to give us bounds on performance. Has its unresolved status stopped us from using NS? No. Almost no one using it cares. Resolving it is valuable, especially if it comes with mathematical and/or physical insight leading to greater understanding. But it is not this is grand result that like instantly unlocks 100+ day weather forecasts.
It would be like saying proving ergodicity more generally for physical systems would unlock condensed matter physics, ignoring how well stat mech has served us regardless.
I am not anti-AI and I don't think we should stop throwing them at conjectures. I'm against this fundamentally misleading type framing that's become prominent. Millennium prize problems are important. Treating this specific aspect of NS as the one missing piece is just harmful. If we just throw compute at formal conjectures voila cancer and fusion.
I think the better example of "AI" usefulness toward solving problems is AlphaFold, and immensely powerful tool. But also suffering from a false framing/marketing problem as "solving protein folding". It feels like the right use of compute. Considering many factors that we can't hold in our head at once. "Solving" something that was already "solved" via computation (simulation) but now much more efficiently. The output is a valuable tool itself, it was not about "solving the protein folding problem", which it didn't do. It is a tool to solve problems requiring a sequence->ground state calculation. Which is a very broad set.
Formal verification of a conjecture we set up as a benchmark we set to test human understanding is not valuable in the same way.
I'm failing to make multiple points and gotta run, but i think that final point is important. The millennium prizes are not about technological/practical value, at least not intentionally. They're about shit that seems fundamental to us, things that feel[1] to us based on our understanding are important AND feel like they should be solvable in a human-comprehensible way. So formally resolving them with pure compute is not really the point. It seems closer to that story about one of those prime conjectures where some guy just ran brute force enumerations to find a counterexample. Valuable for sure, time-saving. And knowing the answer makes it a lot easier to solve a problem.
TL:DR science and math are more than formally resolving conjectures, they're about building up understanding and tooling that you can then build more on. AI should be an increasingly big part of it, but declaring "AI will solve fusion because it's smart" is like the rest of the fucking owl meme. I have no doubt it will help, most likely via simulations/quicker testing/calculations and verification. Maybe partly via reactor designs. Maybe partly being fed conjectures about bounds/limits that would be useful as inputs for the next iteration. And maybe even in the form of resolving some formally stated conjectures (I don't know enough plasma physics to name any).
[1] obviously to the mathematicians it's more than a feeling..
[dead]
[dead]
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.
Don't say that - he'll start making sure everyone knows who he is
I think he's well on his way. Math friends that would have said "Altman who?" a week ago are now saying "Don't talk to me about that #@$!@&!"
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.
The paid subscriptions have opt-out for sharing data for training purposes. I think it's on by default.
I don’t know because I use Anthropic, but I would eat my hat if this was on by default.
It's opt-out for personal plans, and opt-in for business pla s and API.
This is explained on the page[1] linked to from the privacy section of the pricing page.
[1]: https://help.openai.com/en/articles/5722486-how-your-data-is...
>he specifically notes that they used the paid subscriptions, iirc.
Where are you seeing that? He only says "We used several LLMs throughout: Anthropic’s Claude, OpenAI’s Codex, especially with GPT-5.6 Sol and, more recently, Astra. The latter was only used for writeups and auditing our arguments."
I might be missing something, but he doesn't seem to confirm that he opted out, at least in the written writeup, maybe he has on social media? He also likely had early access to Astra given the timing, and I thought early access customers couldn't opt out? (Am I wrong about that?)
It's in this statement he released (linked in the article) [0]:
"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
API or consumer subscription? And did he share drafts of the work with anyone who fed it back in on a consumer subscription without disabling training?
I have reason to believe OpenAI doesn't respect training opt outs, but there is a good chance they let something get through without an opt-out too.
> API or consumer subscription
It's not given in the statement, so I don't know
> And did he share drafts of the work with anyone who fed it back in on a consumer subscription without disabling training?
To this, the statement does have the following:
"... the one Levent and I had quietly chosen to attack"
Note his collaborator (Levent) works at Anthropic, so presumably he knows about opt ins/outs, etc.
> I have reason to believe OpenAI doesn't respect training opt outs, but there is a good chance they let something get through without an opt-out too.
I believe that, at this point in time, OpenAI's reputation speaks for itself. The stakes for success are already enormous, and the CEO has been repeatedly described by those around him as a pathological liar.
People who choose to expose anything remotely sensitive can surely be expected to know the risks of doing so.
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).
We don’t need to guess, OpenAI pretty much indirectly they had the chats in their data set. OpenAI responses are the most suspicious part of that whole controversy, the fact they do not provide straight answers is not a sign of a good faith actor here
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.
Then OpenAI should acknowledge that they can't prove they solved the problem independently, and credit the external researchers. It cuts both ways: if OpenAI really needs to access user data, even anonymised, to improve its models, they have to waive any pretention to solve "independently" any problem other people worked on with its tools. Otherwise they (OpenAI) have to firewall/cleanroom themselves.
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
I could see their comment on user training data as a bit of a CYA statement, but removing Alpoge from the paper is awful. Has really soured what could have been a huge moment for AI progress.
> 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.
Yeah I think the verb "removed" is not the right verb here, because the paper in question is OpenAI's hypothetical paper which Alpöge is not on in the first place.
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".
> [the Open AI rep] twice asserted that he wanted Levent removed from authorship, and said it would all be simple if only it were not the case that, and it was so annoying that, Levent works at Anthropic.
Later on the author claims that the OpenAI rep threatened to ruin his career if he didn't go along with them.
Worth noting that there were two versions of the problem:
- the proof in the equations with viscosity (which OpenAI claims to have solved), and
- the proof with no viscosity (which Tristian and Levent solved)
What is confusing is that if OpenAI can prove their independence from Levent and Tristian, they could take full credit for proving the viscous version of the problem. Offering to give one author credit for something they proved seems like a strange choice: if nothing else it seems obvious that it would drive a very deep wedge between the two authors of the non-viscous version.
see https://cims.nyu.edu/~tristanb/statement.pdf#page=3
It seems very hard for OpenAI to prove that independence. Since they seem unable to exclude the possibility that their model was trained on transcripts by the two mathematicians.
If that's true, either they both deserve credit or neither of them do. You don't just average 0 and 2 and decide that <n> = 1 person deserves credit.
And yet it happens constantly in the history of science
Ah, I missed that part, thanks!
They didn't want his name removed from any paper. The invitation was to write a new joint paper between Buckmaster and OpenAI. An invitation Alpoge couldn't accept and OpenAI wouldn't make since he worked for a competitor.
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.
That’s the definition of current LLMs. They have trained “borrowed” on whatever humans have documented digitally and physically (books).
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.
This is the take I agree.
It is mean spirited but nevertheless sold their model
Yea, strongly agree. I think this is going to back-fire spectacularly. They better start preparing an apology...
Isn’t that how research works? You build on what others have done. I don’t understand the big deal. I’d rather have the result available sooner than later just to assuage some egos
I’m not a math researcher, so I can’t say. But in bird culture we’d call this a dick move.
The whole thing reeks of the desperation of an unprofitable venture-backed startup looking for its next PR win to keep the wind in the sails.
But I think what’s being overlooked in the race to claim absolute credit is that both sides ultimately relied on a LLM (and one of OpenAI’s at that). Either a human researcher made a breakthrough discovery with the help of Codex, or the latest GPT model made a breakthrough with the help of human training data, or a little of both… either way it is undeniable that LLMs have quickly become an integral part of R&D workflows and are accelerating research.
This would be a major win for any normal company. You could even build a bigger collaboration with this guy, give him a big budget and push for extensions to this preliminary result, and in return do a write up on how he uses your model in his workflow. Huge PR win. What this says to me is that their valuation is so astronomical that they feel the only way to justify it is to demonstrate a fully autonomous discovery bot… which it simply is not.
A company that can solve Millenium problems is somehow still can’t ever make profits. How did you come to that conclusion
If you transplant a world class mathematician into a chemistry lab, do you expect similarly ground breaking results? Do you expect a top chemist to make major advances in mathematics?
The frontier labs are likely betting on lay observers (read: investors) confusing headline-grabbing results in abstract mathematics with phenomenal profitability in more grounded endeavours. There is an implicit fallacy that "If our models can solve mathematics they can do everything else."
1. They are massively unprofitable. It is a statement of fact. Nowhere did I say “can’t ever”.
2. Even their pursuit of this problem was itself unprofitable - $15M in compute to solve a problem with a $1M prize. Not that that was the point, but still.
> “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.
I only have an undergrad in math, so very little understanding, but I'd be pretty surprised if it couldn't do forall just as well. Like, say it found this counterexample which relies on axial stretching or whatever approach. Then it already knows how that made the proof work, and can use it to try to prove NS has smooth solutions modulo this particular kind of defect (so it could make some statement about cohomology, or some additional constraining equation). Or if that doesn't work, then it can find a counterexample, which we've established it's good at. Then repeat until you've characterized what does work. The various defects, along with being defect free, become definitions. Now you have a theory.
>Then it already knows how that made the proof work..
I think you cannot assume so, because pattern matching is not reasoning.
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.
> it convinces decision makers that human mathematicians are obsolete, and it convinces young people that their passion for mathematics has no future
Maybe those things are true, so maybe they should be convinced?
In that original statement you can easily substitute "mathematicians" for "programmers", "researchers", "writers", "designers", "teachers", etc, etc.
I don't see why mathematicians think they should be an exception here.
P=NP is for when both AI shops decide they want to go bankrupt LOL
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-...
And yet you still posted this dupe. That quanta piece more duplication. Everything already well discussed in the OpenAI and the Tristan Buckmaster threads! Do better.
I don't think you add value to this conversation, or any of the many conversations in which you do this, by simply pointing out duplicate threads. You'd probably be better off (and less annoying) by simply emailing the mods about the duplication.
Welcome. That's the point tho isn't it: the conversation isn't/wasn't here. It's over there on the source(s). And there's plenty of it. This is a duplicate discussion.
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.
Many mathematicians would be willing to end their careers for $1m. What makes this so sad is that OpenAI spent more than that for this empty PR stunt.
> 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.
Not really. There's a non-pedantic, charitable interpretation widely available. It's below for reference.
> Navier-Stokes is one of six [open] “Millennium Problems” on a list compiled by the Clay Mathematics Institute in 2000.
If solved problems don’t count anymore, the sentence also doesn’t make sense because now navier stokes apparently isn’t open anymore too, right?
Maybe? But then the parent comment doesn’t make sense either. (There are 2 solved.) Like I said, take the charitable view. To a lot of readers this will be “announcing” the closure of the second of 7 problems so is internally consistent.
Interestingly of the two solved, both have rejected the prize money.
FYI: The problem at hand is an existence problem. No real construction of any real formula for the solution is provided, only a singular perturbation expansion.
In short: The problem is about whether a solution (of the NS Equations with external driving force) can be found that blows up in finite time. i.e. exhibits infinite velocity at a point even for a viscous flow.
The solution: Take a circular curl ansatz which shrinks in xy-direction and elongates in z-direction and see whether you can find linearized waves so that these waves show a blow up when propagated on the curl. Then prove that the higher orders of the perturbation are regular before the T0 singularity time and you have solved the problem. The external force is just the remainder of the NS-Equation right hand side.
It is a lot of tedious formula juggling of all the higher orders and some singular perturbation expansions. Perfectly suited for algebra systems. OpenAI was using probably python sympy for the formula work and the researchers had to guide the LLM what to do in higher mathematical language.
Here is the paper:
https://cdn.openai.com/pdf/32d9f210-8b73-45e0-91bc-82a30aef8...
when you upload it to chatgpt astra can explain what they do and why it works, have fun.
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.
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.
Even in the past a lot of “aristocrats” had to earn a living. Among scholars, many worked as teachers or had sinecures that paid the bills, or held clergy posts with minimal responsibilities.
Aristocrats were a dime a dozen.
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.
How many Ramanujan didn’t get the same opportunity to show their work to what was considered the intelligentsia of that time?
Irrelevant in 2026, you can share your results with a click.
Ramanujan was a phenomenon
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.
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.
>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?
Question for the maths people please: Is this solution related to strange attractors? Looking at the visualization my mind can’t help but see a resemblance. I would really appreciate anyone’s 2-cents :)
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.
> 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.
Or they can simply turn off the setting that allows OpenAI to use their chats to improve the model. Or they can use the API where it is off by default.. If the advantage of using OpenAI models will be significant enough for the business in question, these are the options.
>You cannot risk companies like Anthropic, OpenAI or their business partners like Microsoft having unfettered access to proprietary data on your company/businesses.
You do realize that businesses that have contracts with them can specify if they want their data used for training or not right?
"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
I thought as much- my point is that as AI capabilities continue to expand, AI skeptics inadvertently and ironically end up belittling the humans they presumably hold in high esteem vs. the "cold machines" that aren't capable of true thought or creativity. When one says that solving a Millennium prize problem is not impressive, one is essentially demeaning practically all mathematicians and the field of mathematics itself.
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 you want to be pedantic it’s one of the 7 problems a specific institute considers to be the most important in mathematics: https://en.wikipedia.org/wiki/Millennium_Prize_Problems
(Not that I think the comparison to pi digits make sense)
are we really moving the goalpost after solving Millenium Prize Problem? Six years ago that would be something, but today let's move the goalpost
Willing to bet if an AI next cures a cancer people here will go “that wasn’t the most dangerous type of cancer so it is meaningless”.
If anything I'm diminishing the importance of calculus and pi by comparing it to this bullshit
It's a really bad analogy then. So bad that it's hard to find an analogy describing how bad it is :)
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.
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.
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.
ChatGPT can also simple tell your ideas to another user.
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?
It is capitalism doing capitalism stuff, but more fundamentally technology is allowing for more centralized control of more things by fewer people. Regardless of ideology, increasing concentration of power has bad outcomes for people (except the ones in power).
I don't think there are any pneumatic air gun "provider"s that come with an associated risk of them claiming your carpentry work.
… 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?
A better alternative is just to make all your work open and public, then everyone can see what you should get credit for.
Universities should soon start having own-hosted AI based off open models
What can be done to prevent hostile take over of scientific research from humans by AI ? I hear lot of complaints and hue and cry (fair enough) but are there positive ideas on what to do about this ? (Regressing back to being secretive about one’s scientific endeavor is not the answer)
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.
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)
They actually used Lean statements that were carefully human-written and human-reviewed, from here https://github.com/google-deepmind/formal-conjectures/blob/m...
This doesn't guarantee that the statement is correct (Lean cannot do that), but makes it highly likely.
> 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 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.
>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.
This is just lawyer speak. Maybe there was a small reward from a possible thumbs up on any of the chat sessions. Open AI have no way of knowing if that happened or not and the chances that, if this did happen, that it had anything to do with their solution of Navier Stokes is extremely unlikely.
>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.
There was never a threat to not publish their own work with whatever credit to whoever. This was about the offer to be a lead author on the paper that Open AI authored, an invitation that was not extended to Levant.
OpenAI know the exact timelines involved, and what they train on, or do not.
You're right - it is exactly "lawyer speak", rather like Bill Clinton's "I did not have sex with that woman".
Yes they know the timelines, which they've explained. No they don't know exactly what they train on. Even I don't, and my little experiments are nowhere near OpenAI scale. This is par the course for ML. Plus it would kind of defeat the purpose of de-anonimization if they could.
Because AI supposedly provides a significant advantage over not using AI and those who would trust OpenAI might get a significant edge.
They might, or they might just get out-spent and scooped by OpenAI.
This isn't the way you build trust.
IOW is just marketing. My point stands.
Yes it is they all require intelligence.
Navier Stokes is a test of how high the intelligence is.
Intelligence is required to understand that is clueless nonsense.
Perhaps the question should not be "Is OpenAI trustworthy?" but instead "Is any company trustworthy? What does vast amounts of capital do to the trustworthiness of an entity?"
You know, everyone's focused on the math and the human drama aspects, but to me the real story should be about this accusation that they somehow read the stream of data these guys were generating and then reacted to it at all on a human level is pure poison for their hopes for enterprises to be using their software.
Even if these two mathematicians were using the AI services under a clause that nominally allows OpenAI to train on their data, it is still another level above for there to exist some pathway within OpenAI to know that someone is doing something very valuable and important with their AI and to swoop in to try to steal the value of that work. It doesn't matter exactly what that pathway is, just that it exists is a big deal. Today it's a Millennium Prize, but tomorrow, is it the next hot new product category? Is it the patent someone is working on? Does OpenAI constitutionally believe that you may be using their product but whatever you produce really belongs to them and you are just borrowing it? Can we trust contracts that promise that they don't believe that if this is how they act?
Even people who are consciously aware that their sessions are being used to train the AI don't expect the AI companies to be in some way scanning the stream of what AI is working on for high-value propositions to snipe. That changes the relationship between these companies and enterprises, and anyone who thinks they may be doing this sort of work, deeply and fundamentally.
It isn't just that OpenAI is now something we should be suspicious about for math. It's all high-value science. Is there anyone trying to figure out how to develop a next-generation AI architecture using OpenAI? Better stop, OpenAI could see it and scoop you out of who knows how much value.
There is an old story attached to many historical figures that goes:
If this accusation is true, which I'm not completely confident about, but if it is true, that is the situation we would be in... we would have established that OpenAI is willing to steal from its customers, the only question is where the line is now, and where the line might be in the future.Honestly the human drama, while the compelling story, is in monetary terms orders of magnitude less important than the question of whether OpenAI has a mechanism to steal ideas from its customers. Has this happened before and they just successfully covered it up? Or maybe the people stolen from thought it was innocent and just a coincidence that they were scooped? If it established that there is a price, I have a lot of questions about that price.
How ironic that academic institutions, that became outrageously expensive on purpose, are now complaining that academic research is too expensive. This is coming from universities with already incredible endowments. They made science pay-to-play but now don't like that their own rules are being applied to them. Maybe instead of giving money as a bribe to get your kid into a good college, you can give the college some GPU's?
[dupe] Discussions:
https://news.ycombinator.com/item?id=49613262
https://news.ycombinator.com/item?id=49605915
This article reads like it was written by someone who has done less research than the average HN poster. Not a single word of OpenAI threatening people or apologizing for threatening people.
[dead]
[dead]
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.
LLMs pattern match based on the prompt. Go ask for medical with my tummy hurts and patient presents with intestinal cramps and see how asking a question as an expert changes the interaction
Go win a Millenium prize then.
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.
>what the world-class 2 mathematicians did was sat down and started working on their proof for over a year
If they were not related to anthropic I'd probably agree with you. OpenAI is much more for science than they are imo. Anthropic culture is all about "machine go brrrr" more than all of the other labs. If they had access to better models they'd probably would've one-shotted the solution. When the creator of bun was just "vibe-sciencing" it was ok. There is little to no evidence that they've been working using AI in this problem for over a year. Maybe they've been working on the problem for decades. So many other scientist have. Are they better because they threw a prompt and let it go brr??
When we put this in the perspective of how agents are changing the landscape of math/science, true it is shitty and weird. When folks are saying these scientists by anthropic that vibe-science'd the solution are victims, just because they did it with a smaller model, it is not defensible imo. And credit loses meaning here. The credit is shared with all the scientists that contributed somehow with the data in the AI pre-pos/training and not the prompter.
> If they were not related to anthropic I'd probably agree with you.
What does the company they work for (only 1 of them, mind you) have anything to do with the topic at hand? They were using both Anthropic & OAI models during their research, and they were doing it separate to their work as independent researchers rather than as employees of any specific company. In fact, this makes OAIs actions even worse because they tried a bribe in order to slice the Anthropic employee out of the deal.
[dead]
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.
They didn't write a traditional proof, but a lean program, which can be used to validate proofs formally, using a computer. It's still up to humans to check wether the formalization is sensible, but the proof is correct.
Has Lean itself been proved?
I think pretty much every major mathematician has accepted that the ideas and implementation behind lean is solid.