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

Navier-Stokes Announcement

claymath.org

Post reply on HN
Print view View original

141–150 of 292 posts

Re: Navier-Stokes Announcement

#141

Post by fasterik »

IshKebab wrote: post #134
KeplerBoy wrote: post #117

Earlier quoted context omitted.

It's not a large prize though. OpenAI spent many multiples of the prize money in just a few days to get there and even if one solves a problem in the traditional way, that person is most likely already an accomplished professor at a reputable university where a million dollars doesn't mean as much as the eternal fame that comes with it.

It's definitely not a large prize for OpenAI, but actually IIRC they only spend a few hundred thousand dollars. It is a large prize if you're just an academic.

OpenAI said that at public API prices, the agents they ran would have cost $15M. I don't know what their internal pricing is, but it almost certainly cost more than $1M.

Re: Navier-Stokes Announcement

#142

Post by [deleted] »

adastra22 wrote: post #31
auggierose wrote: post #11

Earlier quoted context omitted.

The Lean proof is published, you can download it. The clock definitely is ticking. Edit: Oh, didn't see the "qualifying outlet" condition. But Poincare was ever just put on arXiv, so arXiv must count as well.

Publish in academic language means accepted peer-reviewed paper.

[deleted]

Re: Navier-Stokes Announcement

#144

Post by JumpCrisscross »

Panzer04 wrote: post #139
Tanjreeve wrote: post #124

Earlier quoted context omitted.

I present to you my new theorem as follows: If 1 == 3 then 3 == 3 ---- This statement is 100% logically coherent internally. But it also doesn't matter because we know that 1 does not equal 3 so this proof is completely pointless. I could also say 3 == 5 and it would still be logically sound but completely useless information.

For a laymen, I don't follow this. Are you proving for some arbitrary definition of == that isn't what we commonly consider the definition? How is it logically coherent? You mean only in the sense that you say it is and you haven't provided any rules to disprove it?

> How is it logically coherent?

It's not. But Lean doesn't interrogate logical coherence, just internal consistency.

Re: Navier-Stokes Announcement

#145

Post by joedwin »

drexlspivey wrote: post #19
unknown-unknown wrote: post #9

In my opinion, I think the Clay Mathematics Institute deserves some criticism for all the drama surrounding these problems. Mathematicians know that you can make problems arbitrarily complex, and declaring problems with large prizes attached to them can lead to a lot of competition and drama. I feel that mathematics should be free from competitions and the pursuit of glory. However, after reading the open letter sign…

> In my opinion, I think the Clay Mathematics Institute deserves some criticism for all the drama surrounding these problems. Mathematicians know that you can make problems arbitrarily complex, and declaring problems with large prizes attached to them can lead to a lot of competition and drama. I feel that mathematics should be free from competitions and the pursuit of glory. Currently 0/2 Millenium problem solvers c…

Money is target but this millenium price is not enough for them.

Openai is bringing machine gun to competition that used only knife and pistol.

Re: Navier-Stokes Announcement

#146

Post by HarHarVeryFunny »

Marchant_hq wrote: post #137

The two-year publication rule is the interesting part. OpenAI doesn't need the million, and the community will judge the result regardless of whether Clay ever accepts it.

The result was never the point.

Clearly the real-world cannot "blow-up" - real-world water vortices do not reach infinite velocity, etc.

The point of having Navier-Stokes as a Millennium prize was to hopefully generate new mathematics and techniques along the way, and auto-generating a sprawling AI-slop proof or millions of lines of Lean does not accomplish that result.

Clearly OpenAI has no interest in the math itself - to them this was just a trophy animal to shoot and stuff. I would be very surprised if they now helped analyze the proof and try to extract the mathematical value out of it, and this would obviously require outside help who are probably not inclined to help OpenAI math-wash their behavior.

Re: Navier-Stokes Announcement

#147

Post by NewsaHackO »

Panzer04 wrote: post #139
Tanjreeve wrote: post #124

Earlier quoted context omitted.

I present to you my new theorem as follows: If 1 == 3 then 3 == 3 ---- This statement is 100% logically coherent internally. But it also doesn't matter because we know that 1 does not equal 3 so this proof is completely pointless. I could also say 3 == 5 and it would still be logically sound but completely useless information.

For a laymen, I don't follow this. Are you proving for some arbitrary definition of == that isn't what we commonly consider the definition? How is it logically coherent? You mean only in the sense that you say it is and you haven't provided any rules to disprove it?

No the definition of == is the regular definition; it's just a deductive reasoning statement. Since the first part of the statement is never true, it doesn't matter what the second part of it says. Of course, like he said, that makes the statement have no value.

Re: Navier-Stokes Announcement

#148

Post by HarHarVeryFunny »

tristanj wrote: post #116
crowfunder wrote: post #107

Earlier quoted context omitted.

https://xkcd.com/605/

Relevant, but it's already rumored that OpenAI and Anthropic have made very significant progress on two more Millennium Prize problems. They're in a race to solve the next problem. OpenAI needs to solve another to shut down the (baseless) plagiarism allegations. Anthropic wants blood because OpenAI sniped the last one from one of Anthropic's researchers. It's a matter of pride for both companies. More results will co…

Given that the math community (incl. those 25 Fields medalists) has come out strongly against this trophy hunting of their unsolved problems, to the detriment of mathematics, I don't think these companies are going to be getting positive press if they ignore this plea and continue with this, nor is this going to help turn public sentiment pro-AI.

Presumably the people that OpenAI and Anthropic are trying to impress with these trophy kills are potential IPO investors, but I would have thought investors would also be concerned about the growing public backlash against AI.

Re: Navier-Stokes Announcement

#149

Post by tristanj »

atakan_gurkan wrote: post #140
tristanj wrote: post #121

Earlier quoted context omitted.

1) OpenAI and Buckmaster did not solve the same problem. Per https://x.com/IlinVasily29521/status/2097554700321329393 , here is a breakdown of who solved what. Tristan + Levent: 3D incompressible Euler with forcing OpenAI: 3D incompressible Euler without forcing OpenAI: Navier-Stokes with forcing No one: Navier-Stokes without forcing Euler equations = Navier-Stokes without viscosity. Forcing means external force. Abs…

For your point 2. It is of course possible, but it is highly unlikely if I understood Buckmaster's statements correctly.

Not when you have 10,000 concurrent agents attacking the problem. OpenAI brute-forced their way to a solution. They likely tried every approach in published literature, which includes the 2023 approach by Luis and Diego.

Re: Navier-Stokes Announcement

#150

Post by fasterik »

auggierose wrote: post #11
Legend2440 wrote: post #7

Their rules PDF says they won't accept any solution until at least two years after publication in a qualifying outlet. This allows time for the mathematical community to review and accept new results. As the OpenAI proof hasn't been officially published yet, the clock hasn't started ticking.

The Lean proof is published, you can download it. The clock definitely is ticking. Edit: Oh, didn't see the "qualifying outlet" condition. But Poincare was ever just put on arXiv, so arXiv must count as well.

I think the rules technically exclude the arXiv as a qualifying outlet.

Without limiting any other provision in this Section, a publication lacking any of the following characteristics will be deemed not to be a Qualifying Outlet:

i. an editorial board whose members are named and available for contact;

ii. an editor or editorial board member whose professional knowledge of the global mathematics community would enable him or her to identify an appropriate referee to review a submitted paper;

iii. a published refereeing process that, in the opinion of CMI, ensures that a submitted paper is reviewed and verified by appropriate experts in the field of the Problem; or

iv. inclusion in the list of publications maintained by MathSciNet.

The solution to the Poincaré conjecture was only accepted after an exposition of Perelman's proof was published in a refereed journal. His papers didn't qualify, but of course he got the credit for the result.

Post reply on HN