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

151–160 of 292 posts

Re: Navier-Stokes Announcement

#151

Post by mr_mitm »

raegis wrote: post #30
auggierose wrote: post #11

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.

If I recall (too lazy to check) folks made slight improvements to Perelman's work and published it in mainstream journals, satisfying the "qualifying outlet" requirement.

I checked, you're right, but I think it's important to note that the prize did go to Perelman and he declined to accept.

Re: Navier-Stokes Announcement

#152

Post by paulddraper »

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?

“if X then Y” means “(not X) or Y”

E.g. “If it’s raining, the sidewalk is wet.” That statement holds if it’s not raining or the sidewalk is wet.

This is a common occurrence in mathematics, where someone might not be able to unconditionally prove Y, but they can under the condition X. Later, another mathematician might build on this by proving X, thereby transitively proving Y. (Or conversely, they might unconditionally disprove Y, thereby disproving X.)

Many hard problems are answered this way.

For example, Fermat’s Last Theorem was proven assuming the Taniyama-Shimura-Weil Conjecture, then Wiles proved the conjecture.

Thousands of theorems rely on the the unproven Reinmann Hypothesis, which is why it’s so interesting to mathematicians.

But if your precondition is “stupid,” your proof is stupid.

Re: Navier-Stokes Announcement

#153

Post by mr_mitm »

setopt wrote: post #125
moffkalast wrote: post #109

Earlier quoted context omitted.

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

Not really. It's not peer reviewed, but it's also not a free-for-all repository. If you make a new account, you either have to get someone to vouch for you, or you have to wait arXiv mods to look carefully through your first few preprints. If you are found to post pseudoscience, overly fringe theories, etc., you'll get banned from arXiv; that's why alternative repositories like vixRa.org popped up. But I know why you…

I also don't remember checks, but I believe that having an email address of an approved organization was enough to pass.

Re: Navier-Stokes Announcement

#154

Post by athrowaway3z »

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.

Something like this sketch work for you?

peer(X, 0) :- founding_peer(X).

electorate(T, count) :- peer(Y, T).

support(X, T, count) :- candidate(X), peer(Y, T), recognizes(Y, X, T+1).

peer(X, T+1) :- support(X, T, Votes), electorate(T, Total), 2 * Votes > Total.

Re: Navier-Stokes Announcement

#155

Post by peacefullmind »

thrance wrote: post #127
c7b wrote: post #93

Earlier quoted context omitted.

Even funnier that it wouldn't even be the first time that happens: https://en.wikipedia.org/wiki/Grigori_Perelman

And he also gave up his trophy, which is displayed in a random corridor of a random math museum in Paris, where visitors pass by without looking, lacking most, if not all, of the context. Only because I knew the story and the man did I recognize the object for what it was.

where is it displayed , in which museum ? As a mathematician it would be cool to visit it, but I can't find anything on google.

Re: Navier-Stokes Announcement

#156

Post by elteto »

tristanj wrote: post #121
u1hcw9nx wrote: post #86

Earlier quoted context omitted.

OpenAI has stated that they will not claim the prize. https://openai.com/index/navier-stokes-solution/ While the scandal is still unraveling, it seems that OpenAI did a rush job to steal other mathematicians' thunder and finish the proof first. OpenAI released a statement that their work does not relate to the work of the other team, but it clearly does. They use the same niche smooth-forcing mechanism. Altman and Bu…

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…

This is what Terence Tao said of Buckmaster’s and Alpolge approach:

“There does not seem to be anything in principle preventing the methods from extending all the way to Navier-Stokes, and there is even a non-negligible chance that the forcing term could be eliminated entirely, although there are an enormous number of technical difficulties that would ensue in implementing that program. At this point, I would not be surprised if one could batter out such an extension by pouring an enormous amount of compute and AI assistance at such a task…”

Pouring infinite AI resources into it is exactly what OpenAI did.

Re: Navier-Stokes Announcement

#157

Post by empath75 »

i_no_can_eat wrote: post #120
u1hcw9nx wrote: post #71

Earlier quoted context omitted.

Lean roof search tactics can generate vacuous proofs. They are not errors or a degenerate cases. They are completely valid, sound proof terms. Building a system that reliably detects vacuous proofs in all cases is fundamentally undecidable. It's equal to the halting problem.

Can you elaborate on what constitutes a vacuous proof?

When I first started playing with lean I accidentally defined a group in such a way that it was reduced to triviality. It had one object in it, so everything in the group was trivially equal to everything else. It was not the group that I was trying to prove something about, but the proof went through.

It was too easy, so I double checked my definitions, but it is quite easy to do something like that. And Claude does things like that quite frequently.

I am going through the exercise right now of trying to get Claude to formalize a published paper and it is a _struggle_ to get it not to take shortcuts or prove approximations of the paper’s theorems and then tell you it’s done.

Re: Navier-Stokes Announcement

#158

Post by pegasus »

peacefullmind wrote: post #155
thrance wrote: post #127

Earlier quoted context omitted.

And he also gave up his trophy, which is displayed in a random corridor of a random math museum in Paris, where visitors pass by without looking, lacking most, if not all, of the context. Only because I knew the story and the man did I recognize the object for what it was.

where is it displayed , in which museum ? As a mathematician it would be cool to visit it, but I can't find anything on google.

There can't be that many math museums in Paris...

Re: Navier-Stokes Announcement

#159

Post by AnimalMuppet »

Razengan wrote: post #131
adastra22 wrote: post #31

Earlier quoted context omitted.

Publish in academic language means accepted peer-reviewed paper.

Seems like artificial and maybe bitter gatekeeping

For giving away a million bucks, you get to gatekeep however you choose.

But no, peer reviewed and published in a reputable journal is a fairly normal standard.

Re: Navier-Stokes Announcement

#160

Post by thrance »

peacefullmind wrote: post #155
thrance wrote: post #127

Earlier quoted context omitted.

And he also gave up his trophy, which is displayed in a random corridor of a random math museum in Paris, where visitors pass by without looking, lacking most, if not all, of the context. Only because I knew the story and the man did I recognize the object for what it was.

where is it displayed , in which museum ? As a mathematician it would be cool to visit it, but I can't find anything on google.

It's at Maison Poincaré, in a kind of theater room with a looping movie. There's some neat stuff, but it's mostly targeted at children.
Post reply on HN