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

251–260 of 292 posts

Re: Navier-Stokes Announcement

#251

Post by stbede »

pred_ wrote: post #174
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.

And chances are they never will publish it in any kind of useful format. Right now, the scientific community is outraged at OpenAI for going about their announcement in the least productive fashion they could have. It really does seem like they have no interest in progressing our understanding of maths outside of mining it for marketing material.

Boo hoo. OpenAI got the result only days ago. It makes perfect sense for them to take the win in marketing, and it's fine if they take a few months putting together the paper and present it more productively later. The scientific community didn't get the result themselves, so it isn't theirs to be bossing everyone else around about.

I don't care much for AI myself, or smart phones either, for that matter. I would be content if NS remained a mystery for another 100 years - or forever. But goodness, does the "scientific community" need to take a deep breath and count down from 10.

Re: Navier-Stokes Announcement

#252

Post by HotHotLava »

gerdesj wrote: post #244
soerxpso wrote: post #223

Earlier quoted context omitted.

It's formalized in Lean, isn't it? Do you also rely on a community of C++ experts to tell you whether a program compiles or not?

"It's formalized in Lean, isn't it?" If that's the current burden of proof required in your world for maths then that's fine! 't'ain't in my world: I want to see peer reviewed and published. Surely that's not too much to ask. Its not perfect but generally works rather well for maths. I'm not a sodding programmer so please don't assume everyone here is one. I'm not a mathematician either but I do have standards: Your…

In what world is peer review a higher standard than formal verification in Lean?

Not in the world mathematicians have been living in for the past decades at least. Nearly all big theorems that have been formalized so far had been published beforehand, and it was usually regarded as a step up in rigor. Wrong results get published in peer reviewed journals all the time.

Re: Navier-Stokes Announcement

#253

Post by stbede »

What I'm not seeing reported on much is if the result reveals any new techniques or ideas that advance mathematics - which is what we usually hear is the reason to work on these problems. Or does the resolution of NS just add a fact to the list without any new understanding.

Re: Navier-Stokes Announcement

#254

Post by stbede »

thaumasiotes wrote: post #81
d0mine wrote: post #51

Earlier quoted context omitted.

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

It's a simple binary classification. AI-generated proofs can't be "honest", and the only other possibility is "malicious".

The opposite of malicious is not honest. Nor do I see how motivations fall on a binary. The user submitting an AI proof can be honest, or malicious, or careless, or overzealous, or incompetent, or a whole bunch of other things. As far as the AI's motivations, "malicious" is just as much an anthropomorphism as "honest" and both descriptions are absurd. Nor do I really understand how any proof, regardless of its origin can be called honest. I think their definition of a "malicious" proof makes sense, but I don't see at all why an AI generated proof necessarily meets that definition.

Re: Navier-Stokes Announcement

#255

Post by soVeryTired »

stbede wrote: post #251
pred_ wrote: post #174

Earlier quoted context omitted.

And chances are they never will publish it in any kind of useful format. Right now, the scientific community is outraged at OpenAI for going about their announcement in the least productive fashion they could have. It really does seem like they have no interest in progressing our understanding of maths outside of mining it for marketing material.

Boo hoo. OpenAI got the result only days ago. It makes perfect sense for them to take the win in marketing, and it's fine if they take a few months putting together the paper and present it more productively later. The scientific community didn't get the result themselves, so it isn't theirs to be bossing everyone else around about. I don't care much for AI myself, or smart phones either, for that matter. I would be…

Was it a marketing win though? My takeaway is: if you're doing groundbreaking work with openAI's models and they find out, at best they'll outspend you and scoop you. At worst they'll steal your chat history.

Re: Navier-Stokes Announcement

#256

Post by pietz »

Stevvo wrote: post #191
pietz wrote: post #166

Are there still any reasonable arguments to be mad at OpenAI at this point? Looking at how everything unfolded, this seems to have hit them way harder then they deserved.

They said they started working on millennium problems after hearing a rumor someone had found a solution to one of them. That's just bad taste. It indicates negative motivation rather than positive motivation from the start.

Not someone. Their single competitor. During a time when they were validating their newest internal model. What would you have done?

Truly, if this is the biggest criticism left, they should be celebrated. While in reality, all of this has a bitter aftertaste.

So weird.

Re: Navier-Stokes Announcement

#257

Post by auggierose »

athrowaway3z wrote: post #245
auggierose wrote: post #209

Earlier quoted context omitted.

Still waiting for a definition. People giving nonsense reviews is a feature of the peer review system though, yes.

I want to ensure your PhD is actually from somebody who is acknowledged in the system of peers I bought into, before I want to risk wasting more of my time defining and explain while guessing at your ability to parse and understand them.

Or you could just give me a sensible definition.

Re: Navier-Stokes Announcement

#258

Post by HarHarVeryFunny »

famouswaffles wrote: post #233
HarHarVeryFunny wrote: post #203

Earlier quoted context omitted.

Most research mathematicians are employed as academics, and it's hard to see universities replacing teaching staff with AI even if that were possible. IMO giving a hypothetical AlphaMath to mathematicians, the same way Google gave AlphaFold to research chemists/biologists, would have resulted in far better PR, and the profit opportunity of attempting to replace the jobs of either research group is minimal. It's downr…

>Most research mathematicians are employed as academics, and it's hard to see universities replacing teaching staff with AI even if that were possible. If universities come to only need research mathematicians for teaching ability, then it would still gut the profession. You would presumably need far fewer of them for their research ability, and hopefully hire more people who can actually teach. It's strange that you…

> You would presumably need far fewer of them for their research ability, and hopefully hire more people who can actually teach

I suppose you are suggesting that research mathematicians are either over-qualified mathematically and/or under-qualified in ability to teach, but it seems pretty clear that universities prefer to hire domain experts whose reputations and long publication lists attract students and raise the perceived academic standards of the school.

Your "scenario" of much math research soon being done by AI (supervised and paid for by who, one might wonder), while universities hire people chosen for their teaching skills not academic reputation, seems a bit of a stretch ...

> You're asking why they don't market GPT as "AlphaFold for Mathematicians". They don't because it's not.

No, I am not asking that, nor asking anything for that matter.

I was pointing out that giving a free research tool to mathematicians would likely be better received, and receive better press, than doing something that most top-tier mathematicians are opposed to.

My hypothetical "AlphaMath" certainly could just be free GPT-N access for academics/researchers (as they are also doing to some extent), or it could indeed be a custom system that OpenAI built as a gift to the math community.

As far as the AI companies acting in slimy fashion goes, the most slimy behavior of all is to strongly believe you are doing something that will kill people and cause massive societal disruption ... and still keep doing it.

Re: Navier-Stokes Announcement

#259

Post by jltsiren »

soerxpso wrote: post #223
Aissen wrote: post #219

Earlier quoted context omitted.

> 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. No I cannot, and I'd argue most people can't either. We rely on mathematicians, peer review, and letting the scientific process run its course.

It's formalized in Lean, isn't it? Do you also rely on a community of C++ experts to tell you whether a program compiles or not?

Verification with Lean is a piece of empirical evidence that the proof is correct. The paper passing peer review would be another. But even together, those two would be insufficient to establish the claim.

While it's a convenient to assume that mathematics deals with logical statements, any attempt to evaluate those statements relies on physical processes with both known and unknown failure modes. There cannot be a test that establishes it unambiguously whether a claim is true or false. In all nontrivial situations, mathematical truth is based on expert consensus. When a new claim is made, people will try to raise and resolve objections, until a consensus emerges one way or another.

As for C++, all compilers are different. For any given compiler, there are valid C++ programs the compiler fails to compile and invalid programs it compiles without any errors or warnings. And now that I think of it, a new version of a compiler crashing with valid code earlier versions used to handle is the only class of compiler bugs I see with any regularity.

Re: Navier-Stokes Announcement

#260

Post by shakna »

soerxpso wrote: post #223
Aissen wrote: post #219

Earlier quoted context omitted.

> 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. No I cannot, and I'd argue most people can't either. We rely on mathematicians, peer review, and letting the scientific process run its course.

It's formalized in Lean, isn't it? Do you also rely on a community of C++ experts to tell you whether a program compiles or not?

Formalized in Lean, just five months ago [0], resulted in discovery of bugs.

Just because Lean can compile it, does not mean it is safely proven. It is the start of a process to check whether something actually holds, not the end.

[0] https://news.ycombinator.com/item?id=47759709

Post reply on HN