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.
Navier-Stokes Announcement
61–70 of 292 posts
Re: Navier-Stokes Announcement
#62Earlier 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.
Re: Navier-Stokes Announcement
#63Earlier 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 ?
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
#64Earlier 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 ?
Re: Navier-Stokes Announcement
#65Earlier 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.
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
#66Re: Navier-Stokes Announcement
#67Their 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
Re: Navier-Stokes Announcement
#68Proving things without comprehending them is a threat to intellectual work.
Re: Navier-Stokes Announcement
#69> 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?
Personally, I use the word "interrogate" when I want to question an idea without implying I want to discredit it.
Re: Navier-Stokes Announcement
#70Earlier 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.
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.