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

281–290 of 292 posts

Re: Navier-Stokes Announcement

#281

Post by rcbdev »

aarstid wrote: post #269
HotHotLava wrote: post #252

Earlier quoted context omitted.

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.

I find it really strange the way “peer-reviewed” is used by the general public as some gold standard of truth. As a former academic who has been there, the process is extremely arbitrary and variable. Are people aware that the “peer” refers not to a community or a committee, but literally to one random guy or maybe a couple with zero accreditation? And that the journal editor can do whatever they want with this peer’…

I keep thinking the exact same thing every time I'm asked to peer review a paper.

Re: Navier-Stokes Announcement

#282

Post by Razengan »

AnimalMuppet wrote: post #270
Razengan wrote: post #222

Earlier quoted context omitted.

One thing's for certain: True and false should not depend on convincing people.

Real true or false - which I define as correspondence (or lack thereof) with reality - does not depend on convincing people. Reality does not change when people become convinced; ideas correspond to reality whether people are convinced or not. But perceived truth and falsehood depend on convincing people - either convincing them one by one, or else convincing some gatekeeper, whose word will convince those who accept…

So if an AI proves something but ""rEpUtAbLe"" papers refuse to publish it just on grounds of it being AI, does that make it not true?

You know in the past women (and other marginalized people) weren't allowed to publish scientific papers for the majority of human history?

Is this how you want your "truth" to be?

If so then man, no sympathy; these institutions deserve to be broken down. Let them spaz on the floor and throw tantrums all they want.

Re: Navier-Stokes Announcement

#283

Post by tristanj »

amazingman wrote: post #279
tristanj wrote: post #121

Earlier quoted context omitted.

1) OpenAI and Buckmaster did not solve the same problem. Per https://x.com/IlinVasily29521/status/2097554700321329393 , here is a breakdown of who solved what. Tristan + Levent: 3D incompressible Euler with forcing OpenAI: 3D incompressible Euler without forcing OpenAI: Navier-Stokes with forcing No one: Navier-Stokes without forcing Euler equations = Navier-Stokes without viscosity. Forcing means external force. Abs…

And what of the personal threats?

You realize 1) There were no personal threats, you're being deceptive here and 2) Bushmaster threatened Bubeck (of OpenAI) first? Bushmaster redacted 90% of their conversation to stir up as much FUD as possible, but you can review Bubeck's later statements to fill in what actually happened.

From the statement:

  I said that if OpenAI released its result in the way proposed I would go public with what happened.
Translation: If you release this result, I will go public with my concerns that you plagiarized my work.

  The reply was, “Why would you ruin your career?” I replied that I am an academic, and asked why he thought going public would ruin my career.
Translation: Typically, making unfounded accusations of plagiarism will ruin your career. Why would you do that to yourself?

Bushmaster then redacts 90% of what Bubeck says next (because it would detract from the narrative he's trying to portray) and only includes the most inflammatory line.

   The reply was, “If you don’t want me to be nice, then I don’t have to be nice.”
Translation: You were the closest person to solving the problem. Even though we solved it and you didn't, we offered you to give you the Millennium prize and put your name on the paper, so long as you remove your coauthor (who works at Anthropic). We offered you this because we're being nice. Since you don't want to be nice (by accusing us of doing things we did not do), we're not going to be nice (and offer you the prize/co-authorship of the paper).

When you fill in the context, it's clear: 1) there is no personal threat like you claim and 2) this is hardly a threat, on a scale of threats you can make, this scores a 1.5 out of 10.

For context: Bushmaster is pissed at OpenAI because they sniped a problem he was toiling on for the past year, so during this conversation I believe emotions are quite heated.

I don't claim this interpretation is 100% accurate, but if you disagree, do reply with a better one yourself.

Re: Navier-Stokes Announcement

#284

Post by seanhunter »

eru wrote: post #114
seanhunter wrote: post #94

Earlier quoted context omitted.

You need to read the lean proof (not just the statement of the proposition) to assess whether the proof is honest. The link I provided is the lean prover community firstly officially agreeing with that claim and secondly explaining why that is the case.

Well, Lean needs to get its act together to fix the bugs.

They’re working on it, but the bulk of the effort goes into making it more useful to working mathematicians rather than resisting malicious proof attempts.

Re: Navier-Stokes Announcement

#285

Post by Humorist2290 »

Aissen wrote: post #219
eru wrote: post #59

Earlier quoted context omitted.

I'm not sure it actually makes a difference. OpenAI doesn't care about the million dollars in any case. 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. Though it would be funny if no one ever bothers publishing the result in an appropriate journal, and thus the prize technically can never be claimed.

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

In a way, this task is perfectly suited for LLMs. To even understand the problem statement, much less the proof or Lean, is an extremely specialized skill. The overwhelming majority of people who are aware of this news simply don't have the capacity to call BS. Maybe there are a few thousand people in the world who could, and it seems they haven't yet, but indeed it's only been a few weeks.

The more familiar analogy was when I look at the code that Claude spews for my partner. They take it at face value and hope it works. I usually find it very problematic, but only because I knew what to look for.

Re: Navier-Stokes Announcement

#286

Post by seanhunter »

perching_aix wrote: post #165
i_no_can_eat wrote: post #120

Earlier quoted context omitted.

Can you elaborate on what constitutes a vacuous proof?

If you have a software engineering background, it's like how semantic versioning is bollocks. Semantic versioning describes the following idealized setup: - you have an interface you expose (a contract, and thus a contract signature) - you do not change the contract signature -> patch version bump - you do change it but in a non-breaking way (e.g. additively) -> minor version bump - you do change it but in a breaking…

  > This mirrors the Lean statement and Lean proof situation. The statement is like an interface, and the proof is like the implementation behind that interface.
This is true in a very deep sense due to the Curry-Howard correspondence and calculus of constructions which are central to Lean. In Lean, the proposition you are proving is a type (so it really is an interface directly in the computer science sense) and the proof is a function which takes your hypotheses and returns a term of that type (so it really is the implementation of that interface). In fact in lean, you can just as well write this implementation as a lambda (this is known as “term mode”) as in the “tactic mode” that is more generally used in normal lean use. Lean really doesn’t care at all which one you use and you can switch between them within a proof quite easily without interfering with lean’s ability to check your proof at all.

   > Which really makes me wonder about the actual value proposition of Lean then, but alas...
The purpose of lean really is quite different from what most people on hn seem to want it to be. Lean is designed to be a useful tool for mathematicians who want to formalise areas of mathematics. It’s not a primary goal of most of the lean community to make something that is hardened against malicious proof attempts (although these are considered bugs and there is a small subcommunity who work on this area in particular). So it isn’t primarily for the benefit of people who want to “fire and forget” some proof without reading or understanding it and just get the check mark if it’s true.[1] It’s mainly for mathematicians who want a proof assistant to help them with their work.

[1] there are sub-tools such as comparator that are designed for this type of use case. https://github.com/leanprover/comparator

Re: Navier-Stokes Announcement

#287

Post by taneq »

program_whiz wrote: post #231
jacobrussell wrote: post #167

Earlier quoted context omitted.

I don’t think solving a millennium prize problem can be reduced to some DoorDash economics of “spent Y to make X.” What if it took someone their entire professional career to solve one of these problems, would it not be worth it by the same logic?

Surprisingly this is actually rather fitting in terms of time scale. When you consider it took ~10,000 agents 88 hours, or 880,000 hours to solve. That's 14.5 years in agent time of continuous 365/24/7 processing. Of course, humans solve things much more efficiently (and didn't also need the massive pre-training of every expert on the planet for 1,000,000,000 human years equivalent). But yeah, human researchers can s…

> But yeah, human researchers can solve a problem like this in a decade or so

None of them did, though, despite how many tried. So empirically, it seems unreasonable to say human researchers can solve ‘problems like this’.

Re: Navier-Stokes Announcement

#288

Post by seanhunter »

Panzer04 wrote: post #139
Tanjreeve wrote: post #124

Earlier quoted context omitted.

I present to you my new theorem as follows: If 1 == 3 then 3 == 3 ---- This statement is 100% logically coherent internally. But it also doesn't matter because we know that 1 does not equal 3 so this proof is completely pointless. I could also say 3 == 5 and it would still be logically sound but completely useless information.

For a laymen, I don't follow this. Are you proving for some arbitrary definition of == that isn't what we commonly consider the definition? How is it logically coherent? You mean only in the sense that you say it is and you haven't provided any rules to disprove it?

This is known as a “vacuously true” statement in formal logic. Let me write it out more in more detail and you’ll hopefully see why it’s consistent.

In logic, a proposition is some statement that can be true or false. So, let A be the proposition that 1 equals 3, and B be the proposition that 3 equals 3.

Now the poster is making a third proposition. If A, then B.

A is clearly not true. So in classical logic, B can be anything and “If A then B” is still true.

For example let B be the proposition that I am Elvis Presley (I’m not). So now we have “If one equals 3 then I am Elvis Presley”. This is clearly true. I’m not Elvis Presley, but that doesn’t matter because we’re not saying anything about what happens when one doesn’t equal 3.

Now, let’s try let B be the proposition that I am Sean Hunter (I actually am). So now we have “If one equals 3 then I am Sean Hunter”. This is clearly still true because we still are only making a claim about what happens when one equals three.

https://en.wikipedia.org/wiki/Vacuous_truth

By the way, this isn’t any kind of inherent contradiction or problem, it is just a possibly counterintuitive part of how classical logic works.

You see this type of statement (“If , then ”) being made a lot when people are exaggerating for effect, for example by Mr Bumble in “Oliver Twist”

   > 'That is no excuse,' replied Mr. Brownlow. 'You were present on the occasion of the destruction of these trinkets, and indeed are the more guilty of the two, in the eye of the law; for the law supposes that your wife acts under your direction.' … 'If the law supposes that,' said Mr. Bumble, squeezing his hat emphatically in both hands, 'the law is a ass--a idiot. If that's the eye of the law, the law is a bachelor’
https://www.literaturepage.com/read/olivertwist-460.html

Re: Navier-Stokes Announcement

#289

Post by eru »

Aissen wrote: post #219
eru wrote: post #59

Earlier quoted context omitted.

I'm not sure it actually makes a difference. OpenAI doesn't care about the million dollars in any case. 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. Though it would be funny if no one ever bothers publishing the result in an appropriate journal, and thus the prize technically can never be claimed.

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

> We rely on mathematicians, peer review, and letting the scientific process run its course.

Granted for the sake of argument. But for this process, there's no requirement anyone from Clay needs to be involved, nor that anything has to be published in a traditional journal.

Terrence Tao can download the pdf, think it over, and publish on his blog, and it would be just as valid. Then some other mathematician can write something on 4chan or whatever. (See https://en.wikipedia.org/wiki/Superpermutation#Lower_bounds,... for 4chan.)

Re: Navier-Stokes Announcement

#290

Post by eru »

spott wrote: post #235
MarkusQ wrote: post #232

Earlier quoted context omitted.

More likely it's because a million dollars one way or the other won't make a difference in the hole they are digging / mountain they are building.

It likely cost them more than a million in compute to solve it…

We know that it did.
Post reply on HN