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

841–850 of 1001 posts

Re: On the Navier–Stokes Millennium Prize Problem

#841

Post by aeve890 »

masterspy7 wrote: post #762
aeve890 wrote: post #700

Earlier 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.

Do you even know what a proof entails? This shit is not a proof, come on.

Re: On the Navier–Stokes Millennium Prize Problem

#842

Post by Jblx2 »

professoretc wrote: post #538
rfgplk wrote: post #138

Earlier quoted context omitted.

Skill issue. Also lean is meant to be executed, not read.

A proof is not like a program. The goal of a program is to "do the thing", thus you can make the argument that it doesn't matter what the code looks like as long as its works right. But the goal of a proof isn't to "do the thing" (where "the thing" is just to print Yes or No), it's to communicate . An unintelligible proof is really just a first draft.

>A proof is not like a program.

https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

Re: On the Navier–Stokes Millennium Prize Problem

#843

Post by frabcus »

derangedHorse wrote: post #768
pred_ wrote: post #151

Earlier quoted context omitted.

> we did not read any private chats Your post says “While unlikely, we cannot rule out that de-identified data derived from their usage of our products helped improve our models .” We can discuss what it means to “read” things but obviously the issue here isn't whether you did it manually or automatically. But more importantly, what on earth are you doing threatening real scientists to remove their coauthors, then ma…

Except that’s not what happened. OpenAI offered to collaborate and put conditions on their offer. They aren’t threatening the removal of a coauthor for an independent work.

The condition was ludicrous, and for political reasons, because one of the authors was also an Anthropic employee.

It's completely childish, and not befitting of the weight of the times we're living in.

Re: On the Navier–Stokes Millennium Prize Problem

#845

Post by senshan »

nozzlegear wrote: post #658
onidj wrote: post #312

Earlier quoted context omitted.

>- Do "normies" even know what's happening? Absolutely not. Even to a lot of techy/nerdy people it's still just a chatbot that they sometimes use to help them at work. Even on here people will do whatever they can to downplay. The lack of fucks given is staggering.

How many fucks should be given, in your estimation?

∀ε>0, ∀x: ‖s−x‖ 1/ε

Re: On the Navier–Stokes Millennium Prize Problem

#846

Post by angry_octet »

hellohello2 wrote: post #814
traes wrote: post #545

Earlier quoted context omitted.

Which seems to be entirely true by their own admission! [0] Both the comments about him risking his career and about Levent's authorship seem to have indeed occurred. > 2) I never ever asked for Levent to be removed from authorship of his own work (as indicated by my text). I was surprised to learn during the call with Tristan that they had only solved Euler and not Navier-Stokes; after learning this we brainstormed…

Hm. Looks like its possible everyone behaved terribly here unfortunately. :/ I remained impressed by ChatGPT however!

Everyone?? No, most definitely OpenAI.

But they have learnt their lesson, next time they won't reach out to who they stole it from, they will publish first.

Re: On the Navier–Stokes Millennium Prize Problem

#847

Post by Jblx2 »

aizk wrote: post #413
frotaur wrote: post #185

Earlier quoted context omitted.

The point of lean proofs (as it stands) is simply one bit of information: that a given mathematical statement is indeed true. It's a way to be absolutely certain (modulo bugs in the lean kernel) that a proof you came up for a statement is indeed correct. It is really not meant to be analyzed, much less now that they are fully llm written.

Well, how do we know there aren't errors in their construction within the lean code? Does it just "not compile" or something, or is it deeper / more fundemental than that.

https://ammkrn.github.io/type_checking_in_lean4/trust/trust....

Re: On the Navier–Stokes Millennium Prize Problem

#848

Post by FallCheeta7373 »

samrus wrote: post #834
piloto_ciego wrote: post #819

Earlier quoted context omitted.

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.

You have to look at the incentives

Incentives are one thing, even adjusting for them it's huge, and I don't understand this incentive play for only openai, academics have perverse incentives too, to overreport, overclaim, publication bias etc why are we scrutinizing AI industry to such high degree when they have demonstrated capability and often times are off by a model release at worst.

Re: On the Navier–Stokes Millennium Prize Problem

#849

Post by topaz0 »

pama wrote: post #183
arctic-true wrote: post #35

Buried under the drama is the fact that OpenAI is claiming that an internal model they’ve been training for less than two weeks is more than twice as capable in mathematics as Astra, which was only made public a week ago. Even if this improvement is limited to mathematics, that is an astounding feat.

Not only that, but it used 10k agents coherently over 88 hours to come up with the proof. This is a significant advance.

What makes you think they were coherent?

Re: On the Navier–Stokes Millennium Prize Problem

#850

Post by [deleted] »

hollowcelery wrote: post #839
hansvm wrote: post #740

Earlier quoted context omitted.

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…

But the researchers also did their research using essentially the same models, so that isn’t a counterpoint to AI models being at the far frontier…

[deleted]
Post reply on HN