Proving things without comprehending them is a threat to intellectual work.
Outside of mathematics, I think it’s very rare for a single human to understand 100% of any complex undertaking, and this was true long before AI.
Navier-Stokes Announcement
271–280 of 292 posts
Re: Navier-Stokes Announcement
#272Earlier quoted context omitted.
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 ?
AI has autonomously found (many) proofs of False in Lean and Rocq, so it's not merely a theoretical concern. A misaligned AI agent tasked with proving the near-impossible just might wind up smuggling in a bug deep in a lemma somewhere (anyone remember the days back when AI routinely made tests pass by "fixing" the tests?). That said, I doubt OpenAI would be so foolish as to not do a cursory vetting of the proof for m…
> I doubt OpenAI would be so foolish as to not do a cursory vetting
I dunno, the HuggingFace incident was not too long ago. They might not be foolish, but their model could be smarter than them to "cheat", so to speak
Re: Navier-Stokes Announcement
#273In 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 sign…
I feel like this is answered in the very second paragraph?
> to elevate in the consciousness of the general public the fact that in mathematics the frontier is open, close at hand, and abounds with important unsolved problems; to emphasize the abiding value of working towards a solution of the deepest, most difficult problems; and to recognize achievements in mathematics of historic magnitude.
Also
> These are not arbitrary puzzles akin to fiendish crosswords. Rather, they are fundamental challenges that mark the frontier of human knowledge and challenge us to develop new structures and methods. They provide foci for the continuing struggle, across generations and cultures, to deepen our human understanding of mathematics and the universe that it describes.
Re: Navier-Stokes Announcement
#274Earlier quoted context omitted.
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.
That's a completely different matter. And does it matter to my point if they were successful or not? That's ex-post analysis. It seems clear that ex-ante, they wanted this to be a marketing win. The original poster complained that they wanted a marketing win.
My point is: why shouldn't they want a marketing win from this. What obligation does a non-academic institution have to follow the traditions of academia? Its result doesn't belong to academia. And if academia wants to subject OpenAI to their own internal processes and give them marching orders, it just isn't going to work and maybe - who knows - it'll even further erode their own legitimacy. Does anyone actually believe that NS would have been resolved in the 2020's if we lived in a parallel world where LLM's were never invented? Would Buckmaster have gotten as far as he did without LLM's doing a lot of the work for him? We can complain about AI companies contributing to mathematics, but are we complaining about Terence Tao using AI in his research? When Tao publishes something are we all going to go to war against him because maybe other mathematicians' prompts went into training the AI that Tao used?
Re: Navier-Stokes Announcement
#275Earlier 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?
Yes, but there's still the possibility that it's either exploiting a bug in Lean, or that the theorem statement is not set up correctly (i.e. it's actually proved a different theorem). My understanding is that the theorem statement is quite simple, so i guess the latter is not very likely, but the former is very much a possibility in a proof this large, and it will take some human eyeballs to go over it before convin…
Take a look at https://github.com/leanprover/comparator which was used to verify the result. It's of course not impossible that they're hitting some bug, but way harder than one would intuitively think. For starters, they'd have to hit two bugs in two independently written Lean kernels.
Re: Navier-Stokes Announcement
#276sounds 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.
Per 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/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 w…
Per the rules link that you yourself post, no, publication must not necessarily happen in a peer-reviewed journal.
Re: Navier-Stokes Announcement
#277Earlier quoted context omitted.
> 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. Yes, you can make problems arbitrarily complex. But the prize problems were chosen not just because the solutions appear likely to be very complex (the problem statements aren't necessarily inherently complex--there is a way to restate the Riemann…
and it seemed likely that solving them would require major breakthroughs If building a machine that solves these kinds of problems isn't a "major breakthrough," I don't know what is. Is the objection merely that it came from engineers rather than mathematicians? If so, there's plenty of room for contributions from many fields. The best thing a mathematician can do to advance their art, at this point, is to drop whate…
Note my comment was in response to someone questioning the very notion of prizes for mathematics problems. These prizes were created over a quarter century ago.
Re: Navier-Stokes Announcement
#278Earlier quoted context omitted.
https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke... Do you believe no open questions remain as to the truth of the Collatz conjecture?
Not sure what you mean. Here is what happened in that case: https://news.ycombinator.com/item?id=49137060#49140177
The point is, they "proved" the Collatz conjecture. You would not know they exploited a bug unless you actually went and dug into their proof. Can we be so certain this has not happened within the millions of lines of Navier-Stokes? In an ideal world, our proof assistants would be more battle-hardened by now (recent exploits deny this), our AI better aligned (their tendency to cheat at tests denies this), or their handlers more responsible (the Hugging Face incident denies this), but the reality is more complicated.
At this point in time, we really can't be confident in accepting proof certificates without any human eyes on the script that generated it. I still have 95%+ confidence in this particular result being trustworthy, but a precedent of blind faith is guaranteed to end badly.
Re: Navier-Stokes Announcement
#279Earlier 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…
And what of the personal threats?
Re: Navier-Stokes Announcement
#280Earlier 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?
Nothing to do with special hacks with operators. The reason it's useless because the precondition is never true. "If my aunt had two wheels and a handlebar then she'd be a bicycle"
Is the same problem with a non maths flavour.