231–240 of 245 posts
Earlier quoted context omitted.
you're as sure of what you say as wrong about it.
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.
Earlier quoted context omitted.
you're as sure of what you say as wrong about it.
If that were true you could explain it. There are lots of solvers for navier stokes simulations and they do a good job.
> 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.
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.
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
Earlier 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…
Earlier quoted context omitted.
>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.
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
Earlier quoted context omitted.
>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…
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
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.
Earlier 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.
Worth noting they claim they did not choose the line of attack. Of course we don’t know whether that is true.
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.
> 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.
Earlier quoted context omitted.
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
Prior updated :)