AI and Math Research

[Hornbein]

----
@hhh4804
(As a physicist) i don't know, it feels like a chess player solving a position using a chess engine... i think we are completely missing the meaning of scientific research, there is no point in solving math problems using AI
----

Me
Well it depends. Do you want to solve problems or do you enjoy the thrill of the chase?

As for me I worked in a tiny field that very few were seriously interested in. Over a couple of decades I solved everything I wanted to to my satisfaction. I wrote up the results in friendly form. That was all very nice but now I no longer have anything to ponder in my spare time so I'm bored. Did I win or did I lose?

In my case it was strictly amateur. Suppose I were funding research. Would I want results as quickly and cheaply as possible? Or is my goal to keep gentlemen in endless character-building struggle?

 

[jack action]

I thought this news fitted this thread:

Did AI Just Solve Navier-Stokes? What OpenAI's Claim Actually Proves

To work the problem, OpenAI used 10,000 parallel AI agents, 88 hours of compute, and roughly $22.5M in accumulated costs.

Here's where the fine print matters. The official Clay formulation for Navier-Stokes includes four options, labeled A, B, C, and D. Options A and B ask for global smooth solutions with no external forcing, in ordinary three-dimensional space or a periodic domain. Options C and D allow blow-up examples with a smooth external forcing term. OpenAI's proof targets options C and D, meaning the forced variant is genuinely part of the official Clay problem.

That said, many mathematicians consider options A and B to be the deeper question, because forcing is externally imposed: you're choosing the force to cause the blow-up, rather than asking whether the equations can break down on their own. Whether the approach can be extended to remove the forcing and address A and B is not yet clear, and that question is very much still open. The gap between what's been shown and what many experts consider the heart of the problem is the actual takeaway here.

[...] an independent researcher's year of unpublished work became the resource a well-funded lab ran a multi-million-dollar sprint around, [...]

If you aren't familiar with Lean, know it's a formal proof verification system that checks whether each logical step follows from the previous one. A Lean-verified proof can't be "talked into" looking correct: if it passes, the logical chain is sound. What Lean doesn't do is tell you whether the approach is conceptually meaningful, whether it addresses the problem as experts understand it, or whether a human mathematician would recognize it as a genuine solution.

Terence Tao, arguably the most prominent living mathematician, offered a warning about this dynamic on September 5th, before OpenAI's announcement. Writing on Mathstodon in response to rumors circulating at the time, he noted it was a hypothetical concern: "there is a substantial opportunity cost in converting a historically productive and motivating problem such as Navier-Stokes regularity into a mere viral social media post advertising some benchmark progress, rather than actually advancing the field and developing the next generation of both problems to ask, and people to work on them." After the announcement, Tao praised the Buckmaster-Alpöge work as "a remarkable achievement" and noted their arguments had been formalized in Lean. He hasn't publicly endorsed OpenAI's specific claimed proof.

Axios put the uncomfortable question plainly: what happens when the company providing scientists with AI research tools can also mobilize vastly more resources to compete with them? Buckmaster and Alpöge were using OpenAI's own Codex throughout their year of work. The tools a researcher uses to build toward a result can be owned by the same organization that can outpace them with those same tools at 10,000x scale. That's not a conspiracy. It's a structural feature of the current moment, and it's the scenario people have been worried about, independent of whether OpenAI did anything wrong here.

The sprint model produced a result. Whether it produced a result, in the sense mathematicians mean, is a different question, and one that'll take considerably more time to answer.

OpenAi's article: On the Navier–Stokes Millennium Prize Problem

 

[javisot]

I thought this news fitted this thread:

Did AI Just Solve Navier-Stokes? What OpenAI's Claim Actually Proves








OpenAi's article: On the Navier–Stokes Millennium Prize Problem

I am amazed at how long it has taken for this matter to be mentioned on PF. A Millennium problem, C-D, has been solved (or so it seems). We should have been talking about this since yesterday.

(I have been trying since yesterday to apply OpenAI's work to gain a deeper understanding of black hole jets)