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

101–110 of 292 posts

Re: Navier-Stokes Announcement

#101

Post by kzrdude »

Paracompact wrote: post #74
zone411 wrote: post #53

Earlier quoted context omitted.

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…

If we read the link, it has a section called Gold Standard: comparator and external checkers, and comparator is how OpenAI has gone about checking their lean proofs.

Re: Navier-Stokes Announcement

#102

Post by kzrdude »

ncruces wrote: post #75
ngruhn wrote: post #13

Earlier quoted context omitted.

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

But if I remember correctly, he gained recognition for his achievement rather quickly after posting.

Re: Navier-Stokes Announcement

#103

Post by scrollaway »

I am utterly fascinated by the amount of comments here from engineers that clearly have zero experience with mathematics making utter fool of themselves by claiming to know better than mathematicians what their jargon is/means, how publishing works/should work, etc…

I try not to go down the route of “hn was better before!” but… jeez, do better, people. What happened to this community, there used to be some effort to not be bottom-barrel like this.

Re: Navier-Stokes Announcement

#104

Post by holowoodman »

glimshe wrote: post #100
jltsiren wrote: post #91

Earlier quoted context omitted.

It's possible that Clay Mathematics Institute will not award the prize at all. The spirit of the rules seems to be that the result can be attributed clearly to one or more individual mathematicians. If the attribution remains unclear (maybe because the main contributions were made by AI), the rules include an option for not awarding the prize at all.

Wouldn't the proof be attributed to the people who operated the AI? After all, it took more than writing a "prove the navier Stokes Clay problem" prompt.

> After all, it took more than writing a "prove the navier Stokes Clay problem" prompt.

Yes, but it took far less than using your meat brain to prove the Navier-Stokes Clay problem.

Re: Navier-Stokes Announcement

#105

Post by wokwokwok »

auggierose wrote: post #77
athrowaway3z wrote: post #65

Earlier quoted context omitted.

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.

Your (many) replies on this topic are being down voted for a reason; please either post substantive comments or stop.

Re: Navier-Stokes Announcement

#106

Post by hyperbovine »

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

For one thing it was, I’m guessing, 100% written by actual humans. An increasingly rare phenomenon.

Re: Navier-Stokes Announcement

#107

Post by crowfunder »

vatsachak wrote: post #21
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…

Who cares about the prize and the outdated methods? OpenAI and Anthropic might have 3 millennium problems by December

https://xkcd.com/605/

Re: Navier-Stokes Announcement

#108

Post by Planktonne »

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.

> The statement is so sterile they don't even mention who solved it.

Possibly because of the ongoing debate about who actually deserves credit.

Re: Navier-Stokes Announcement

#109

Post by moffkalast »

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.

Anyone can put anything on arxiv, it counts the same as printing it on tissue paper.

Re: Navier-Stokes Announcement

#110

Post by auggierose »

wokwokwok wrote: post #105
auggierose wrote: post #77

Earlier quoted context omitted.

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

Your (many) replies on this topic are being down voted for a reason; please either post substantive comments or stop.

Yes, for a reason, but not a reasonable reason, but the same reason you have for your comment: you just don’t know any better.
Post reply on HN