4 ms·
I'm not sure it actually makes a difference. OpenAI doesn't care about the million dollars in any case. And the judgement that they did it is independent of w
by eru 1mo ago
I'm not sure it actually makes a difference. OpenAI doesn't care about the million dollars in any case. And the judgement that they did it is independent of whether the Clay people agree: you can make up your own mind and so can everyone else.
Though it would be funny if no one ever bothers publishing the result in an appropriate journal, and thus the prize technically can never be claimed.
- c7b 1mo agoEven funnier that it wouldn't even be the first time that happens: https://en.wikipedia.org/wiki/Grigori_Perelman https://en.wikipedia.org/wiki/Grigori_Perelman
- thrance 1mo agoAnd he also gave up his trophy, which is displayed in a random corridor of a random math museum in Paris, where visitors pass by without looking, lacking most, if not all, of the context. Only because I knew the story and the man did I recognize the object for what it was.
- peacefullmind 1mo agowhere is it displayed , in which museum ? As a mathematician it would be cool to visit it, but I can't find anything on google.
- yen223 1mo agoIt's very likely that no one will claim any of the cash prizes, which is funny to me
- jgalt212 1mo agoNot including salaries, OpenAI spend $20MM to make $1MM. Very on-brand for a start-up.
- jacobrussell 1mo agoI don’t think solving a millennium prize problem can be reduced to some DoorDash economics of “spent Y to make X.” What if it took someone their entire professional career to solve one of these problems, would it not be worth it by the same logic?
- jgalt212 1mo agoOf course, you're right. I was making social commentary / joke.
- program_whiz 1mo agoSurprisingly this is actually rather fitting in terms of time scale. When you consider it took ~10,000 agents 88 hours, or 880,000 hours to solve. That's 14.5 years in agent time of continuous 365/24/7 processing. Of course, humans solve things much more efficiently (and didn't also need the massive pre-training of every expert on the planet for 1,000,000,000 human years equivalent). But yeah, human researchers can solve a problem like this in a decade or so, while sleeping, teaching, traveling, and taking breaks, only working a few hours a day on the idea.
- nomel 1mo agoHow many people have worked on this problem? How many have failed? How many hours total?
- taneq 1mo ago> But yeah, human researchers can solve a problem like this in a decade or so None of them did, though, despite how many tried. So empirically, it seems unreasonable to say human researchers can solve ‘problems like this’.
- soperj 1mo agoHe did it because he had principals. OpenAI the opposite.
- MarkusQ 1mo agoMore likely it's because a million dollars one way or the other won't make a difference in the hole they are digging / mountain they are building.
- pwdisswordfishq 1mo agoHe had principals, while OpenAI had agents?
- znnajdla 1mo agoIt does make a difference because the only reason OpenAI cares about these problems in particular versus any other random problem in math is because of the prestige associated with official recognition, not just claiming something as marketing.
- eru 1mo agoMaybe. But the prestige requires that the Clay people have offered the prize money, it doesn't require that OpenAI claims the prize money.
- Aissen 1mo ago> And the judgement that they did it is independent of whether the Clay people agree: you can make up your own mind and so can everyone else. No I cannot, and I'd argue most people can't either. We rely on mathematicians, peer review, and letting the scientific process run its course.
- soerxpso 1mo agoIt's formalized in Lean, isn't it? Do you also rely on a community of C++ experts to tell you whether a program compiles or not?
- tired-turtle 1mo ago"Beware of bugs in the above code; I have only proved it correct, not tried it." — Knuth, 1977
- mpardalos 1mo agoYes, but there's still the possibility that it's either exploiting a bug in Lean, or that the theorem statement is not set up correctly (i.e. it's actually proved a different theorem). My understanding is that the theorem statement is quite simple, so i guess the latter is not very likely, but the former is very much a possibility in a proof this large, and it will take some human eyeballs to go over it before convincing mathematicians.
- rawland 1mo agoI ran the proof 3 days ago. They do a Comparator Challenge to validate that they actually solved the correct theorem from the result, which they copied from Google/DeepMind: https://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b38b6e212696e8a30e3e91517af887bbd/ComparatorChallenges/NavierStokes.lean#L26 https://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b... - this is valid for both Euler and NS. Also, they validated with an external kernel from the Lean Kernel Arena. That way bugs in the Lean kernels were found in the past already, iirc. Having said that, I strongly believe a positive result with the challenge above is the reason why they published it. I highly doubt anybody at OpenAI (or anywhere else) fully gets the proof after such a short time since publishing. This is also what Terry Tao criticized the most in my opinion. Independent of the remaining drama [0], from my point of view, the proof is correct and an achievement. [0]: https://news.ycombinator.com/item?id=49661928 https://news.ycombinator.com/item?id=49661928 - I am pretty much on the critical side, however, one can not ignore that it is an achievement. Esp. the unforced result.
- jacquesm 1mo agoWhy would that be funny? Years of people's work appropriated and they end up without even the recognition? I'd be furious.