Live data from Hacker News

Navier-Stokes Announcement

claymath.org

61–70 of 292 posts

Re: Navier-Stokes Announcement

#61
post #33
post #12

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

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.

If you consider this event in isolation it is cause for celebration. But the controversy around this isn't so much about how the proof was obtained but what this means for the practice of mathematics going forward. It seems we can probably expect more and more results of this nature being dumped into the community. It's happened before that one person, Bill Thurston, was so successful in his field, proving theorem after theorem, that he inadvertently killed his field. People hesitated to enter his field, knowing that they could be scooped at any moment. It took years before his field recovered - and I think his famous essay was written in response to this.

https://arxiv.org/abs/math/9404236

Re: Navier-Stokes Announcement

#62

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.

I run this journal that you've never heard of that might interest you. I'd also like to invite you to be an editor, you can put it on your CV of course ...

Re: Navier-Stokes Announcement

#63

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 ?

Someone made a 'proof' of the Collatz conjecture that way in Lean.

However if the prove relies on a bug like that, you'll be able to 'simplify' the proof a lot and you'll be able to proof contradictions.

Re: Navier-Stokes Announcement

#64

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 ?

Soundness bugs in lean are not unheard of. That's why they recommend using external checkers for "malicious" proofs.

https://github.com/leanprover/lean4/issues/14576

Re: Navier-Stokes Announcement

#65

Earlier quoted context omitted.

Publish in academic language means accepted peer-reviewed paper.

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

Re: Navier-Stokes Announcement

#67
post #10

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

[dead]

Re: Navier-Stokes Announcement

#69
post #17

> 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

What a load od corporate drivel. "Interrogated"? Was their need for words so dire?

Per Merriam Webster, an interrogation is "a formal and systematic questioning," which is exactly what is called for when examining a proof.

Personally, I use the word "interrogate" when I want to question an idea without implying I want to discredit it.

https://www.merriam-webster.com/dictionary/interrogation

Re: Navier-Stokes Announcement

#70
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

You might be right. At this rate, if AI solves the remaining five problems, we're heading towards a hilarious situation where all the Millennium Problems are solved, but nobody wants to claim the prize money.

TBF a company the size of openai claiming a prize of this sort would be a pretty bad look. If they did accept it I expect they would inevitably redirect it to charity for PR reasons.

I'm surprised perelman turned it down though. Seems straightforward enough to offer half of it to the other guy if you feel strongly about it.

Post reply on HN