I've been working on this problem for what seems like for ever. Kudos to the OpenAI team. For those of you who don't care about the drama and want to see this distilled to 3 lines: https://x.com/nadermx/status/2097414953225310280
Any version with a bit more prose for a peasant like me to remotely pretend to grasp it
On the Navier–Stokes Millennium Prize Problem
991–1000 of 1001 posts
Re: On the Navier–Stokes Millennium Prize Problem
#992Earlier quoted context omitted.
Why is it unlikely?
Because the models are trained on hundreds of billions of user conversations, across more than a billion different humans. The conversations are anonymized and not easily traceable back to a specific user. It's unknowable and not possible to prove if any one specific conversation contained the insights for solving Navier–Stokes. We also don't know if the authors unintentionally provided data to OpenAI through alterna…
Re: On the Navier–Stokes Millennium Prize Problem
#993Earlier quoted context omitted.
Yes, that was the allegation last night. I work at OpenAI, though not on the team that did this, and my understanding is: - we decided to ask our model for Millenium problem solutions because of two reasons: (a) our new model was looking incredibly good and (b) we heard rumors that some Millenium problems had been solved and were curious if our models could solve them (the goal here was not to scoop any particular in…
Some millennium problems? Are there more coming?
Re: On the Navier–Stokes Millennium Prize Problem
#994Earlier quoted context omitted.
> We don't have any proof of that It’s fair to give benefit of doubt to Buckmaster given OpenAI is currently being very credibly sued by Apple for openly stealing others’ original work in another context.
A prior of "one large company is current involved in an unrelated lawsuit with another large company" is pretty weak; the case is undecided and about an entirely different kind of IP theft. In short I think a lot of people are jumping to conclusions without supporting evidence and that's really not helping the situation.
The guy mocked accessing his prior employer's circuit diagrams and was protected by OpenAI until Apple filed suit.
Tabula rasa, sure, we need more evidence. But ignoring the priors should at least be explicitly acknowledged.
Re: On the Navier–Stokes Millennium Prize Problem
#995Earlier quoted context omitted.
I worked at OpenAI previously, but don't know any of the people involved in this. My guess was it was probably this was more a nerd snipe than any action from OpenAI that was a "massive team" being put on it. Literally someone looking at this and asking "I wonder if our models are good enough yet". It's easy to assume that having access to massive compute amounts means significant coordination, but this assumes that…
They said that a customer would have paid around 15 million for the required compute. I can't imagine that this was not a significant internal spending even with "free" tokens.
If you consider this as a cost to be compared against the question: "What does it take to be able to prove that you have a model that can solve the hardest problems that humans know about?", then spending a some amount of thousands/millions to know the boundaries of that seems not too important in comparison.
You've also got to consider this as compute that's allocated to pushing the frontier of what models can do, so while it's using GPUs that have been paid for etc., it's not like it's a cost that's supposed to be use less of this so that others can have capacity. If you made researchers afraid to use capacity like this, a lot of the things that improve would tend to do so significantly slower. (some may say that's a good thing ;)
A good way to think about this is when tokens are free, you get to choose whether you're optimizing for latency or intelligence rather than having to consider price.
---
Publically, tibo (Codex owner) in Feb this year: https://x.com/thsottiaux/status/2024649339344445825
> OpenAI employees currently get unlimited inference. Usage is now peaking at > XX billion tokens per week for some of them.
Mathew Berman (AI Youtuber) in Jun: https://x.com/MatthewBerman/status/2067270730795134984
> I've used 25 billion tokens in the last 7 days.
Re: On the Navier–Stokes Millennium Prize Problem
#996Earlier quoted context omitted.
They managed to solve a problem that was beyond current human ability.
That was the net effect (assuming what they solved was the actual problem and not a loophole in the problem statement or a lean bug). My point is they need not all work coherently to do that -- for example, for all we know 3/4 of them went off the rails, their results were pruned, and the relevant results came from a random subset that happened to produce something useful.
I am not an expert in lean4, but I could follow parts of the high level lean definitions of the problem statement in the repo. A lean bug would be a fun scenario; I am certain this proof will receive the deserved scrutiny, and if it uncovers a bug, it will make the story even more exciting. It is extremely unlikely to be the case, however, because the 10k agents working on the proof didnt use lean, so it would have to be a math logic error that translates to a lean bug—perhaps something the agents picked up during training?
Re: On the Navier–Stokes Millennium Prize Problem
#997Earlier quoted context omitted.
Not only that, but it used 10k agents coherently over 88 hours to come up with the proof. This is a significant advance.
If you can create a graph of independent work, which you can with many such problems, agents can work together nicely. Again, thank Lean and the tooling around it.
Re: On the Navier–Stokes Millennium Prize Problem
#998Earlier quoted context omitted.
Not only that, but it used 10k agents coherently over 88 hours to come up with the proof. This is a significant advance.
With 10,000 agents and $20M of compute this is just brute force search. It's a bit like telling 10,000 kids there's an easter egg hidden over there, pointing to one corner of your yard (or having "heard a rumor" it was hidden in that corner). If you have $20M to spend on your problem, then yes, AI brute force search is an option, but unless you know a solution is possible (as OpenAI did here), you may still be wastin…
To me it feels closer to taking the top 10k human mathematicians on a large retreat for a year and having them self organize to collectively solve this problem—not kids and easter eggs.
Re: On the Navier–Stokes Millennium Prize Problem
#999Earlier quoted context omitted.
It'd be corporate suicide for them to be caught violating zero-data-retention commitments. But also if you're really paranoid you can just use ChatGPT on Azure or AWS, where nothing is flowing back to OpenAI at all.
> It'd be corporate suicide for them to be caught violating zero-data-retention commitments Would it, though? Considering their entire business model is built on the agglomeration of data that isnt theirs.
The businesses API usage will disappear overnight if OpenAI doesn't honor its contracts with businesses.
Re: On the Navier–Stokes Millennium Prize Problem
#1000People had joked a couple years ago "Well if they solve a Millenium problem it's AGI"... Well here we are.
> I have a couple friends who did the Math tripos at Cambridge (so a pretty high level!) who work in tech and have unanimously said they have 0% expectations of an LLM doing a millennium problem anytime soon https://news.ycombinator.com/item?id=38433655 > Let's talk when we've got LLMs proving the Riemann Hypothesis (or any mathematical hypothesis) without any proofs in the training data. I'm confident in my belief t…