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

51–60 of 292 posts

Re: Navier-Stokes Announcement

#51

Post by d0mine »

baby wrote: post #10
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.

It’s easy to verify the lean statement, you don’t need to read the proof. That is part of the breakthrough

> we use “malicious” to describe code that goes out of its way to trick or mislead the user, exploit bugs or compromise the system. This includes un-reviewed AI-generated proofs and programs.

It is interesting that AI-generated proofs are described as malicious by Lean docs unless reviewed.

Re: Navier-Stokes Announcement

#52

Post by asdfman123 »

mi_lk wrote: post #45
tristanj wrote: post #3

Smart move by them for waiting until the drama died down before making a completely neutral statement. The statement is so sterile they don't even mention who solved it. The word "OpenAI" doesn't appear at all.

I really like this style of writing for some reason. Not sure how to put it but it’s a rare combination of a vague post and confidence

"We're just happy it was solved"

Re: Navier-Stokes Announcement

#53

Post by zone411 »

seanhunter wrote: post #32
baby wrote: post #10

Earlier quoted context omitted.

It’s easy to verify the lean statement, you don’t need to read the proof. That is part of the breakthrough

You absolutely need to read the lean proof firstly to assess the correctness of the proposition it is proving (ie in this case that it is actually proving or otherwise the smoothness of navier-stokes in R^3 and not something else) and secondly to determine whether the proof is “honest” in the sense given here https://lean-lang.org/doc/reference/latest/ValidatingProofs/

Completely misleading.

This is all you need to read and understand for Anthropic's FLT formalization:

  import Mathlib
  import Theorems.Thm_fermat_last_theorem

  /-- Solution side: the same statement, binder for binder, proved by this tree's `fermat_last_theorem`. -/
  theorem FLT_for_comparator (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ) (ha : 0  fermat_last_theorem n hn a b c (Nat.pos_of_ne_zero ha) (Nat.pos_of_ne_zero hb) (Nat.pos_of_ne_zero hc)
The actual proof is 13 million lines of Lean.

Re: Navier-Stokes Announcement

#54

Post by auggierose »

d0mine wrote: post #48
auggierose wrote: post #37

Earlier quoted context omitted.

Accepted by whom? Peer-reviewed by whom? I guess these little questions are what this article is really about.

> “The ultimate decision as to whether a publication qualifies as a “Qualifying Outlet” shall reside in the sole and unfettered discretion of CMI.”

[flagged]

Re: Navier-Stokes Announcement

#55

Post by skayvr »

baby wrote: post #12

It feels like a nice post. It’s almost like we’re not supposed to celebrate the fact that mathematics is accelerating.

Wait, I thought the provenance of the proof is still disputed? There's a mathematician in NY saying he used OpenAI to develop his Navier-Stokes ideas. And OpenAI's proof is suspiciously similar.

At this point, how can we tell whether AI is improving or it's just reappropriating its users work? It's probably a bit of both. But still, thick milky.

Re: Navier-Stokes Announcement

#56

Post by user43928 »

kaffekaka wrote: post #34
gps372 wrote: post #33

Earlier quoted context omitted.

Agree! 'Problems' are getting solved and this needs to be celebrated. Wondering how this will discourage mathematicians at all, since now they have another tool to accelerate their research. Nothing is stopping them from using 'new technologies' or sticking a gun to their head to use the 'new technologies' either.

You mean that every mathematician can assign ten thousands Astra bots and 20 million dollars in compute to their thesis problems now?

In December 2024 o3 scored 87.5% on ARC-AGI-1 and cost $4560 per task.

DeepSeek V4 Flash 0731 scores 89% and costs $0.02 per task.

If we apply the same factor to the guesstimated API price of $20M for this problem, we arrive at $57.

Real cost is a fraction of the API price. Although the internal model might have a higher API price than the ~$19.5M I estimated based on Astra's pricing.

Re: Navier-Stokes Announcement

#57

Post by xanderlewis »

famouswaffles wrote: post #44
seanhunter wrote: post #40

Earlier quoted context omitted.

That’s a big if. In the maths community, there has been a feeling that Navier-Stokes was close to being solved for a while now. I don’t know of anyone credible who feels that way about the Riemann hypothesis. Here’s what Terrence Tao had to say about it https://youtu.be/vuT-2_e4NHg Edit to add: The fun part about the RH since people mentioned lean in a sibling thread is that in lean’s mathlib4 there is verified state…

It's really not that big. Yeah Navier-Stokes was easier than Riemann but that's not really the issue. AI has and will improve at a much greater rate than human mathematicians. So it's really a question of if AI gets good enough to tackle it before any human does. It doesn't look like humans will be solving it anytime soon but where will AI be in 2 years ? Hell, it looks like at least one other result will be announce…

Has and will. Are you going to back that assertion up at all, or just repeat it like that other viral thought-terminating cliche: ‘this is the worst the models will ever be’?

Re: Navier-Stokes Announcement

#58

Post by famouswaffles »

xanderlewis wrote: post #57
famouswaffles wrote: post #44

Earlier quoted context omitted.

It's really not that big. Yeah Navier-Stokes was easier than Riemann but that's not really the issue. AI has and will improve at a much greater rate than human mathematicians. So it's really a question of if AI gets good enough to tackle it before any human does. It doesn't look like humans will be solving it anytime soon but where will AI be in 2 years ? Hell, it looks like at least one other result will be announce…

Has and will. Are you going to back that assertion up at all, or just repeat it like that other viral thought-terminating cliche: ‘this is the worst the models will ever be’?

Yes. This is the worst the models will ever be. Perhaps you should start paying attention to that now.

Re: Navier-Stokes Announcement

#59

Post by eru »

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.

I'm not sure it actually makes a difference. OpenAI doesn't care about the million dollars in any case. And the judgement that they did it is independent of whether the Clay people agree: you can make up your own mind and so can everyone else.

Though it would be funny if no one ever bothers publishing the result in an appropriate journal, and thus the prize technically can never be claimed.

Re: Navier-Stokes Announcement

#60

Post by eru »

seanhunter wrote: post #32
baby wrote: post #10

Earlier quoted context omitted.

It’s easy to verify the lean statement, you don’t need to read the proof. That is part of the breakthrough

You absolutely need to read the lean proof firstly to assess the correctness of the proposition it is proving (ie in this case that it is actually proving or otherwise the smoothness of navier-stokes in R^3 and not something else) and secondly to determine whether the proof is “honest” in the sense given here https://lean-lang.org/doc/reference/latest/ValidatingProofs/

You don't need to read the lean proof for that, only the statement.
Post reply on HN