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 bas…
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.
How An AI math breakthrough ignited a controversy
211–220 of 246 posts
Re: How An AI math breakthrough ignited a controversy
#212This 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 s…
You do realize that businesses that have contracts with them can specify if they want their data used for training or not right?
Re: How An AI math breakthrough ignited a controversy
#213Regardless 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 bas…
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 pr…
Re: How An AI math breakthrough ignited a controversy
#214Earlier quoted context omitted.
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 direct…
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…
Re: How An AI math breakthrough ignited a controversy
#215Earlier quoted context omitted.
If you read Buckmasters statement, he specifically notes that they used the paid subscriptions, iirc.
>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 h…
"I pay for the tools my group uses out of my own research funds, including footing a large bill to OpenAI."
Re: How An AI math breakthrough ignited a controversy
#216Earlier quoted context omitted.
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.
Re: How An AI math breakthrough ignited a controversy
#217Regardless 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 bas…
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..
Re: How An AI math breakthrough ignited a controversy
#218Regardless 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 bas…
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.
Re: How An AI math breakthrough ignited a controversy
#219Earlier quoted context omitted.
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.
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. O…
I guess I'm having trouble unraveling your experience and personal usage vs. what you're concluding about the labs.
Re: How An AI math breakthrough ignited a controversy
#220Earlier quoted context omitted.
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 charitabl…
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.