7 ms·

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 resul

by rsfern 8d ago

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

chermi 8d ago
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..
SwtCyber 7d ago
[dead]
rakejake 8d ago
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.
- chermi 8d ago
  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.
- dcre 8d ago
  Worth noting they claim they did not choose the line of attack. Of course we don’t know whether that is true.
  - freejazz 7d ago
    Yeah, they didn't choose the line of attack, the person they copied it from did..
  - rakejake 8d ago
    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.
- cmiles8 8d ago
  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.
harhargange 8d ago
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.
- vonneumannstan 8d ago
  Theres a reason those same mathematicians did not solve the problem on their own. Minimizing the impact the model made here seems unjustified.
- nayroclade 8d ago
  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 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.
  - 8d ago
sigmar 8d ago
>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?
- tantalor 8d ago
  It might but the math results from GenAI so far have been limited to finding counterexamples to known conjectures, not building new mathematics.
  - cma 7d ago
    > 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
    - tantalor 7d ago
      True, these results are from last month. My info was a little out of date. Prior updated :)
- rsfern 8d ago
  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
u1hcw9nx 8d ago
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.
- SwtCyber 7d ago
  [dead]
- robotpepi 8d ago
  you're as sure of what you say as wrong about it.
  - jgalt212 8d ago
    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.
  - Toutouxc 8d ago
    Note that your reply has exactly 0 value for anyone who doesn’t already know where and how the parent poster is wrong.
    - robotpepi 8d ago
      fair enough
  - hyperbovine 8d ago
    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.
    - robotpepi 8d ago
      I was referring to the "it's just mathematicians checking boxes" claim
jhrmnn 8d ago
Working with AI on science (not LLMs though), couldn't agree more.
jgalt212 8d ago
> 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.
- rsfern 8d ago
  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
fxj 8d ago
[dead]
alansaber 8d ago
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.
_zoltan_ 8d ago
> 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).
00ze 8d ago
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.
- eieje1 8d ago
  [dead]

by rsfern 8d ago

chermi 8d ago

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..

SwtCyber 7d ago

[dead]

rakejake 8d ago

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.

chermi 8d ago
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.
dcre 8d ago
Worth noting they claim they did not choose the line of attack. Of course we don’t know whether that is true.
- freejazz 7d ago
  Yeah, they didn't choose the line of attack, the person they copied it from did..
- rakejake 8d ago
  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.
cmiles8 8d ago
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.

harhargange 8d ago

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.

vonneumannstan 8d ago
Theres a reason those same mathematicians did not solve the problem on their own. Minimizing the impact the model made here seems unjustified.
nayroclade 8d ago
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 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.
- 8d ago

sigmar 8d ago

>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?

tantalor 8d ago
It might but the math results from GenAI so far have been limited to finding counterexamples to known conjectures, not building new mathematics.
- cma 7d ago
  > 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
  - tantalor 7d ago
    True, these results are from last month. My info was a little out of date. Prior updated :)
rsfern 8d ago
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

u1hcw9nx 8d ago

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.

SwtCyber 7d ago
[dead]
robotpepi 8d ago
you're as sure of what you say as wrong about it.
- jgalt212 8d ago
  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.
- Toutouxc 8d ago
  Note that your reply has exactly 0 value for anyone who doesn’t already know where and how the parent poster is wrong.
  - robotpepi 8d ago
    fair enough
- hyperbovine 8d ago
  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.
  - robotpepi 8d ago
    I was referring to the "it's just mathematicians checking boxes" claim

jhrmnn 8d ago

Working with AI on science (not LLMs though), couldn't agree more.

jgalt212 8d ago

> 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.

rsfern 8d ago
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

fxj 8d ago

[dead]

alansaber 8d ago

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.

_zoltan_ 8d ago

> 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).

00ze 8d ago

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.

eieje1 8d ago
[dead]