Earlier quoted context omitted.
With Lean, math has become a really well suited problem for LLMs. We will likely see large gains for many years from here, just doing more and more rlvr, like continuously, non stop. No need to train from scratch. It really doesn't speak to the general intelligence of models though. It does speak to how good these things can become when a problem space has verifiable rewards, especially when you can verify one step a…
It's crazy how deep Microsoft's bench is (Lean was started there, vscode is another), for everything not directly related to the the ai models (hell, even github for data). So interesting how everything played out, I remember in the early days when MS came out with the partnership with OpenAI it seemed like they were playing 5d chess and were poised to win big. And it all just fizzled out. Second biggest fumble after…
On the Navier–Stokes Millennium Prize Problem
831–840 of 1001 posts
Re: On the Navier–Stokes Millennium Prize Problem
#832Earlier quoted context omitted.
> WOW This. I do dislike the AI oligarchs as much as the next person, but I do find the thread full of complaining a bit depressing still. If the result holds (and it looks it does), this may be one of the, if not the, biggest things to happen in computing to date. A lot bigger than e.g. Deep Blue beating Kasparov in chess or AlphaGo beating Sedol in Go.
Seeing mathematicians such as Terry Tao being unhappy with open problems being solved makes me sort of question the usefulness of any of this pure mathematics. If we're not happy that the problems are being solved, why care about this field at all?
Why would you go out of your way to make a case of something being not useful when, ironically, so much advancement in human history has come from the discipline?
Your motive is more worrying than your straw man argument.
Re: On the Navier–Stokes Millennium Prize Problem
#833Earlier quoted context omitted.
Recursive self improvement of their upcoming IPO value maybe. They are fluffy PR pieces otherwise.
How can you possible say this sort of thing in context of what looks like a millenium prize being solved. I swear there's nobody blinder than those who won't see.
Re: On the Navier–Stokes Millennium Prize Problem
#834Earlier quoted context omitted.
Also possible: we're 99.999% sure, but a lawyer said to be safe and strictly accurate, we should stick in a sentence in saying we can't be perfectly sure, since it's infeasible for us to prove it. I promise you that if we took their work from ChatGPT and stuck in a bunch of weasel words to give the opposite impression while remaining technically true, I would quit on the spot. (I work at OpenAI.)
Nice damage control bud, too bad the veil's lifting and everyone's seeing what you sociopaths at OpenAI are really like
Re: On the Navier–Stokes Millennium Prize Problem
#835I think this is clear evidence that AI models are now at the far frontier of mathematics innovation and discovery and exceed human limits. This specific problem having had a $1 million bounty on its head and still remaining unsolved for 26 years after the bounty was placed is pretty clear evidence that many of the world's best human mathematicians would have solved this problem if they could have, and none were able…
Not a counterpoint per se, but I burned $50k recently on a much more modest math problem (result already known, just thought I had a sketch of a more interesting proof), and the LLM thought it had proved it within those bounds but had instead subtly fucked up the Lean definition. Take from that what you will. Not to mention, it's still very much up in the air whether the model derived the answer of its own accord or…
Re: On the Navier–Stokes Millennium Prize Problem
#836My take: 1. It shows what even this wave of AI can actually do. 2. I wish it were done by different folks, ideally under some kind of public control like NASA research or the NPR model. 3. Keep in mind: natural science is different. It's not always a matter of computation. Computer science folks often struggle with this -- but this virtual world here does not actually exist. Everything is physical, including informat…
I would argue the main reason AI labs have been focusing on programming is to unlock industrial scale automation, next logical step is to solve math as it's the key to unlock everything else. Once you hold the key for math, everything downstream fields become a matter of compute
Re: On the Navier–Stokes Millennium Prize Problem
#837Earlier quoted context omitted.
OpenAI's position: > We (the researchers and the agents) did not see any of their work through any means until they released it publicly — in particular, no specific user data was accessed in order to solve this problem. While unlikely, we cannot rule out that de-identified data derived from their usage of our products helped improve our models . However, our proofs differ significantly and even the precise results p…
Why is it unlikely?
Re: On the Navier–Stokes Millennium Prize Problem
#838I think this is clear evidence that AI models are now at the far frontier of mathematics innovation and discovery and exceed human limits. This specific problem having had a $1 million bounty on its head and still remaining unsolved for 26 years after the bounty was placed is pretty clear evidence that many of the world's best human mathematicians would have solved this problem if they could have, and none were able…
Not a counterpoint per se, but I burned $50k recently on a much more modest math problem (result already known, just thought I had a sketch of a more interesting proof), and the LLM thought it had proved it within those bounds but had instead subtly fucked up the Lean definition. Take from that what you will. Not to mention, it's still very much up in the air whether the model derived the answer of its own accord or…
Re: On the Navier–Stokes Millennium Prize Problem
#839Re: On the Navier–Stokes Millennium Prize Problem
#840Earlier quoted context omitted.
Parent comment is claiming creativity and genius beyond human experts, so why not ask for a fully unassisted AI novel result? Having access to the entire corpus of human knowledge, what else such amazing entity would require to solve a hard problem by its own? Any result of such kind from an AI alone would be enough to refute my argument, yet you don't present any. >Also there are proofs where the only human steering…
https://www.anthropic.com/research/riemann-zeta >Throughout this process, Jarred's input was mostly limited to sending Claude messages of encouragement (mostly variants of “keep going” or “believe in yourself”).2 This seems to have helped Claude overcome some initial skepticism that it could make meaningful progress.