9 ms·
Navier-Stokes Announcement
- swyx 1mo agosounds like they are providing notice that the clock has started on affirming the solution, that it IS presumptively solved, but that they are not commenting on the credit dispute nor the fields medalists open letter. seems appropriate.
- qlte 1mo agoPer the rules in their link, the clock starts after publication in a qualifying peer-reviewed journal so, no, I don't think that's the reason. https://www.claymath.org/wp-content/uploads/2022/03/millennium_prize_rules_0.pdf https://www.claymath.org/wp-content/uploads/2022/03/millenni... I'm sure they've been getting a lot of press inquiries and don't want anyone to misinterpret their silence as refusing to engage with OpenAI's solution. Now they have a statement on the record that can be quoted with a gentle reminder of the qualifying criteria (which makes clear they have nothing to evaluate either way yet). Also to emphasize the original optimistic ideals of the prizes and their role as neutral arbiters who aren't going to litigate anything outside the scope of the prize itself.
- HotHotLava 1mo agoPer the rules link that you yourself post, no, publication must not necessarily happen in a peer-reviewed journal.
- tristanj 1mo agoSmart move by them for waiting until the drama died down before making a completely neutral statement. The statement is so sterile they don't even mention who solved it. The word "OpenAI" doesn't appear at all.
- minimaxir 1mo agoWhat makes a man turn neutral? Lust for gold? Power? Or were they just born with a heart full of neutrality?
- num42 1mo ago"In recent years there has been an increasing sense of anticipation as breakthroughs in the surrounding field (some recognised by the Clay Research Award) have raised hopes that the Navier-Stokes problem might soon be resolved. The increasing ability of new technologies to accelerate mathematical research has heightened this sense of anticipation." Keyword: New Technologies
- stevefan1999 1mo agoThat is so vague you might as well call Windows NT new technologies
- bananaflag 1mo agowell, WNT > VMS
- jhrmnn 1mo agoIt’s written from a perspective of decades, not years
- jtpmath 1mo ago[flagged]
- mi_lk 1mo agoI really like this style of writing for some reason. Not sure how to put it but it’s a rare combination of a vague post and confidence
- asdfman123 1mo ago"We're just happy it was solved"
- hyperbovine 1mo agoFor one thing it was, I’m guessing, 100% written by actual humans. An increasingly rare phenomenon.
- monatron 1mo agoThis was the first thing I noticed as well. It was refreshing to read.
- lanyard-textile 1mo agoIt's optimistic and grounded in knowledge seeking. I like it too. It's easy to get caught in the details of today. Our skepticism, our distrust, our loathing. For people, for companies. This is a nice pull in the other direction, a silver lining. In the grand scheme of things, we're solving these frontier problems: Somebody did it and that's amazing. That's what it was all about when this started of in 2000.
- 47484848 1mo ago[flagged]
- teovall 1mo agoThe bureaucratic voice
- Planktonne 1mo ago> The statement is so sterile they don't even mention who solved it. Possibly because of the ongoing debate about who actually deserves credit.
- DrBenCarson 1mo ago> 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
- tgv 1mo agoWhat a load od corporate drivel. "Interrogated"? Was their need for words so dire?
- Zarathustra30 1mo agoPer 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 https://www.merriam-webster.com/dictionary/interrogation
- bmacho 1mo agoIt's a common (most common?) word in mathematics in this meaning. You interrogate a proof.
- drexlspivey 1mo ago[flagged]
- thih9 1mo agoMy honest take is that it was intentional. But yes, Poe’s Law will get referenced a lot in the next months/years I guess.
- da_chicken 1mo agoI think it was obviously intentional because they haven't accepted the solution yet. The purpose is to announce that they are aware of the claims of a solution, not to announce that a solution has been accepted. They're waiting on the required two year timeline before announcing whether or not the solution is accepted. Their writing reflects that they are explicitly NOT accepting a solution until then.
- Legend2440 1mo agoTheir 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.
- baby 1mo agoIt’s easy to verify the lean statement, you don’t need to read the proof. That is part of the breakthrough
- rramadass 1mo agoIf 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.
- phtrivier 1mo agoAlso, 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 ?
- eru 1mo agoSomeone 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.
- thaumasiotes 1mo ago> 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. I don't think this is true in general. It's an issue I've already run into in personal work. I want to do a proof that involves some cases. It happens to the best of us. In lean, the structure of a situation like this is that your single branch with a goal divides into multiple branches, all sharing the same original goal but including one additional premise that defines the branch. Sometimes I know that for whatever reason one case I have to deal with is impossible. The most correct way to show that is to prove False and then apply False.elim. This is the equivalent, in a human proof, of saying "I don't have to address this situation, because it can never arise". But it can be true that the premise defining the impossible case makes it very easy to "prove" the goal directly. And that's allowed too. The proof will still be just as valid if you map a logical path from a premise that can never be true to an inevitable consequence of that premise. But it's less informative and it lowers the quality of the proof. You may do it anyway because it's easier. This is the equivalent of saying "I don't know whether this situation can ever come up or not, but if it does I do know how to address it". It would be nice to do the explicit proof by contradiction whenever possible. But in the general case it may be very far from obvious that a contradiction is possible. I read your comment as claiming that if you can prove "false premise => goal", you can also prove "false premise => explicit contradiction", and I don't think this makes sense as a practical test. It's true in some sense, but discovering the proof of an explicit contradiction may be many orders of magnitude harder than discovering the proof of the goal. And in particular, I don't think it is necessarily the case that you will be able to prove a contradiction by simplifying the proof. You may need to add significant complexity.
- baby 1mo agoIt feels like a nice post. It’s almost like we’re not supposed to celebrate the fact that mathematics is accelerating.
- ComplexSystems 1mo agoI agree. I found it refreshing to get away from all of the AI drama and just enjoy the advancement in math.
- noisy_boy 1mo agoWe should enjoy the advancement. I also think the AI companies solving this or such problems with rewards shouldn't get any cash - that's the least they can do for human advancement having stolen the entirety of human knowledge and continuing to swallow never before seen amount of energy.
- kaffekaka 1mo agoFWIW I think OpenAI have stated they will not claim the award. They did not do it for the money obviously, but for the PR, that much everyone must agree on.
- SiempreViernes 1mo ago> They did not do it for the money obviously, but for the PR Doing it for the PR is still just doing it for the money, only they have a much bigger pile in mind.
- gps372 1mo agoAgree! '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.
- tristanj 1mo agoIt's worth mentioning that OpenAI will not be eligible for the Millennium Prize for quite a while. Per the rules listed https://www.claymath.org/wp-content/uploads/2022/03/millennium_prize_rules_0.pdf https://www.claymath.org/wp-content/uploads/2022/03/millenni... , Clay Mathematics Institute have some requirements to make this process deliberately slow. 1) The solution must be published in a qualifying outlet, i.e. a peer-reviewed math journal. Publishing on your own website (which is what OpenAI did) or posting arXiv does not count. 2) At least two full years must pass after publication in a qualifying journal, before CMI will even consider evaluating it. The intent is to give the maths community time to scrutinize the solution. Realistically, they'll be eligible for a prize ~2.5 years from now, or around 2029.
- ngruhn 1mo ago> 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
- tristanj 1mo agoYou 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.
- jtpmath 1mo agoI did and was intending to claim the prize, that is why I worked with GPT-4 and GPT-5 to program the algorithms that lead to the breakthrough. You think NS is a surprise? Wait until you see that my NS counterexample was based on my RH disproof.
- seanhunter 1mo agoThat’s a big if. In the maths community, there has been a feeling that Navier-Stokes was close to being solved for a while now. I don’t know of anyone credible who feels that way about the Riemann hypothesis. Here’s what Terrence Tao had to say about it https://youtu.be/vuT-2_e4NHg https://youtu.be/vuT-2_e4NHg Edit to add: The fun part about the RH since people mentioned lean in a sibling thread is that in lean’s mathlib4 there is verified statement of the Riemann Hypothesis with a comment that says something like “instantiating an object of this type will lead to a prize of a million dollars”
- unknown-unknown 1mo agoIn my opinion, I think the Clay Mathematics Institute deserves some criticism for all the drama surrounding these problems. Mathematicians know that you can make problems arbitrarily complex, and declaring problems with large prizes attached to them can lead to a lot of competition and drama. I feel that mathematics should be free from competitions and the pursuit of glory. However, after reading the open letter signed by 25 Fields Medalists, I became quite concerned. It feels like the mathematical world is changing very rapidly, almost overnight. I used to think that before AI, you could spend your entire lifetime working on some of the hardest problems in mathematics. If you were an introvert or someone who enjoyed solitude, all you really needed was a pencil, some paper, and an eraser. You could spend years thinking about a problem, and if you were lucky enough to make a breakthrough, it would be your own journey. Now AI is changing that. I wonder what this means for the kind of mathematics that people have traditionally done. Mathematics has given us so many stories of lonely geniuses and their passions, people like Andrew Wiles, Grigori Perelman, and Yitang Zhang. Their stories are interesting because they show how deeply personal mathematics can be. They spent years working on problems because they were genuinely interested in them. I am worried that we might slowly lose some of that side of mathematics as AI becomes more powerful. I do not think change is necessarily bad, but I think it is worth thinking about what mathematics should be in the future and whether it can still remain a deeply personal pursuit of curiosity and understanding.
- drexlspivey 1mo ago> In my opinion, I think the Clay Mathematics Institute deserves some criticism for all the drama surrounding these problems. Mathematicians know that you can make problems arbitrarily complex, and declaring problems with large prizes attached to them can lead to a lot of competition and drama. I feel that mathematics should be free from competitions and the pursuit of glory. Currently 0/2 Millenium problem solvers claimed the prize money so clearly money is not their motivation for tackling the problem.
- joedwin 1mo agoMoney is target but this millenium price is not enough for them. Openai is bringing machine gun to competition that used only knife and pistol.
- deleted 1mo ago[deleted]
- desighoda 1mo ago[dead]
- andsoitis 1mo agoProving things without comprehending them is a threat to intellectual work.
- thih9 1mo agoBased on recent history, we’re likely going to ignore this threat, continue doing this and perhaps call it vibe mathing.
- alain94040 1mo agoWhy is it a threat and not an opportunity? Imagine if in ancient times there was their Oracle that could produce mathematical proofs of any question you asked it, would you burn it or try to understand how it works and use it to ask questions you are stuck on?
- vouaobrasil 1mo agoI would burn it because it's too much power for any one person to handle. Or, I would take it for myself by force and use it to dominate everyone else.
- aeve890 1mo ago>without comprehending Very on brand with using AI for everything.
- Stevvo 1mo ago
- scrollaway 1mo agoI am utterly fascinated by the amount of comments here from engineers that clearly have zero experience with mathematics making utter fool of themselves by claiming to know better than mathematicians what their jargon is/means, how publishing works/should work, etc… I try not to go down the route of “hn was better before!” but… jeez, do better, people. What happened to this community, there used to be some effort to not be bottom-barrel like this.
- aaa_aaa 1mo agoWhat did you expect? Degree of BS increases together with the population.
- scrollaway 1mo agoPut simply, I expected better, friend.
- zeroonetwothree 1mo agoGell-Mann Amnesia HN version?
- scrollaway 1mo agoFor this I'd need to be any good at mathematics.
- p1dda 1mo ago[dead]
- Marchant_hq 1mo agoThe two-year publication rule is the interesting part. OpenAI doesn't need the million, and the community will judge the result regardless of whether Clay ever accepts it.
- HarHarVeryFunny 1mo agoThe result was never the point. Clearly the real-world cannot "blow-up" - real-world water vortices do not reach infinite velocity, etc. The point of having Navier-Stokes as a Millennium prize was to hopefully generate new mathematics and techniques along the way, and auto-generating a sprawling AI-slop proof or millions of lines of Lean does not accomplish that result. Clearly OpenAI has no interest in the math itself - to them this was just a trophy animal to shoot and stuff. I would be very surprised if they now helped analyze the proof and try to extract the mathematical value out of it, and this would obviously require outside help who are probably not inclined to help OpenAI math-wash their behavior.
- zeroonetwothree 1mo agoRight, the real world doesn’t blow up. So if N-S does then it means in some situations it doesn’t model the real world well. That’s important because if we can understand those situations we can avoid erroneously relying on it.
- HarHarVeryFunny 1mo agoDid anyone ever think that N-S was a perfect model?
- jltsiren 1mo agoClay will award the prize (or choose to not award it) when there is an expert consensus that the problem has been solved and the solution is correct. The rules merely state what that would mean in some typical cases. There is always an option that Clay changes the rules to match the reality better.
- pietz 1mo agoAre 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.
- Stevvo 1mo agoThey 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.
- pietz 1mo agoNot 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.
- Stevvo 1mo agoThat is not the narrative given in the OpenAI announcement. They claim to have started working on it after "we heard rumors that two Millennium Prize problems had been resolved", on September 1st, that "we later realized was related to Levent Alpöge" on Sepetember 6th "After the completion of our full project and lean verification" That does stretch the reader's credulity. I think most people find it far more likely the rumor was related to Anthropic all along.
- perching_aix 1mo agoTL;DR: - "yeah we know" - "looking into it" - "will ping you" - "might take a while though" + preemptive linguistic cushioning in case they feel socially (politically) compelled enough to forbid clanker proofs in their solution acceptance criteria, or in case they decide against conceding to such pressuring
- dang 1mo agoRecent and related. Others? OpenAI’s Navier-Stokes release included a Lean 4 formal proof - https://news.ycombinator.com/item?id=49650326 https://news.ycombinator.com/item?id=49650326 - Sept 2026 (179 comments) More questions about whether researchers can trust OpenAI with unpublished math - https://news.ycombinator.com/item?id=49639408 https://news.ycombinator.com/item?id=49639408 - Sept 2026 (813 comments) The Navier–Stokes Millennium Prize Problem - https://news.ycombinator.com/item?id=49621697 https://news.ycombinator.com/item?id=49621697 - Sept 2026 (237 comments) Tao: Open math problems being non-renewably mined by AI - https://news.ycombinator.com/item?id=49616968 https://news.ycombinator.com/item?id=49616968 - Sept 2026 (420 comments) On the Navier–Stokes Millennium Prize Problem - https://news.ycombinator.com/item?id=49613262 https://news.ycombinator.com/item?id=49613262 - Sept 2026 (1134 comments) Navier-Stokes – Tristan Buckmaster [pdf] - https://news.ycombinator.com/item?id=49605915 https://news.ycombinator.com/item?id=49605915 - Sept 2026 (827 comments)
- stbede 1mo agoWhat 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.
- zeroimpl 1mo agoMy understanding is that it’s proof by counterexample, so the main thing to study would be the implications of the counterexample. The technique used to find it sounds like a lot of brute force. But I’m not a mathematician, and maybe the AI used some clever techniques to narrow in on it.