Maybe a naive question, but how does one know that a particular lean proof is actually a proof of what one thinks? Like, ok the logic checks out and it proves something , but there's still the problem of does this logical result actually prove the initial question that was asked?
On the Navier–Stokes Millennium Prize Problem
251–260 of 1001 posts
Re: On the Navier–Stokes Millennium Prize Problem
#252Earlier quoted context omitted.
No, its a pure outrage. I defended OpenAI til today. I now affirm they must be totally destroyed, burned utterly to the ground.
Why the rage? Weather an individual or a company found the solution (stolen or not) they both used AI to come get the solution. We have AGI and the intelligence abundance is going to be amazing for everyone in the future.
Why? These 'geniuses in a datacenter' aren't good, they aren't 'aligned', they don't work for you. They'll take your job, then they'll hack your computer, and then who knows what's next.
Re: On the Navier–Stokes Millennium Prize Problem
#253Earlier quoted context omitted.
Why can't they rule it out? Is even OpenAI unable to track the provenance of all of their training data? This is one of the major problems with these enormous closed models, and even most open-weights models, which don't disclose their training process or training data. You can never be sure what went into its training. Did it come up with an idea originally, or is it just plagiarising its training data? Are there ma…
To truly prove some incidental usage data made no difference we'd have to (a) identify any of their de-identified data that came from their usage of ChatGPT, (b) train a bunch of expensive giant models, and (c) ask them all to solve the Navier-Stokes Millenium problem until hitting some level of statistical significance. It's just not feasible to run experiments like this to prove whether a piece of data has an effec…
Re: On the Navier–Stokes Millennium Prize Problem
#254Is this the one that was allegedly based on someone else's actual work & prompts? https://news.ycombinator.com/item?id=49605915 https://bsky.app/profile/quantian.bsky.social/post/3muyhwbcd... https://cims.nyu.edu/~tristanb/statement.pdf
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…
The question I am interested in is not "did we read private chats", but "was this new model trained using any of Tristan and Levent's chats, regardless of whether they were marked private". Can you comment on that?
Re: On the Navier–Stokes Millennium Prize Problem
#255Earlier quoted context omitted.
What else can they declare really? Yeah the model has training data from previous attempts. Alpöge and Buckmaster also similarly benefited from attempts before theirs.
They could have thought about the problem for like 2 minutes and not done this! I think that literally any academic mathematician could have explained to them, had they asked, why it is considered extraordinarily rude to react to rumors of research progress by desperately rushing to get there first.
Re: On the Navier–Stokes Millennium Prize Problem
#256Maybe a naive question, but how does one know that a particular lean proof is actually a proof of what one thinks? Like, ok the logic checks out and it proves something , but there's still the problem of does this logical result actually prove the initial question that was asked?
What else could a theorem prove if not its own statement? (barring bugs in Lean, which have been detected and exploited)
Re: On the Navier–Stokes Millennium Prize Problem
#257This really leaves a bitter taste.... "On Tuesday, September 1, we heard rumors that two Millennium Prize problems had been resolved. Inspired by these rumors and by the step change in performance of our internal model, we launched an effort to evaluate it on all open Millennium Prize problems and a few other high-impact problems." IPO+rumour driven research. I appreciate the achievement, but it doesn't feel right.
Re: On the Navier–Stokes Millennium Prize Problem
#258Re: On the Navier–Stokes Millennium Prize Problem
#259Re: On the Navier–Stokes Millennium Prize Problem
#260the context here is super important, for those who haven't seen it yet. OAI maybe just trained on a real researchers solution and then celebrated having scored the goal unassisted save for the brief commentary at the bottom of this blog post. Here's the other side. https://x.com/rynorhn/status/2097223532438487463