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

71–80 of 292 posts

Re: Navier-Stokes Announcement

#71

Post by u1hcw9nx »

zone411 wrote: post #53
seanhunter wrote: post #32

Earlier quoted context omitted.

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_o…

Lean roof search tactics can generate vacuous proofs. They are not errors or a degenerate cases. They are completely valid, sound proof terms.

Building a system that reliably detects vacuous proofs in all cases is fundamentally undecidable. It's equal to the halting problem.

Re: Navier-Stokes Announcement

#73

Post by Bluestein »

kaffekaka wrote: post #43
gps372 wrote: post #36

Earlier quoted context omitted.

If it works (something they need to be convinced about), if it accelerate mathematics and solve complex problems for humanity, then why not? Aren't they already using computers, mobiles, calculators, etc. already?

Yes, but a big part of the problem right now is that two big labs have monopoly on the resources and they for sure are not working for the benefit of mankind. The Startrek future is still a long way out.

Earl Grey, hot.-

  ⎿  You've hit your session limit · resets 2:52am (123°24′W Etc/GMT+8)
  /upgrade to increase your usage limit.

Re: Navier-Stokes Announcement

#74

Post by Paracompact »

zone411 wrote: post #53
seanhunter wrote: post #32

Earlier quoted context omitted.

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_o…

First of all, that is Fermat's Last Theorem, not Navier-Stokes.

Second of all, you did not read the link.

> In particular, we use honest when the goal is to create a valid proof. This allows for mistakes and bugs in proofs and meta-code (tactics, attributes, commands, etc.), but not for code that clearly only serves to circumvent the system (such as using the debug.skipKernelTC).

Given that AI has autonomously found proofs of `False` in Lean and other proof assistants, it is far from impossible that such a circumvention could be present somewhere in 13 million lines.

Re: Navier-Stokes Announcement

#75

Post by ncruces »

ngruhn wrote: post #13
tristanj wrote: post #8

It's worth mentioning that OpenAI will not be eligible for the Millennium Prize for quite a while. Per the rules listed https://www.claymath.org/wp-content/uploads/2022/03/millenni... , Clay Mathematics Institute have some requirements to make this process deliberately slow. 1) The solution must be published in a qualifying outlet, i.e. a peer-reviewed math journal. Publishing on your own website (which is what OpenA…

> or posting arXiv does not count The Poincaré conjecture guy also broke that rule. They wanted to give him the prize anyway but he refused. OpenAI announced they would also not claim the prize. Looks like no one wants this prize lol

Perelman posted to arXiv in 2002/3.

The prize was offered to him in 2010, after multiple others had digested his work and published elsewhere.

Re: Navier-Stokes Announcement

#76

Post by thaumasiotes »

athrowaway3z wrote: post #65
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.

By peers. Peer in peer-reviewed is a logical coherent and functional definition with answers. The logical issue with 'peers' is how to bootstrap it. At that bootstrap moment you can ask "by whom?". We are several centuries past that moment. The cultural/social question you might ask today is "why (keep) them?". At which point people will naturally ask you to make a strong case for "why not them?".

> The logical issue with 'peers' is how to bootstrap it. At that bootstrap moment you can ask "by whom?". We are several centuries past that moment.

Huh? We're about six decades past that moment.

Re: Navier-Stokes Announcement

#77

Post by auggierose »

athrowaway3z wrote: post #65
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.

By peers. Peer in peer-reviewed is a logical coherent and functional definition with answers. The logical issue with 'peers' is how to bootstrap it. At that bootstrap moment you can ask "by whom?". We are several centuries past that moment. The cultural/social question you might ask today is "why (keep) them?". At which point people will naturally ask you to make a strong case for "why not them?".

> Peer in peer-reviewed is a logical coherent and functional definition with answers.

What is the definition? If you tell me that, then I might be able to tell you if it is logical coherent and functional, I have a PhD in computational logic.

Re: Navier-Stokes Announcement

#78

Post by thih9 »

drexlspivey wrote: post #24
DrBenCarson wrote: post #4

> Today, CMI shares in the excitement of the global mathematical community as we contemplate the announcement that the Navier-Stokes problem has apparently been settled. We hope to see waves of new human understanding unleashed as the innovations behind this work are analysed and interrogated. That “apparently” feels load-bearing

[flagged]

My honest take is that it was intentional. But yes, Poe’s Law will get referenced a lot in the next months/years I guess.

Re: Navier-Stokes Announcement

#79

Post by Paracompact »

phtrivier wrote: post #47
rramadass wrote: post #18

Earlier quoted context omitted.

If the Lean initial-problem-setup/statements/assumptions/etc. aren't correct then the proof is meaningless. Lean does not know what it is that it is proving i.e. it does not have any semantic understanding but only executes formal logic. Humans need to verify everything.

Also, and sorry if it's been discussed to death (pointers welcome), but, what is the probability that the proof holds in lean becaude of... A bug in lean ?

AI has autonomously found (many) proofs of False in Lean and Rocq, so it's not merely a theoretical concern. A misaligned AI agent tasked with proving the near-impossible just might wind up smuggling in a bug deep in a lemma somewhere (anyone remember the days back when AI routinely made tests pass by "fixing" the tests?). That said, I doubt OpenAI would be so foolish as to not do a cursory vetting of the proof for malicious compliance, so the actual odds are probably pretty low.

Re: Navier-Stokes Announcement

#80

Post by nearbuy »

skayvr wrote: post #55
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.

Buckmaster (the mathematician) and Alpöge used and credit AI substantially for their proof. Even if OpenAI did copy their ideas, it still wouldn't show that this didn't come from AI improving.

OpenAI's proof is substantially different and I don't think anyone has claimed otherwise. The accusation is that they used the same avenue of attack, and it's an uncommon one, and that makes it suspicious that they may have taken the idea.

Post reply on HN