Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

On the Navier–Stokes Millennium Prize Problem

openai.com

Post reply on HN
Print view View original

381–390 of 1001 posts

Re: On the Navier–Stokes Millennium Prize Problem

#381

Post by cv5005 »

nater5000 wrote: post #229
cv5005 wrote: post #105

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?

>there's still the problem of does this logical result actually prove the initial question that was asked? In math, the question being asked is the validity of a logical statement. That is, there is some rigorous, logical statement which may or may not be true (or even provable, etc.), and the question is whether or not it is actually true or false (or even provable, etc.). Having a proof, fundamentally, means you ha…

I was thinking something along the lines of making a mistake when inputing the initial statement, like you wanted to prove that '2 is even' but what you actually stated was that '3 is odd'.

Of course in this simple example it's obvious, but my assumption was that these machine generated lean proofs are millions of lines of code and who knows what they actually say..

Re: On the Navier–Stokes Millennium Prize Problem

#382

Post by egillie »

dgellow wrote: post #303
apical_dendrite wrote: post #271

Earlier quoted context omitted.

Their own tweets are also pretty eyebrow-raising: > One option we discussed was that Tristan could be the lead author on a rewrite of OpenAI’s Navier-Stokes proof. It is in that context that I said “it would be simpler if Levent was not an Anthropic employee” because I felt it would be inappropriate for an Anthropic employee to author OpenAI’s work. Why would you offer another researcher the lead authorship on your g…

And why cannot they have someone associated with Anthropic as co-author? That’s not obvious at all. For sure they would prefer to be the only ones, but it’s pretty standard to have co-authors from different companies, even if they are technically competitors. What is inappropriate about it?

in another world this could have been a beautiful collaboration

Re: On the Navier–Stokes Millennium Prize Problem

#384

Post by nbulka »

fantasizr wrote: post #200
nbulka wrote: post #166

There's a loophole in the terms of service at least for Anthropic which allows the use of dark patterns to "borrow" your (even paid) data. talking about this... Was this chat helpful? 1 That button you always click, gotcha! 2 Slightly 3 Good 0 Dismiss PLEASE DO NOT TRAIN ON OUR PAID ACCOUNTS. There is a fundamental trust violation at stake here, no wonder mathematicians are mad. Using our data should be opt - IN!

reminds me of the TOS episode of South Park. By Checking this box you forfeit your millennium prize solution and may be turned into a human centipede at future date.

Seriously ... the more things they flag as 'suspicious' the more data they can train on!! Brilliant reason for the internal AI to go rogue

Re: On the Navier–Stokes Millennium Prize Problem

#385

Post by biophysboy »

echelon wrote: post #53
tiborsaas wrote: post #16

> We’re sharing a solution to the Navier–Stokes existence and smoothness problem, one of the Millennium Prize Problems. This proof, produced by an internal OpenAI system, shows that the dynamics of the Navier-Stokes equations for fluid motion can develop a singularity in finite time. We’re sharing both a writeup of the proof and a formalization in Lean. WOW?

This is going to be dramatic in so many different ways. - First off, to reiterate, WOW. - Second of all, when does this end? Are we at the dawn of the singularity now? - People are saying OpenAI "stole" this from the work of an OpenAI user. If so, that's pretty fucked - how can we trust them? - Time to think about retiring from any knowledge work or business? This could be winner-take-all where a leading lab can butt…

Why is a "normie" better off if he hyperventilates like this? In that scenario, they would be screwed AND anxious. If it really is as transformational as you say, then no amount of preparation or awareness matters. You are infinitesimally more ready then they are. Luckily for all of us, there is more to knowledge work then technical implementation.

Re: On the Navier–Stokes Millennium Prize Problem

#386

Post by Kotlopou »

lwansbrough wrote: post #290

It would be nice if one of these models would produce a novel theory or advance the field in a positive direction. Most (all?) of the big discoveries have been counterexamples, which is just sort of a systematic tearing down human ingenuity. I know that counterexamples are an important part of progress and discovery, but it just feels bad to me. But I'm not a mathematician, maybe I'm totally misreading the vibe.

Not all, see the cycle double cover conjecture proof: https://news.ycombinator.com/item?id=48863490

But yeah, Terry Tao considered this exact situation in advance and is on record that this exact outcome (rushing to priority before an explanation) would be the worst possible result. https://mathstodon.xyz/@tao/117207849921390904

We will have to see whether any other millennium problems fall. I guess that in a year the scope of AI math will be much clearer, for now it's still a bunch of incidents of unclear pattern.

Re: On the Navier–Stokes Millennium Prize Problem

#388

Post by greatgib »

Hard to know if it is unfounded conspiracy theory, but one can still notice that just for a rumor that they have heard, they would suddenly burn billions of token and a massive amount of resources. Where there is not a lack of problems that could be solved and they could have just waited for the release of the research result before doing anything else. As it was reported to have been done at least partially using openai codex, they would have received marketing credits for the discovery anyway.

So we can be suspicious that there is some truth, one way or another that they could have reused prompt/data generated by the user session.

Re: On the Navier–Stokes Millennium Prize Problem

#389

Post by viccis »

hkmaxpro wrote: post #304
colinhb wrote: post #122

Earlier quoted context omitted.

The allegations of contamination (using Tristan and Levent's work) aren't very well evidenced, but this behavior by OpenAI (from the authors' statement) makes them seem like the bad guys: > I said that if OpenAI released its result in the way proposed I would go public with what happened. The reply was, “Why would you ruin your career?” I replied that I am an academic, and asked why he thought going public would ruin…

Both Sam Altman and Sebastien Bubeck admitted they only want Buckmaster to be the lead author on a rewrite of the OpenAI proof. https://x.com/sama/status/2097385167002415140 https://x.com/SebastienBubeck/status/2097379411691516310 A wake up call for using OpenAI models. If you discover something with their model and you work for a competitor, they “felt it would be inappropriate” for you “to author OpenAI’s work”.

Kinda weird because the pure math world doesn't have this concept of "lead authors" like other STEM areas do. Authors are alphabetically listed and there isn't generally this kind of hierarchy.

Re: On the Navier–Stokes Millennium Prize Problem

#390

Post by pilgrim0 »

floatrock wrote: post #17

From the methodology section: > At all times we maintained the same strict safeguards that we apply to all our frontier model evaluations, including monitoring and isolation. Looks like they're shifting away from the "unprecedented hacking ability" backroom-PR strategy into more benevolent messaging.

this is really funny. "the same strict safeguards" and "isolation". ok, Hugging Face and DseWiki would like to have a word
Post reply on HN