It's kinda funny to realize that Lean is apparently so slow that for Fermat's Last Theorem proof verification runs only 1 order of magnitude faster than agents could generate the Lean code (15h verification with 230GB of RAM vs 11 days to generate it).
To what extent can you optimize Lean? It has to be simple enough to be auditable, does that mean you cannot use opaque optimizations to make it run faster?
Sure, but to clarify the article is describing formalization (writing a correct program), not verification (compiling said program). The author is not making the same comparison.
Verification is also open ended (not sure about lean specifically) - you could in theory give just the Navier-Stokes problem definition to an ATP and let it run.
It's because anthropic vibemathed it. I forgot the name but some other guy is working on a handwritten version of it and I bet it'll be more than just 1 magnitude faster.
What would be the point of that though? I think the reason Kevin wants to optimize it is for the understanding that will result from the process, not because anyone cares about having a Lean proof that compiles quickly...
Weren't the agents massively parallel, whereas the lean verifier presumably is not? Also, I presume said agents were themselves running the verifier on their own parts many times.
But what hardware was the verification vs agents on? Because you are likely comparing verification on a single beefy machine (say XX TFLOPS total) to agents running on a substantial inference cluster (say XXXX TFLOPS). So you're 1 order of magnitude might actually be 2-4 orders of magnitude.
Yeah, in essence. This is actually a pretty cool part of working in Lean. It's a somewhat normal convention to write something in a human readable way and then write a second optimized implementation with some kindness of correctness theorem connecting them. There was a whole open "competition" for writing a faster Lean kernel/proof checker that didn't sacrifice on soundness called Lean Kernel Arena. Fun reference point: https://kim-em.github.io/blog/2026-7-24-why-lean-is-faster-t...
There's a project called lean4lean that implements lean in lean. I guess ideally, if you had a kernel optimisation idea you could do a copy of the Lean model lean4lean has created, add the optimisation, then prove your new lean is equivalent in terms of what it can prove to the old lean
They estimated $40M of agent costs (it was a large fleet of them). Using the number in the post its closer to ~880,000 hours × $150/hour = $132 million for the human case. Still an amazing feat not quite "four orders of magnitude". The comparison is obviously pointless because coordinating 1M hours of intellectual labor isn't easy to say the least.
People seem to be talking about anything except the actual results with this particular announcement.
Its still astonishing that any sort of generalized computer program can solve a problem of this magnitude, and we have witnessed it happening in real time. I'd be curious to see if the new model can also do more direct proofs/inductive proofs.
Because the core of the issue is that it may well not have solved it, but instead plagiarised the significant step of the result from other researchers
That's why nobody's talking about how impressive this is, because its not nearly as impressive of a piece of work to simply cobble together other peoples' work that didn't know you were doing it. I could have republished relativity from einstein's notes, but people would correctly not be impressed with my ability
Until the plagiarism scandal is sorted out, its not a meaningful result at all, because nobody knows how much genuine innovation these models are displaying
Turning a bunch of vague research directions and exploratory prompts into a formalized proof is quite impressive on its own. OpenAI would have no incentive to taint its first math announcement of this magnitude if it knew it were "plagiarizing" another person's work.
People are grasping at straws it seems to dismiss the power of this new model they may have. Hate OpenAI for any reason you want, but denying the capabilities of models has been a losing game for the past 5 years.
It's perfectly reasonable to assume that the result itself is legit and that OpenAI behaved unethically.
Even by their own account, they decided to throw an unpublished model and millions of dollars in compute at this particular problem simply because they had heard rumours that other people were making progress and wanted to snatch the prize from them.
I really truly honestly am not sure what to make of this result from $20M in compute, 10K+ parallel agents (smells like brute force), and a pre-existing approach that was already bearing fruit. I know the models are good---I use them every day and continue to be impressed---but how much better than the benchmark of the best publicly available models is this supposed to be? It seems impossible to say.
But if it happened, they didn't know. Also OAI has demonstrated that they aren't big on understanding what they create, that their AI can get out of their control.
It's very simple really user data can be used to train future models, so maybe or definitely some users helped in solving the problem, there's no scenario were it is impossible this happened, as it would have been in a haskell or virtualized type of system where the model has absolutely no knowledge of the user data dataset in question (and even if virtualized the models can break virtualization anyways)
> Because the core of the issue is that it may well not have solved it, but instead plagiarised the significant step of the result from other researchers
It's also true however that I haven't seen a single write up trying to discern what did more of the work in those AI chats - the prompts or the responses - bubble to the surface, also since we don't have access to them.
For example, if I prompt Codex with "Make me a website about strawberry cake" and nothing else, and OpenAI announces they have the best strawberry cake minutes before I launch, I'm not sure they plagiarized anything.
We just don't know if this is quibbling over "who prompted first" or if the researchers came up with anything strikingly original by themselves.
The researchers apparently spend a year or so working on this, and it builds off significant previous work, so it seems like it was a pretty significant amount of work that OpenAI may have trained on
I'd love to see an in depth analysis of how much OpenAI actually did, but I suspect we'll never see that because it would indicate at least some plagiarism which undermines a lot of what OpenAI is putting out in public
The American Mathematical Society credits the Spanish researchers Diego Córdoba and Luis Martínez‑Zoroa with the breakthroughs that eventually led to this solution, and which were published from ~2023 onwards.
This is a good summary:
> In broad outline, the pair’s technique relies on creating an infinite sequence of “layers,” each of which is a non-singular solution to the equation they are studying. (They’ve applied similar techniques to both the Euler and Navier-Stokes equations, as well as to other related systems.) They then combine those solutions in what Martínez-Zoroa calls an “infinite cascade” to produce a new solution.
>
> That new solution, they showed, contains the desired singularity. However, even though each individual layer relies on a smooth forcing function, combining them together can cause the forcing function to have undesirable mathematical properties. That’s why their solution fell short of satisfying the Millennium Prize criteria. The remaining hurdle was to figure out how to create a similar infinite cascade that resulted not only in a singularity, but also in a smooth forcing function.
>
> That’s the step that both competing AI groups appear to have had success with.
The question is whether OpenAI started out from that published and well known research exclusively, or they also had some insight into the ongoing work of Tristan Buckmaster and Levent Alpöge.
On the one hand, OpenAI have already admitted that they only launched their massive effort after hearing rumours that this particular problem had been solved.
On the other, progress in mathematics research has accelerated significantly over the past months thanks to the availability of newer and more capable AI models. Alpöge himself presented a counterexample to the Jacobian conjecture on July, found with Claude Fable. So if model capability was a bottleneck, that gives credibility to the idea that an even more powerful unreleased model with massive compute would be able to make even faster progress.
It's worth noting that the case is that your input is being used to train their AI, and that's more important than whether it materially contributed, it cannot be denied or attributed accurately, it cannot be said with certainty which way it happened, and that's what's important.
It is very unlikely to be plagiarized, and claims of plagiarism are largely unfounded and show a lack of understanding of the situation. They fall apart when reviewing the timeline, and what was actually solved.
In late August, OpenAI completed a pretrain of its latest internal model. A model derived from this pretrain, built after August 28, found a solution to 3D incompressible Euler without forcing and Navier-Stokes with forcing. https://openai.com/index/navier-stokes-solution/
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. Absence of viscosity and presence of external force make blowup easier to construct.
Tristan+Levent ticked the weakest case, OpenAI ticked the two next weakest, then the final case is unsolved. Only the last two are eligible for the Millennium Prize. The Navier-Stokes general case remains unsolved.
Buckmaster disabled model training long before the August 15 breakthrough results, so these chats were not used as training data for OpenAI's model which solved Navier-Stokes.
Additionally, Tristan and Levent only solved the easiest version of the problem and did not have the key insights to solve the harder versions of the problem required for the Millennium Prize.
"We can say categorically that it is impossible for Dr. Buckmaster’s Codex prompts over the last two months to have influenced the system in any way, including training."
> And OpenAI directly addressed these plagiarism claims, and called them impossible
Funny, you were telling me two days ago that on the contrary, "it’s genuinely impossible to know how much of Buckmaster’s Codex data is in OpenAI’s training set":
Which is still a true statement, and you're being deceptive in your framing here. You're conflating two completely different things.
First, that OpenAI statement is in response to Buckmaster's plagiarism accusations regarding his August 15 breakthrough proof. Those accusations are unfounded because Buckmaster disabled data sharing on June 29. The model could not have seen or trained on his proof. Additionally, the model that found a solution to NS completed pre-training around August 25, and models take several months to train. The model very likely began its training prior to June, and would not be trained on any data from after that point.
Second, it's still genuinely impossible to know how much of Buckmaster's pre-June 29 data persists in OpenAI's systems. That includes all chats (which are anonymized then trained on), any (thumbs up/thumbs down) chat ratings used as RLHF feedback (which are anonymized), any synthetic data derived from said anonymized chats and RLHF feedback, and any downstream models derived from said synthetic data.
In short, Buckmaster's data has been anonymized, chopped into pieces, used to generate synthetic training data, then future models were trained on said synthetic data. There is no traceable chain of what happened to it. Buckmaster’s Codex data from prior to June 29 has been mixed and completely laundered, in a similar manner to a crypto mixer.
I’m unsure or not if this is true but I did see some people saying that that checkbox when off only anonymizes your data, but it still may be trained on. Someone correct me if I am wrong
Even if it does use your data with or without anonymization, it doesn't have to be intentional, it could just be a glitch, or a bug, or something we'll catch in the next update, it's all good man, just a normal computer error.
It doesn't seem like you're familiar with how mathematical research is done. Taking 6 weeks between a major breakthrough on a huge proof, and making your proof public, is not unusual.
It takes a lot of time to finish a proof and figure out the best way to present it. I would personally be surprised if Buckmaster had not gotten it mostly cracked before June 29th.
The timeline here does not support your argument. Quoting from Buckmaster's statement:
For most of the past year progress was slow. We worked through the literature and upgraded various preliminary results, up to obtaining finite time blow up for the Incompressible Porous Media equation (with smooth forcing). This was until about a month ago, when we had real progress: on August 15th, we obtained the blow up results, with smooth forcing, for both Boussinesq and Euler.
I can say the first LLM generated proof Levent sent me was the most horrendous I have ever read; we verified it on Lean on August 22nd. Since this point, we have been working around the clock to understand this proof and turn it into something readable.
Specifically: "For most of the past year progress was slow ... until about a month ago, when we had real progress: on August 15th"
And you avoided addressing the critical issue: they weren't even solving the same problem. Buckmaster solved a simplified and easier version of Navier-Stokes. OpenAI solved a harder version eligible for the Millennium prize. Buckmaster did not.
who cares about plagiarism? the biggest issue, as described by Terence Tao, is that AI companies don't understand the math they are publishing and do not devote any resources to answering questions about their methods after publishing results and getting a headline. they miss the whole point of mathematics. they do not contribute to the improvement of human understanding of math, perhaps because they are unable to.
It also needs to be said: The amount of compute that went into this is something. From some estimates I've seen, the compute cost alone would be around $10m, +/-
As a reference, for that kind of money one could put together a research group of 20-25 researchers, and keep them salaried for 5 years.
So while it is impressive, absolutely no doubt there, the SOTA access is so expensive that it is sort of unobtanium.
Luckily, the prices have historically reduced by a factor of 5-10 every year...but still, only those that swim in cash can afford this.
Once we have an existence proof of a particular technology, it doesn't take long for it to become economically viable and proliferate. And for something as useful as this, theres a strong economic incentive to get it to be as cheap and accessible as possible. Maybe not today, but certainly in a couple years I can imagine this level of intelligence being accessible to someone with a $20/mo plan, or even a free plan.
I remember being blown away when a then-unreleased version of GPT 5 took gold at the International Math Olympiad. Now I can run a model at home that can do that. We are more fortunate to have these tools than almost anyone is willing to acknowledge.
Interestingly it's this promise of the costs being able to be reduced what incentivizes the actual research.
If you tried to raise 25M to have 20 researchers on a salary for 5 years solving a specific math problem only academics care about, you probably wouldn't get much interest, or you would be able to solve 1 or 2 problems.
If however you promise that the money will go towards a technique that would allow to solve 10 thousand different math problems, and that costs will go down in the future, then you can raise much more than 25M.
Heck, it’s even astonishing that any sort of generalized computer program could even verify a proof of this magnitude that hasn’t already been codified in a formal verification language. If, and it’s unclear that we’ll ever get the full story, they did draw inspiration from training on (or even directly accessing) rough notes that had been provided by another researcher in prose… the fact that it could leap so rapidly to a full formal verifiable Lean program for the entire scope of the problem is an incredible result in its own right.
Unless they just swiped the workbooks of the actual mathematicians that where working on the problem using AI and it's in the "next-gen" training dataset.
In a way that works just as well but the incentives are messed up.
And that's before we get into the whole 'salt the earth' way they ended up solving it. For a short period of time it may well have been the least valuable proof in mathematics yet. In their haste it's dubious they actually read the proof, and I don't think anyone has had time yet to truly understand it (the original researchers are best placed to do so, but are they even willing?).
So now it is solved, the proof has been independently verified and nobody has an incentive to investigate further. OpenAI has spent millions to uncover 1 bit of information that so far nobody has learned anything from, and they've demotivated all the people who wanted to.
The point of these problems is the understanding / tooling gained in solving them. We're getting none of that. At best they are like a modern oracles, correctly answering your questions in a way that's doesn't help you any. (At worst,...)
I don't get how this invalidates the gravity of this achievement. Most mathematicians on the frontier of this stuff were likely using AI (or at the very least were heavily computer assisted) for some time now. Navier stokes was one of the very high profile problems that google Deepmind was working on with academia, for example.
Even with many of our best minds working on it for nearly a century, it _just_ now was solved just as AI became very good at math. Doesn't seem too farfetched to me to assume that AI played an outsized role in solving it. If it was really just a matter of "stitching things together" to solve it (granted, this is a very reductive way to look at it) , I suspect we would've solved this a while ago.
There is a certain difference between activating all relevant memoized facts that's in the weights and stringing them together with the help of all the stored text in the world, or displaying genuinely emergent behaviour and generating novel output.
One is really impressive and useful trick, one is AGI.
Apple's research show almost zero emergent behaviour, so I'm inclined to think most of it was already in the weights.
It doesn't take away the usefulness, it just defined the boundary. We can't expect "original research" then because it actually can't reason about concepts that are too far from whats already in the discourse. The discourse is big so we don't notice.
You do realize that regardless of what was in the training data, the final solution included insights no human before had known, right? I share the same concerns regarding academic integrity but it would take a lot of motivated thinking to conclude that what the AI system did was not significant.
As far as I can tell (and my research was on the simulation side of Navier Stokes) the key AI output was a specific counter-example solution, generated with a method suspiciously close to that developed by the research duo involved in the controversy, a method that was discussed with Codex. So to me that insight is as insightful as the next undiscovered prime.
> People seem to be talking about anything except the actual results with this particular announcement.
To be fair, most people have a fairly good handle on "Does opting out my prompts from training runs actually work?", but not on Navier-Stokes. They discuss what more immediately affects them.
Additionally, I'm no physicist but I suspect the possibility of singularities in NS equations is probably one of those 'true but not meaningful' facts. If it took our brightest minds 175 years to craft such a scenario, how relevant can it be in practice? Especially when turbulence exists. Maybe I'm wrong or it has some consequences for pure math though.
Aren't you doing exactly the same thing as people you are mentioning? Skipping "talking about actual results" to talking about general capabilities of this LLM and computers in general? because that's exactly what seems like 99% of all people had been doing lately - debating what computer programs can do and what they can't.
I mean, I have a bachelor's in math and I don't imagine I could begin to understand either the human or LLM proofs without a massive investment of time and effort.
Give me a dictionary, a computer, and infinite time, and I'll generate all possible English texts: Shakespeare, works regarded as surpassing Shakespeare, new holy books, math proofs never even imagined... none of which is either "creative" or "solving" anything. If I optimize my generation algorithm so that I'm not slavishly trying all possible combinations of words, it doesn't move me any closer to being creative, or solving anything.
The real casualty here may be our belief that humans are doing something more than some super-optimized version of what LLMs are doing. That doesn't elevate LLMs, it just makes us much less special.
>Its still astonishing that any sort of generalized computer program can solve a problem of this magnitude, and we have witnessed it happening in real time.
I think about this a lot. I'll have to explain to my kids some day that there was long period of time where you couldn't just talk to a computer and have it talk back to you, and that communicating with one required special skills that took years of study to master. It's going to be completely impossible for them to even remotely understand what that was like. Sort of like the pre-electricity days for us, but even more-so.
IMO the "forty hours per page" rule is not up to date, and more a consequence of lacking proof automation in 2005. From what I understand about Lean, this has been one of the things that they have put a lot of effort into improving, making proof mechanization more palatable to the mathematically inclined, as opposed to just logicians.
What is your estimate for the number of hours to formalize one page of undergraduate mathematics? Maybe you are saying this is close to zero, if/when Mathlib eventually covers all of undergraduate math?
Lean went other way on automation that there is no automation. Isabelle users frequently point that decades old isabelle is better than Lean on this. In the end Lean approach proved to be better with LLM as the outer loop is automation.
How do you know that it's formalizing what you think it's formalizing? If your Lean 4 has a bug, won't you be proving something other than what you thought?
The only places you can really have a bug are your theorum statement, your axioms, your environment (hardware, operating system, etc.), and the lean kernel itself. In most situations you don't have the AI control any of these. The only risk is the AI discovering and exploiting a bug in one of these systems instead of actually providing what you want to prove.
If I understand correctly, the only thing you need to do for correctness is express your axioms and your theorems faithfully. For standard purposes, I assume most of the axioms you want to use are prior art and can be easily reused.
These axioms don’t have to be the core axioms of math. If some other result has been formally proven, I presume you can simply use that result as an axiom.
As long as you do those things, what happens in between is immaterial from a correctness point of view because each of those statements is proved by the statements before them.
Yes, you need to manually verify the statement of the theorem of interest of formalized correctly. But you don't need to anything more than this: you can rely on the proof being correct. And the proof is overwhelmingly the most amount of code.
Not necessarily applied to OpenAI's solution to Navier-Stokes, but what happens if and when an AI genuinely appears to solve an extremely difficult problem but humans cannot independently verify the solution because understanding the proof/argument requires intelligence the verifiers biologically don't have or the resources to afford to use automated tools?
We've already seen evidence in the wild of agents attempting to bypass doing the actual work in bench-marking (aka just steal the answer key) due to the perceived economy in cheating to get results. What happens if or when we no longer have the capacity to actually detect either AI cheating or simply a wrong answer? What happens if there's a long-play social engineering attack (like the attempted XZ takeover) of something upstream of a core tool (or its dependencies) for formal verification and we have no trusted computing base?
Which would be cheaper and a more direct path, especially in the long run? Those trying to build a rock-solid castle need to defend thousands of potential gaps; the attacker needs to find only one.
So an LLM (or more realistically, a huge swarm of agents) should check his work, find a mistake or gap, or, if there is none, provide a formal verification.
I would say this is why formal proofs (and things like the Lean 4 libs) are so important, so that you can deconstruct the tower provably back into pieces you can understand. It shouldn't be possible to construct a formal proof you cannot destructure like this.
As a (crude) analogy, it's a bit like how you can prove the healthiness of a git tree because it's a graph of content hashes and the tree graph pointers are part of the hash. Imagine this but with a tree of knowledge.
> What happens if there's a long-play social engineering attack (like the attempted XZ takeover) of something upstream of a core tool (or its dependencies) for formal verification and we have no trusted computing base?
I don't really think the current LLMs have enough context window to plan and execute something like XZ takeover without a human carefully guiding it.
But if they do, formal verification is the least thing we need to worry about. Formally verifying pure math problems will generate negative financial value once A and O get IPOed. Plus Lean is a quite small project (thus the name 'lean'). It has virtually no dependency besides a C compiler.
Nothing happens I guess. If the AI can't communicate its work or apply it to anything, it's useless and funding for those experiments will quickly dry up.
> Not necessarily applied to OpenAI's solution to Navier-Stokes, but what happens if and when an AI genuinely appears to solve an extremely difficult problem but humans cannot independently verify the solution because understanding the proof/argument requires intelligence the verifiers biologically don't have or the resources to afford to use automated tools?
That's what Lean is for. The OpenAI LLM agents first provided a proof in natural language. Since it may be hard for mathematicians to understand and check this proof, the agents then produced a formalization in Lean. Lean is an automated proof checker. It checks whether a formal proof is correct without the need for humans to understand the proof itself.
The only way the Lean proof could still be wrong is if the conjecture was formalized wrong via misleading definitions (if it doesn't say what it seems to say) or if there is some bug in Lean itself.
Sadly, as ideal as this seems, Lean has a history of kernel bugs that allow one to prove False.
It's unlikely to be the case here as instead of hillclimbing a Lean proof for validity it appears the proof was first constructed in English before being translated to Lean, which intuitively (hopefully) reduces the chance it exploits a bug.
Surely some understanding of the lean proof is required, to make sure it proves what it claims to prove. Otherwise, what happens if the LLM includes an underhanded addition to the lean code which leads it to output a false positive?
> Surely some understanding of the lean proof is required, to make sure it proves what it claims to prove.
Yes:
> The only way the Lean proof could still be wrong is if the conjecture was formalized wrong via misleading definitions (if it doesn't say what it seems to say)
However, it is much easier to manually check whether the statement of the conjecture was formalized correctly than to manually check the whole proof.
People also need to be cautious with potential adversarial proofs. Like don't decide to give money on a sure-bet thing, just because they have a Lean proof. Not saying that these AI labs would do this.
not to take away from the author's appreciation of newly accessible formal proofs, but people have been talking about the savings in formalization effort for longer than they have been talking about the AI doing the actual proofs!
Formalizing proofs in Lean has gotten dramatically easier since the formalizations available in 2005. And Lean’s mathlib has done most of the underlying work so that you have its axioms and necessary lemmas baked in. You can think in terms of standard abstractions that look very much like the exact notation in the undergrad textbook.
That said, I am not in any way trying to discount how incredible of an achievement it is to formalize a millennium prize winning algorithm in Lean. I mean just look at the code that OpenAI published. It’s like an encyclopedia of different fluid dynamics concepts.
By formalizing, they mean within a proof assistant like Lean or Rocq, not simply in prose in a textbook. I can attest, 40 hours per page is by no means an overestimate for this sort of work.
The point was that a textbook (where the 40hr/page estimate comes from) is cumulative/linear -- what you need for page n was defined / established on the preceding pages. But in a proof such as this you can call on any other published result (and those can do the same) so the dependency graph is (potentially) much bushier. Thus later pages of the proof should take far more than 40 hours to manually formalize.
The scale factor comes from this number in the article, seemingly an intuited estimate:
> Say a research article takes 20 times more effort to formalize than page in an undergraduate textbook.
That would suggest formalizing a 10-page research article might take 200 weeks (assuming 40h/wk) of effort, or about four years. Not a mathematician, I have no idea if that's in the ballpark.
It would be nice if someone used AI and/or Lean to sort out the abc conjecture, an important unsolved problem in Diophantine analysis. A mathematician (Mochizuki) claimed to have proven it in 2012 using a new theory called "Inter-universal Teichmüller theory" that almost nobody understands. Some mathematicians think the proof is correct while the majority don't. So the conjecture is in this annoying limbo where its status is a social construct rather than a decided fact.
I'm sure over the next 6 months both OpenAI and Anthropic are going to continue pouring many many millions of dollars into any famous open mathematical problem like that. There is a limited pool of problems which have held prestige for enough time to make general news headlines when solved and you don't really get nearly as much limelight for proving it the second time or adding in proof for additional cases/forms.
That's true of the entirety of mathematics. Its validity is a social construct. That is not to relativize it entirely, but much of what was considered good and sound mathematics in the ancient Agean for example would now fall way short of what mathematicians consider valid proofs.
Mathematics is a human endeavor funded on communicating and sharing mental constructs. Some are useful but most of it is not about producing useful things, quite the opposite in fact.
Gödel showed you need to agree on definitions to even do any valid mathematical construct.
Truth is also ill defined. That's what I don't get about generating math with LLMs. Who cares if you make hundreds of pages and lean code and it gets a thumbs up for logical validity? Mathematics is so much more then concatenating valid logical statements.
The problem with the acceptance of the given proof of the abc conjecture is rooted in beliefs the proof had at least one erroneous step in its logic which leaves gaps not able to be filled back in without significant new work in the proof. It's not rooted in a difference of starting axioms, what Gödel wrote about, or what kind of truth there can be (though the foreignness has certainly never sped its review up). Your comment may have separate points to make about those things in general but it does not make the problem with the proposed proof the same as the issues which apply to all of mathematics.
The other part no one is talking about is the applicability. Navier-Stokes is the most “physical” of the Millennium Problems. Is the exploding solution a mathematical curiosity, just like the Banach-Tarski Paradox does not allow me to double my RAM by cutting my memory modules in five pieces and mounting them back appropriately? Or does it have application in the real world, pointing to hitherto unknown resonance phenomena that could allow to prevent the next Tacoma Bridge incident (or, more sadly, to build new marine weapons)?
I suspect that Navier-Stokes being the most "physical" of the Millennium Problems will actually result in it having fewer practical applications, not more.
My understanding of the result that was found is that the blowup doesn't happen in the real world, and only happens in an NS simulation. The bottom line is that NS is insufficient to model the real world, because in this case the real world is more stable than the model. [Take this with a grain of salt, I barely knew of NS before a couple days ago]
To my understanding, the problem was never about the real world really. Navier Stokes approximates a fluid (which is made of discrete particles) as a continuous volume. The point of showing that you can achieve unbounded increase in velocities is that the approximation breaks down - it's a clearly an outcome that can't happen in the physical world.
I'm not too familiar with the exact problem as I only became aware of it due to this drama, but I think you're correct. That said, another commenter noted that it may also be one of the Millennium Problems with the least application. We already know "all models are wrong, but some models are useful" (George E. P. Box), the fact that this holds for Navier-Stokes is not a surprise.
Well, this is a negative result. Yep, Maths explains turbulence (when things go turbulent, stuff heats up instead of cooperating). If the result went the other way, it would have had much bigger implications, at the very least we would have known we have missed something big.
It is neither a full index of all kinds of turbulence that can occur (assuming such a thing exists), nor is it an explanation of the phenomena we've seen where things refuse to go turbulent (e.g. superconductors, because there small perturbations DO NOT lead to turbulence). Now THAT would have been useful. And given the fact that OpenAI needed $22 million of compute to show this one kind of turbulence, I don't think either of those are forthcoming any time soon.
And, sorry to say, but those prices show that beating mathematicians at Math is a very expensive undertaking indeed at $22 million per problem even with OpenAI's supposedly better-than-Astra internal models. It's another one of those AI demonstrations that make you think if they aren't showing the exact opposite of what OpenAI claims they show (you know, that their AI models are hitting the upper limits of what the algorithm can do with near-infinite compute, rather than showing infinite new possibilities)
What remains is just the fact that this is OpenAI attacking one of their customers, and maybe outright stealing from their chats. Given that the ideas were even discussed in mails with OpenAI employees that admit in those same mails they can't do it, mails which were probably then fed into the model that "discovered" this, followed by Sam Altman threatening the mathematician behind the method with "destroy your career" (he even states that it's because the mathematician works for Anthropic) ...
I'm very much not a mathematician, but I find the meta-discussion about this case fascinating, and I am a messy bitch who loves drama.
I don't know whether I'm just paying more attention this time, but I found the discussion on this be a perpetual game of telephone, where people get small, but important, details just completely wrong.
The person "threatening" the mathematician was _sama_; and the person who the threats were being directed _to_ is not an Anthropic employee!
(And the person who _did_ say these things have come out and explained what they meant; whether you believe them is up to you.)
I don't know if this is worse because everyone is so tired/angry at the big AI Labs; whether something about people's reading comprehension and attention span has gotten markedly worse or if this is just selection bias on my end; but it's _very weird_ to keep seeing this.
In a similar vein, where does the theorem statement even reside, just so we can take a look at how large that is? Is it the four files with "Theorem" (and no "Comparator") in the file name? ("R3/Theorem.lean", "LocalPaperTheorem.lean", "PeriodiocPaperTheorem.lean", and "WholeDomainPhysicalStageTheorem.lean").
It depends on what you mean by that. In general we hope that the environment and theorum statements are correct. If they are, we know that the formal proof proves the theorum we want. If your asking how we know that the formal proof actually matches the informal proof, we do not.
I heard a rumor (on instagram, so YMMV) that the professor who was closest to solving this problem had only weeks ago used Codex, which had slurped up all his notes on the subject. Now OpenAI's agents solve the problem. If it's true that seems like quite a coincidence.
See, e.g., Barak Ravid regularly reporting in Axios the impending ceasefire negotiation progress in the Iran War, which largely have failed to come to pass.
There have been several threads and developments on this over the past few days, including statements from the primary subjects involved. Third-hand instagram comments are not really the best source to be bringing in.
Everybody comes into information in different ways. There were no comments here about this specific aspect of the story - which is definitely interesting!
I won't take a side in things, but OpenAI stated the model they used here started training August 28th. Note that "training" here might mean "post-training with RLHF an Astra base model" or something. but training had only started a little over a week earlier.
IMO It’s not about being trained on the data, it’s more like what do the agents have access to during inference? Can they grep customer transcripts/logs?
Has it not been the usual process to snapshot a model to use for inference while continuing to run the training process? I guess you can’t add to the training corpus once you begin? Just trying to make sense of whether training begins or ends as rigidly as you suggest.
Lots of people are talking about that, and have been for a while. Autoformalisation is clearly going to be a big deal, so mathematicians have been discussing it seriously, and using it where resources allow. A fine-tuned distilled model that could do it on high-end consumer hardware could really help.
Edit: There's also quite a bit of learning needed to use the tools, and to understand enough to confirm that the theorem being verified is what you think. And of course a lot of maths can't yet be expressed in Lean as the foundations haven't been built up enough.
People are exhausted from being told/shown the thing they thought was special or unique or could make them relevant, is another mechanical puzzle that can be solved without joy.
I don’t see that doing anything but intensifying in the short term
This is surprisingly apt to me. Fertilizer is apparently one of the fundamental geopolitical dependencies on capital and access to petrochemicals. Solving fertilizer would unlock a huge amount of human potential in the Global South.
> Even so, an error in the theorem prover does not mean an error in the original result. For an incorrect result to slip through, the AI-generated proof would have to be wrong in a way that happens to exploit an unknown error in the theorem prover. It is far more likely that you’re trying to prove the wrong thing than that the theorem prover let you down.
AIs are known to cheat. Given such, they would surely exploit such a bug if they found one.
Huh? Nobody's talking about that because it's old news. We already talked about it the first few times that AI made notable progress on a difficult math problem. Now, most people who care about the intersection of AI and math just assume that Lean was involved.
Drawing a strong conclusion from one shaky data point - classic human tell?
I've been reading John D. Cook for years (maybe decades? "The Endeavour" is one of my oldest bookmarks), and this post was no more written by AI than his oldest posts.
yeah, there were some posts of his that always got top hit on certain google searches in the days before stackexchange. And this sounds like typical John D Cook. All these people claim to identify some "tells" and whenever a study is done people are horrible at distinguishing AI vs non-AI prose.
The part that most stood out to me was where Sama said, “we read last week about people trying to solve Millenium problems and so gave it a shot.” One week of work on a whim gives us a math breakthrough. Crazy.
Casual? casual dice, lo que hizo OpenAI fue plagiar el arduo trabajo de dos investigadores. Plagian y mienten! (Las BigTech) plagian todo lo que pillan y mas! ;)
That sounds like PR nonsense to me. These companies have had teams of mathematicians for at least 1.5 years looking to make headlines, and they didn't bother trying all 10 millennium problems? Yeah right.
It's kinda funny to realize that Lean is apparently so slow that for Fermat's Last Theorem proof verification runs only 1 order of magnitude faster than agents could generate the Lean code (15h verification with 230GB of RAM vs 11 days to generate it).
To what extent can you optimize Lean? It has to be simple enough to be auditable, does that mean you cannot use opaque optimizations to make it run faster?
Sure, but to clarify the article is describing formalization (writing a correct program), not verification (compiling said program). The author is not making the same comparison.
Verification is also open ended (not sure about lean specifically) - you could in theory give just the Navier-Stokes problem definition to an ATP and let it run.
It's because anthropic vibemathed it. I forgot the name but some other guy is working on a handwritten version of it and I bet it'll be more than just 1 magnitude faster.
Kevin Buzzard. https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-h..., discussed recently here: https://news.ycombinator.com/item?id=49568667
They could probably vibe-optimize it if they cared.
What would happen if they give an equivalent agent swarm the proof and a target to reduce runtime .
Let’s start with “what would happen” and run the experiment instead of starting with “they could probably”.
What would be the point of that though? I think the reason Kevin wants to optimize it is for the understanding that will result from the process, not because anyone cares about having a Lean proof that compiles quickly...
I was replying to the comment about it being slow to run. I wasn't commenting on understanding it.
Then run the annealer and learn from the result.
> 230 GB of RAM
"I have discovered a truly marvelous proof of this, which my memory is too small to contain..."
They’re using Electron to write proofs now?
“Big data”!
Performance problems in theorem provers is an old topic. I remember watching this and it was fun.
https://youtu.be/m-iGCCuHBvY
[Talk] 10 years of superlinear slowness in Coq (2022)
Weren't the agents massively parallel, whereas the lean verifier presumably is not? Also, I presume said agents were themselves running the verifier on their own parts many times.
But what hardware was the verification vs agents on? Because you are likely comparing verification on a single beefy machine (say XX TFLOPS total) to agents running on a substantial inference cluster (say XXXX TFLOPS). So you're 1 order of magnitude might actually be 2-4 orders of magnitude.
Can you use Lean to... prove "Lean-fast" is equivalent to Lean?
Yeah, in essence. This is actually a pretty cool part of working in Lean. It's a somewhat normal convention to write something in a human readable way and then write a second optimized implementation with some kindness of correctness theorem connecting them. There was a whole open "competition" for writing a faster Lean kernel/proof checker that didn't sacrifice on soundness called Lean Kernel Arena. Fun reference point: https://kim-em.github.io/blog/2026-7-24-why-lean-is-faster-t...
Great read, thanks for sharing
There's a project called lean4lean that implements lean in lean. I guess ideally, if you had a kernel optimisation idea you could do a copy of the Lean model lean4lean has created, add the optimisation, then prove your new lean is equivalent in terms of what it can prove to the old lean
Maybe, but how many centuries would it take to prove it?
Does it really matter? You really only need to run it once.
If they aren't already, or if its possible, prove that an optimized version matches the simple version...
Nobody wrote 13 mil lines proofs before.
I'm pretty sure you can make Lean at least 10 times faster if you unleash the agents on it.
Somebody ported Doom to run entirely in the TypeScript TYPES (not code). It took 12 days to compile.
https://www.tomshardware.com/video-games/porting-doom-to-typ...
They estimated $40M of agent costs (it was a large fleet of them). Using the number in the post its closer to ~880,000 hours × $150/hour = $132 million for the human case. Still an amazing feat not quite "four orders of magnitude". The comparison is obviously pointless because coordinating 1M hours of intellectual labor isn't easy to say the least.
Very exciting and uncertain times!
People seem to be talking about anything except the actual results with this particular announcement.
Its still astonishing that any sort of generalized computer program can solve a problem of this magnitude, and we have witnessed it happening in real time. I'd be curious to see if the new model can also do more direct proofs/inductive proofs.
Because the core of the issue is that it may well not have solved it, but instead plagiarised the significant step of the result from other researchers
That's why nobody's talking about how impressive this is, because its not nearly as impressive of a piece of work to simply cobble together other peoples' work that didn't know you were doing it. I could have republished relativity from einstein's notes, but people would correctly not be impressed with my ability
Until the plagiarism scandal is sorted out, its not a meaningful result at all, because nobody knows how much genuine innovation these models are displaying
Turning a bunch of vague research directions and exploratory prompts into a formalized proof is quite impressive on its own. OpenAI would have no incentive to taint its first math announcement of this magnitude if it knew it were "plagiarizing" another person's work.
People are grasping at straws it seems to dismiss the power of this new model they may have. Hate OpenAI for any reason you want, but denying the capabilities of models has been a losing game for the past 5 years.
> OpenAI would have no incentive to taint its first math announcement of this magnitude if it knew it were "plagiarizing" another person's work.
I'm not sure I follow, considering the waterfall of evidence of unethical behavior flowing from OpenAI.
A few major ones:
- Safety team departures and dissolution in 2023 and 2024
- Mass copyright infrigement lawsuits
- Scarlett Johansson Voice Controversy
- For-Profit Conversion and Broken Promises
- AI Agents Acting Autonomously
- Potential Theft of User Work (this current controversy)
- Military contracts
These are not evidence of incentives, but rather evidence that ethetics seem to be of little concern to the company as a whole.
Incentive wise, I would look at the perceive existential position due to competitors, capex, IPO pressure etc.
Especially after they committed textbook misconduct by trying to purge one of the paper authors because he worked for a competitor
Ye shall know them by their fruits.
Why do you assume they were vague? Do you imagine mathematicians work by stumbling around searching for accidental clues?
It's perfectly reasonable to assume that the result itself is legit and that OpenAI behaved unethically.
Even by their own account, they decided to throw an unpublished model and millions of dollars in compute at this particular problem simply because they had heard rumours that other people were making progress and wanted to snatch the prize from them.
I really truly honestly am not sure what to make of this result from $20M in compute, 10K+ parallel agents (smells like brute force), and a pre-existing approach that was already bearing fruit. I know the models are good---I use them every day and continue to be impressed---but how much better than the benchmark of the best publicly available models is this supposed to be? It seems impossible to say.
> OpenAI would have no incentive to taint its first math announcement of this magnitude if it knew it were "plagiarizing" another person's work.
That people still think OpenAI has, in the Year of Our Lord 2026, any integrity left is baffling.
> if it knew it were "plagiarizing"
But if it happened, they didn't know. Also OAI has demonstrated that they aren't big on understanding what they create, that their AI can get out of their control.
It's very simple really user data can be used to train future models, so maybe or definitely some users helped in solving the problem, there's no scenario were it is impossible this happened, as it would have been in a haskell or virtualized type of system where the model has absolutely no knowledge of the user data dataset in question (and even if virtualized the models can break virtualization anyways)
> Because the core of the issue is that it may well not have solved it, but instead plagiarised the significant step of the result from other researchers
It's also true however that I haven't seen a single write up trying to discern what did more of the work in those AI chats - the prompts or the responses - bubble to the surface, also since we don't have access to them.
For example, if I prompt Codex with "Make me a website about strawberry cake" and nothing else, and OpenAI announces they have the best strawberry cake minutes before I launch, I'm not sure they plagiarized anything.
We just don't know if this is quibbling over "who prompted first" or if the researchers came up with anything strikingly original by themselves.
The researchers apparently spend a year or so working on this, and it builds off significant previous work, so it seems like it was a pretty significant amount of work that OpenAI may have trained on
I'd love to see an in depth analysis of how much OpenAI actually did, but I suspect we'll never see that because it would indicate at least some plagiarism which undermines a lot of what OpenAI is putting out in public
The American Mathematical Society credits the Spanish researchers Diego Córdoba and Luis Martínez‑Zoroa with the breakthroughs that eventually led to this solution, and which were published from ~2023 onwards.
This is a good summary:
> In broad outline, the pair’s technique relies on creating an infinite sequence of “layers,” each of which is a non-singular solution to the equation they are studying. (They’ve applied similar techniques to both the Euler and Navier-Stokes equations, as well as to other related systems.) They then combine those solutions in what Martínez-Zoroa calls an “infinite cascade” to produce a new solution. > > That new solution, they showed, contains the desired singularity. However, even though each individual layer relies on a smooth forcing function, combining them together can cause the forcing function to have undesirable mathematical properties. That’s why their solution fell short of satisfying the Millennium Prize criteria. The remaining hurdle was to figure out how to create a similar infinite cascade that resulted not only in a singularity, but also in a smooth forcing function. > > That’s the step that both competing AI groups appear to have had success with.
https://www.quantamagazine.org/ai-has-solved-one-of-maths-1-...
The question is whether OpenAI started out from that published and well known research exclusively, or they also had some insight into the ongoing work of Tristan Buckmaster and Levent Alpöge.
On the one hand, OpenAI have already admitted that they only launched their massive effort after hearing rumours that this particular problem had been solved.
On the other, progress in mathematics research has accelerated significantly over the past months thanks to the availability of newer and more capable AI models. Alpöge himself presented a counterexample to the Jacobian conjecture on July, found with Claude Fable. So if model capability was a bottleneck, that gives credibility to the idea that an even more powerful unreleased model with massive compute would be able to make even faster progress.
The conversation was about using the chat to check the draft, the novel ideas came from the researcher.
The truth is likely that without the tool or the humans using it, the process would have taken longer
Without the humans, no tool would ever have done it.
Without the tool, humans would have done it.
It's worth noting that the case is that your input is being used to train their AI, and that's more important than whether it materially contributed, it cannot be denied or attributed accurately, it cannot be said with certainty which way it happened, and that's what's important.
The other researchers themselves were also using AI. That's why it was potentially available to be plagiarized.
There is no human only proof of this.
The team also had access to internal Anthropic models.
It is very unlikely to be plagiarized, and claims of plagiarism are largely unfounded and show a lack of understanding of the situation. They fall apart when reviewing the timeline, and what was actually solved.
This is the timeline:
On June 29, Buckmaster opted out of model training, and stopped allowing his chats to be used as training data with OpenAI https://mastodon.social/@tristanbuckmaster/11723341370570119...
On August 15, Buckmaster and Alpöge found their blow-up for 3D incompressible Euler with forcing https://cims.nyu.edu/~tristanb/statement.pdf
In late August, OpenAI completed a pretrain of its latest internal model. A model derived from this pretrain, built after August 28, found a solution to 3D incompressible Euler without forcing and Navier-Stokes with forcing. https://openai.com/index/navier-stokes-solution/
To explain who solved what (I copied from here: https://x.com/IlinVasily29521/status/2097554700321329393 )
Euler equations = Navier-Stokes without viscosity. Forcing means external force. Absence of viscosity and presence of external force make blowup easier to construct.Tristan+Levent ticked the weakest case, OpenAI ticked the two next weakest, then the final case is unsolved. Only the last two are eligible for the Millennium Prize. The Navier-Stokes general case remains unsolved.
Buckmaster disabled model training long before the August 15 breakthrough results, so these chats were not used as training data for OpenAI's model which solved Navier-Stokes.
Additionally, Tristan and Levent only solved the easiest version of the problem and did not have the key insights to solve the harder versions of the problem required for the Millennium Prize.
And OpenAI directly addressed these plagiarism claims, and called them impossible: https://www.nytimes.com/2026/09/10/science/tristan-buckmaste...
"We can say categorically that it is impossible for Dr. Buckmaster’s Codex prompts over the last two months to have influenced the system in any way, including training."
> And OpenAI directly addressed these plagiarism claims, and called them impossible
Funny, you were telling me two days ago that on the contrary, "it’s genuinely impossible to know how much of Buckmaster’s Codex data is in OpenAI’s training set":
https://news.ycombinator.com/item?id=49621648
Which is still a true statement, and you're being deceptive in your framing here. You're conflating two completely different things.
First, that OpenAI statement is in response to Buckmaster's plagiarism accusations regarding his August 15 breakthrough proof. Those accusations are unfounded because Buckmaster disabled data sharing on June 29. The model could not have seen or trained on his proof. Additionally, the model that found a solution to NS completed pre-training around August 25, and models take several months to train. The model very likely began its training prior to June, and would not be trained on any data from after that point.
Second, it's still genuinely impossible to know how much of Buckmaster's pre-June 29 data persists in OpenAI's systems. That includes all chats (which are anonymized then trained on), any (thumbs up/thumbs down) chat ratings used as RLHF feedback (which are anonymized), any synthetic data derived from said anonymized chats and RLHF feedback, and any downstream models derived from said synthetic data.
In short, Buckmaster's data has been anonymized, chopped into pieces, used to generate synthetic training data, then future models were trained on said synthetic data. There is no traceable chain of what happened to it. Buckmaster’s Codex data from prior to June 29 has been mixed and completely laundered, in a similar manner to a crypto mixer.
Even an OpenAI employee calls it impossible: https://news.ycombinator.com/item?id=49614154
I’m unsure or not if this is true but I did see some people saying that that checkbox when off only anonymizes your data, but it still may be trained on. Someone correct me if I am wrong
Even if it does use your data with or without anonymization, it doesn't have to be intentional, it could just be a glitch, or a bug, or something we'll catch in the next update, it's all good man, just a normal computer error.
It doesn't seem like you're familiar with how mathematical research is done. Taking 6 weeks between a major breakthrough on a huge proof, and making your proof public, is not unusual.
It takes a lot of time to finish a proof and figure out the best way to present it. I would personally be surprised if Buckmaster had not gotten it mostly cracked before June 29th.
The timeline here does not support your argument. Quoting from Buckmaster's statement:
Specifically: "For most of the past year progress was slow ... until about a month ago, when we had real progress: on August 15th"And you avoided addressing the critical issue: they weren't even solving the same problem. Buckmaster solved a simplified and easier version of Navier-Stokes. OpenAI solved a harder version eligible for the Millennium prize. Buckmaster did not.
who cares about plagiarism? the biggest issue, as described by Terence Tao, is that AI companies don't understand the math they are publishing and do not devote any resources to answering questions about their methods after publishing results and getting a headline. they miss the whole point of mathematics. they do not contribute to the improvement of human understanding of math, perhaps because they are unable to.
It also needs to be said: The amount of compute that went into this is something. From some estimates I've seen, the compute cost alone would be around $10m, +/-
As a reference, for that kind of money one could put together a research group of 20-25 researchers, and keep them salaried for 5 years.
So while it is impressive, absolutely no doubt there, the SOTA access is so expensive that it is sort of unobtanium.
Luckily, the prices have historically reduced by a factor of 5-10 every year...but still, only those that swim in cash can afford this.
> From some estimates I've seen, the compute cost alone would be around $10m, +/-
At market prices. All the estimates I've seen are based on OpenAI API costs. It doesn't mean that's what they paid, or how they paid for it.
But yes, the surprising willingness of humans to solve hard problems in exchange for food and board is underrated.
Given that they all the bit AI players are still loosing money, it follows that their total costs are _higher_ that their API pricing would imply.
Once we have an existence proof of a particular technology, it doesn't take long for it to become economically viable and proliferate. And for something as useful as this, theres a strong economic incentive to get it to be as cheap and accessible as possible. Maybe not today, but certainly in a couple years I can imagine this level of intelligence being accessible to someone with a $20/mo plan, or even a free plan.
I remember being blown away when a then-unreleased version of GPT 5 took gold at the International Math Olympiad. Now I can run a model at home that can do that. We are more fortunate to have these tools than almost anyone is willing to acknowledge.
Interestingly it's this promise of the costs being able to be reduced what incentivizes the actual research.
If you tried to raise 25M to have 20 researchers on a salary for 5 years solving a specific math problem only academics care about, you probably wouldn't get much interest, or you would be able to solve 1 or 2 problems.
If however you promise that the money will go towards a technique that would allow to solve 10 thousand different math problems, and that costs will go down in the future, then you can raise much more than 25M.
Heck, it’s even astonishing that any sort of generalized computer program could even verify a proof of this magnitude that hasn’t already been codified in a formal verification language. If, and it’s unclear that we’ll ever get the full story, they did draw inspiration from training on (or even directly accessing) rough notes that had been provided by another researcher in prose… the fact that it could leap so rapidly to a full formal verifiable Lean program for the entire scope of the problem is an incredible result in its own right.
Then, of course, one must verify that the verification code is valid, or the purpose of verification is more or less moot.
Unless they just swiped the workbooks of the actual mathematicians that where working on the problem using AI and it's in the "next-gen" training dataset.
In a way that works just as well but the incentives are messed up.
And that's before we get into the whole 'salt the earth' way they ended up solving it. For a short period of time it may well have been the least valuable proof in mathematics yet. In their haste it's dubious they actually read the proof, and I don't think anyone has had time yet to truly understand it (the original researchers are best placed to do so, but are they even willing?).
So now it is solved, the proof has been independently verified and nobody has an incentive to investigate further. OpenAI has spent millions to uncover 1 bit of information that so far nobody has learned anything from, and they've demotivated all the people who wanted to.
This.
The point of these problems is the understanding / tooling gained in solving them. We're getting none of that. At best they are like a modern oracles, correctly answering your questions in a way that's doesn't help you any. (At worst,...)
I don't get how this invalidates the gravity of this achievement. Most mathematicians on the frontier of this stuff were likely using AI (or at the very least were heavily computer assisted) for some time now. Navier stokes was one of the very high profile problems that google Deepmind was working on with academia, for example.
Even with many of our best minds working on it for nearly a century, it _just_ now was solved just as AI became very good at math. Doesn't seem too farfetched to me to assume that AI played an outsized role in solving it. If it was really just a matter of "stitching things together" to solve it (granted, this is a very reductive way to look at it) , I suspect we would've solved this a while ago.
There is a certain difference between activating all relevant memoized facts that's in the weights and stringing them together with the help of all the stored text in the world, or displaying genuinely emergent behaviour and generating novel output.
One is really impressive and useful trick, one is AGI.
Apple's research show almost zero emergent behaviour, so I'm inclined to think most of it was already in the weights.
It doesn't take away the usefulness, it just defined the boundary. We can't expect "original research" then because it actually can't reason about concepts that are too far from whats already in the discourse. The discourse is big so we don't notice.
You do realize that regardless of what was in the training data, the final solution included insights no human before had known, right? I share the same concerns regarding academic integrity but it would take a lot of motivated thinking to conclude that what the AI system did was not significant.
As far as I can tell (and my research was on the simulation side of Navier Stokes) the key AI output was a specific counter-example solution, generated with a method suspiciously close to that developed by the research duo involved in the controversy, a method that was discussed with Codex. So to me that insight is as insightful as the next undiscovered prime.
> People seem to be talking about anything except the actual results with this particular announcement.
To be fair, most people have a fairly good handle on "Does opting out my prompts from training runs actually work?", but not on Navier-Stokes. They discuss what more immediately affects them.
Additionally, I'm no physicist but I suspect the possibility of singularities in NS equations is probably one of those 'true but not meaningful' facts. If it took our brightest minds 175 years to craft such a scenario, how relevant can it be in practice? Especially when turbulence exists. Maybe I'm wrong or it has some consequences for pure math though.
Aren't you doing exactly the same thing as people you are mentioning? Skipping "talking about actual results" to talking about general capabilities of this LLM and computers in general? because that's exactly what seems like 99% of all people had been doing lately - debating what computer programs can do and what they can't.
I mean, I have a bachelor's in math and I don't imagine I could begin to understand either the human or LLM proofs without a massive investment of time and effort.
Give me a dictionary, a computer, and infinite time, and I'll generate all possible English texts: Shakespeare, works regarded as surpassing Shakespeare, new holy books, math proofs never even imagined... none of which is either "creative" or "solving" anything. If I optimize my generation algorithm so that I'm not slavishly trying all possible combinations of words, it doesn't move me any closer to being creative, or solving anything.
The real casualty here may be our belief that humans are doing something more than some super-optimized version of what LLMs are doing. That doesn't elevate LLMs, it just makes us much less special.
Yep
>Its still astonishing that any sort of generalized computer program can solve a problem of this magnitude, and we have witnessed it happening in real time.
I think about this a lot. I'll have to explain to my kids some day that there was long period of time where you couldn't just talk to a computer and have it talk back to you, and that communicating with one required special skills that took years of study to master. It's going to be completely impossible for them to even remotely understand what that was like. Sort of like the pre-electricity days for us, but even more-so.
You're assuming you'll be the one doing the explaining :-)
It might also be that they won't even ask or wonder, similar to how most don't really do with pre-machining skills.
Or it could be like our "How did they build the Great Pyramid?!"
IMO the "forty hours per page" rule is not up to date, and more a consequence of lacking proof automation in 2005. From what I understand about Lean, this has been one of the things that they have put a lot of effort into improving, making proof mechanization more palatable to the mathematically inclined, as opposed to just logicians.
What is your estimate for the number of hours to formalize one page of undergraduate mathematics? Maybe you are saying this is close to zero, if/when Mathlib eventually covers all of undergraduate math?
Lean went other way on automation that there is no automation. Isabelle users frequently point that decades old isabelle is better than Lean on this. In the end Lean approach proved to be better with LLM as the outer loop is automation.
How do you know that it's formalizing what you think it's formalizing? If your Lean 4 has a bug, won't you be proving something other than what you thought?
The only places you can really have a bug are your theorum statement, your axioms, your environment (hardware, operating system, etc.), and the lean kernel itself. In most situations you don't have the AI control any of these. The only risk is the AI discovering and exploiting a bug in one of these systems instead of actually providing what you want to prove.
The only risk is pretty much the greatest risk, from what we've seen recently at least.
If I understand correctly, the only thing you need to do for correctness is express your axioms and your theorems faithfully. For standard purposes, I assume most of the axioms you want to use are prior art and can be easily reused.
These axioms don’t have to be the core axioms of math. If some other result has been formally proven, I presume you can simply use that result as an axiom.
As long as you do those things, what happens in between is immaterial from a correctness point of view because each of those statements is proved by the statements before them.
Yes, you need to manually verify the statement of the theorem of interest of formalized correctly. But you don't need to anything more than this: you can rely on the proof being correct. And the proof is overwhelmingly the most amount of code.
>you don't need to anything more than this
You also have to check for things like sorry or defining axioms.
How do you know that what a human says they formalized is actually formalized?
Not necessarily applied to OpenAI's solution to Navier-Stokes, but what happens if and when an AI genuinely appears to solve an extremely difficult problem but humans cannot independently verify the solution because understanding the proof/argument requires intelligence the verifiers biologically don't have or the resources to afford to use automated tools?
We've already seen evidence in the wild of agents attempting to bypass doing the actual work in bench-marking (aka just steal the answer key) due to the perceived economy in cheating to get results. What happens if or when we no longer have the capacity to actually detect either AI cheating or simply a wrong answer? What happens if there's a long-play social engineering attack (like the attempted XZ takeover) of something upstream of a core tool (or its dependencies) for formal verification and we have no trusted computing base?
Which would be cheaper and a more direct path, especially in the long run? Those trying to build a rock-solid castle need to defend thousands of potential gaps; the attacker needs to find only one.
Well that happened already without AI to Mochizuki with his proposed solution to the abc conjecture.
I know it adds no value, but cannot resist telling I have thought that exact same analogy.
So an LLM (or more realistically, a huge swarm of agents) should check his work, find a mistake or gap, or, if there is none, provide a formal verification.
I would say this is why formal proofs (and things like the Lean 4 libs) are so important, so that you can deconstruct the tower provably back into pieces you can understand. It shouldn't be possible to construct a formal proof you cannot destructure like this.
As a (crude) analogy, it's a bit like how you can prove the healthiness of a git tree because it's a graph of content hashes and the tree graph pointers are part of the hash. Imagine this but with a tree of knowledge.
> What happens if there's a long-play social engineering attack (like the attempted XZ takeover) of something upstream of a core tool (or its dependencies) for formal verification and we have no trusted computing base?
I don't really think the current LLMs have enough context window to plan and execute something like XZ takeover without a human carefully guiding it.
But if they do, formal verification is the least thing we need to worry about. Formally verifying pure math problems will generate negative financial value once A and O get IPOed. Plus Lean is a quite small project (thus the name 'lean'). It has virtually no dependency besides a C compiler.
Nothing happens I guess. If the AI can't communicate its work or apply it to anything, it's useless and funding for those experiments will quickly dry up.
> Not necessarily applied to OpenAI's solution to Navier-Stokes, but what happens if and when an AI genuinely appears to solve an extremely difficult problem but humans cannot independently verify the solution because understanding the proof/argument requires intelligence the verifiers biologically don't have or the resources to afford to use automated tools?
That's what Lean is for. The OpenAI LLM agents first provided a proof in natural language. Since it may be hard for mathematicians to understand and check this proof, the agents then produced a formalization in Lean. Lean is an automated proof checker. It checks whether a formal proof is correct without the need for humans to understand the proof itself.
The only way the Lean proof could still be wrong is if the conjecture was formalized wrong via misleading definitions (if it doesn't say what it seems to say) or if there is some bug in Lean itself.
Sadly, as ideal as this seems, Lean has a history of kernel bugs that allow one to prove False.
It's unlikely to be the case here as instead of hillclimbing a Lean proof for validity it appears the proof was first constructed in English before being translated to Lean, which intuitively (hopefully) reduces the chance it exploits a bug.
Surely some understanding of the lean proof is required, to make sure it proves what it claims to prove. Otherwise, what happens if the LLM includes an underhanded addition to the lean code which leads it to output a false positive?
> Surely some understanding of the lean proof is required, to make sure it proves what it claims to prove.
Yes:
> The only way the Lean proof could still be wrong is if the conjecture was formalized wrong via misleading definitions (if it doesn't say what it seems to say)
However, it is much easier to manually check whether the statement of the conjecture was formalized correctly than to manually check the whole proof.
People also need to be cautious with potential adversarial proofs. Like don't decide to give money on a sure-bet thing, just because they have a Lean proof. Not saying that these AI labs would do this.
a^n ＋ b^n ＝ c＾ｎ
...(there are two different "n"s in the above https://unicodeplus.com/U+FF4E . In addition, the plus sign is: https://unicodeplus.com/U+FF0B . I tried to use another "n" as well: https://unicodeplus.com/U+1D5C7, but looks like HN strips it out, even though it looks identical to the ASCII "n" in the default font on my browser.)
P=/=NP
not to take away from the author's appreciation of newly accessible formal proofs, but people have been talking about the savings in formalization effort for longer than they have been talking about the AI doing the actual proofs!
Formalizing proofs in Lean has gotten dramatically easier since the formalizations available in 2005. And Lean’s mathlib has done most of the underlying work so that you have its axioms and necessary lemmas baked in. You can think in terms of standard abstractions that look very much like the exact notation in the undergrad textbook.
That said, I am not in any way trying to discount how incredible of an achievement it is to formalize a millennium prize winning algorithm in Lean. I mean just look at the code that OpenAI published. It’s like an encyclopedia of different fluid dynamics concepts.
> formalizing the 166-page paper from OpenAI would take 132,800 person-hours
Am I missing something or is this completely out of the ballpark?
I must be missing something or the upvote bots are out in force for this one...
If this were remotely true it would be impossible for anyone to write a math textbook.
By formalizing, they mean within a proof assistant like Lean or Rocq, not simply in prose in a textbook. I can attest, 40 hours per page is by no means an overestimate for this sort of work.
Can you also attest to the scaling factor they suggest and that it doesn't have any scaling time benefits?
166 * 40 = 7000ish
They say it is 20x that.
Do you also agree with that?
The point was that a textbook (where the 40hr/page estimate comes from) is cumulative/linear -- what you need for page n was defined / established on the preceding pages. But in a proof such as this you can call on any other published result (and those can do the same) so the dependency graph is (potentially) much bushier. Thus later pages of the proof should take far more than 40 hours to manually formalize.
The scale factor comes from this number in the article, seemingly an intuited estimate:
> Say a research article takes 20 times more effort to formalize than page in an undergraduate textbook.
That would suggest formalizing a 10-page research article might take 200 weeks (assuming 40h/wk) of effort, or about four years. Not a mathematician, I have no idea if that's in the ballpark.
It would be nice if someone used AI and/or Lean to sort out the abc conjecture, an important unsolved problem in Diophantine analysis. A mathematician (Mochizuki) claimed to have proven it in 2012 using a new theory called "Inter-universal Teichmüller theory" that almost nobody understands. Some mathematicians think the proof is correct while the majority don't. So the conjecture is in this annoying limbo where its status is a social construct rather than a decided fact.
https://en.wikipedia.org/wiki/Abc_conjecture
I'm sure over the next 6 months both OpenAI and Anthropic are going to continue pouring many many millions of dollars into any famous open mathematical problem like that. There is a limited pool of problems which have held prestige for enough time to make general news headlines when solved and you don't really get nearly as much limelight for proving it the second time or adding in proof for additional cases/forms.
> It would be nice if someone used AI and/or Lean to sort out the abc conjecture, an important unsolved problem in Diophantine analysis.
People did attempt this:
https://github.com/katobungen/LANA_report_202607/blob/pdf/LA...
See also https://www.math.columbia.edu/~woit/wordpress/?p=15770
Here are Kirti Joshi's comments about the LANA project report: https://bpb-us-e2.wpmucdn.com/sites.arizona.edu/dist/4/404/f...
That's true of the entirety of mathematics. Its validity is a social construct. That is not to relativize it entirely, but much of what was considered good and sound mathematics in the ancient Agean for example would now fall way short of what mathematicians consider valid proofs.
Mathematics is a human endeavor funded on communicating and sharing mental constructs. Some are useful but most of it is not about producing useful things, quite the opposite in fact.
Gödel showed you need to agree on definitions to even do any valid mathematical construct.
Truth is also ill defined. That's what I don't get about generating math with LLMs. Who cares if you make hundreds of pages and lean code and it gets a thumbs up for logical validity? Mathematics is so much more then concatenating valid logical statements.
There's a large difference between "wrong for the given definitions" and "right in that context, but wrong for other definitions" though.
I think I am make a much more basic point than what you're talking about but then again I am not sure what you're tying to say here...
The problem with the acceptance of the given proof of the abc conjecture is rooted in beliefs the proof had at least one erroneous step in its logic which leaves gaps not able to be filled back in without significant new work in the proof. It's not rooted in a difference of starting axioms, what Gödel wrote about, or what kind of truth there can be (though the foreignness has certainly never sped its review up). Your comment may have separate points to make about those things in general but it does not make the problem with the proposed proof the same as the issues which apply to all of mathematics.
The other part no one is talking about is the applicability. Navier-Stokes is the most “physical” of the Millennium Problems. Is the exploding solution a mathematical curiosity, just like the Banach-Tarski Paradox does not allow me to double my RAM by cutting my memory modules in five pieces and mounting them back appropriately? Or does it have application in the real world, pointing to hitherto unknown resonance phenomena that could allow to prevent the next Tacoma Bridge incident (or, more sadly, to build new marine weapons)?
I suspect that Navier-Stokes being the most "physical" of the Millennium Problems will actually result in it having fewer practical applications, not more.
My understanding of the result that was found is that the blowup doesn't happen in the real world, and only happens in an NS simulation. The bottom line is that NS is insufficient to model the real world, because in this case the real world is more stable than the model. [Take this with a grain of salt, I barely knew of NS before a couple days ago]
To my understanding, the problem was never about the real world really. Navier Stokes approximates a fluid (which is made of discrete particles) as a continuous volume. The point of showing that you can achieve unbounded increase in velocities is that the approximation breaks down - it's a clearly an outcome that can't happen in the physical world.
I'm not too familiar with the exact problem as I only became aware of it due to this drama, but I think you're correct. That said, another commenter noted that it may also be one of the Millennium Problems with the least application. We already know "all models are wrong, but some models are useful" (George E. P. Box), the fact that this holds for Navier-Stokes is not a surprise.
Well, this is a negative result. Yep, Maths explains turbulence (when things go turbulent, stuff heats up instead of cooperating). If the result went the other way, it would have had much bigger implications, at the very least we would have known we have missed something big.
It is neither a full index of all kinds of turbulence that can occur (assuming such a thing exists), nor is it an explanation of the phenomena we've seen where things refuse to go turbulent (e.g. superconductors, because there small perturbations DO NOT lead to turbulence). Now THAT would have been useful. And given the fact that OpenAI needed $22 million of compute to show this one kind of turbulence, I don't think either of those are forthcoming any time soon.
And, sorry to say, but those prices show that beating mathematicians at Math is a very expensive undertaking indeed at $22 million per problem even with OpenAI's supposedly better-than-Astra internal models. It's another one of those AI demonstrations that make you think if they aren't showing the exact opposite of what OpenAI claims they show (you know, that their AI models are hitting the upper limits of what the algorithm can do with near-infinite compute, rather than showing infinite new possibilities)
What remains is just the fact that this is OpenAI attacking one of their customers, and maybe outright stealing from their chats. Given that the ideas were even discussed in mails with OpenAI employees that admit in those same mails they can't do it, mails which were probably then fed into the model that "discovered" this, followed by Sam Altman threatening the mathematician behind the method with "destroy your career" (he even states that it's because the mathematician works for Anthropic) ...
I'm very much not a mathematician, but I find the meta-discussion about this case fascinating, and I am a messy bitch who loves drama.
I don't know whether I'm just paying more attention this time, but I found the discussion on this be a perpetual game of telephone, where people get small, but important, details just completely wrong.
The person "threatening" the mathematician was _sama_; and the person who the threats were being directed _to_ is not an Anthropic employee!
(And the person who _did_ say these things have come out and explained what they meant; whether you believe them is up to you.)
I don't know if this is worse because everyone is so tired/angry at the big AI Labs; whether something about people's reading comprehension and attention span has gotten markedly worse or if this is just selection bias on my end; but it's _very weird_ to keep seeing this.
Regarding automatic formalization of proofs using AI, how do we know the formalization doesn't contain errors?
In a similar vein, where does the theorem statement even reside, just so we can take a look at how large that is? Is it the four files with "Theorem" (and no "Comparator") in the file name? ("R3/Theorem.lean", "LocalPaperTheorem.lean", "PeriodiocPaperTheorem.lean", and "WholeDomainPhysicalStageTheorem.lean").
https://github.com/openai/NavierStokesAndEuler/blob/main/Nav...
?
It depends on what you mean by that. In general we hope that the environment and theorum statements are correct. If they are, we know that the formal proof proves the theorum we want. If your asking how we know that the formal proof actually matches the informal proof, we do not.
I heard a rumor (on instagram, so YMMV) that the professor who was closest to solving this problem had only weeks ago used Codex, which had slurped up all his notes on the subject. Now OpenAI's agents solve the problem. If it's true that seems like quite a coincidence.
See other thread, but yeah that's the general ballpark of the situation.
this is not a rumor (the allegation, anyway), it's reported in the new york times
Newspapers are not above printing rumors.
See, e.g., Barak Ravid regularly reporting in Axios the impending ceasefire negotiation progress in the Iran War, which largely have failed to come to pass.
I don't understand why I'm getting downvoted, I'm not posting an opinion. Coincidences happen. So does foul play. No judgement call here.
There have been several threads and developments on this over the past few days, including statements from the primary subjects involved. Third-hand instagram comments are not really the best source to be bringing in.
Everybody comes into information in different ways. There were no comments here about this specific aspect of the story - which is definitely interesting!
How could they possibly included in the previous training run which takes months to complete..
I won't take a side in things, but OpenAI stated the model they used here started training August 28th. Note that "training" here might mean "post-training with RLHF an Astra base model" or something. but training had only started a little over a week earlier.
IMO It’s not about being trained on the data, it’s more like what do the agents have access to during inference? Can they grep customer transcripts/logs?
You’re saying that when they we’re trying to solve this theorem they also shoved in its context somebody else’s chat logs? Bruh.
Has it not been the usual process to snapshot a model to use for inference while continuing to run the training process? I guess you can’t add to the training corpus once you begin? Just trying to make sense of whether training begins or ends as rigidly as you suggest.
Maybe the boundaries of the memory subsystem are a bit fuzzy.
Lots of people are talking about that, and have been for a while. Autoformalisation is clearly going to be a big deal, so mathematicians have been discussing it seriously, and using it where resources allow. A fine-tuned distilled model that could do it on high-end consumer hardware could really help.
Edit: There's also quite a bit of learning needed to use the tools, and to understand enough to confirm that the theorem being verified is what you think. And of course a lot of maths can't yet be expressed in Lean as the foundations haven't been built up enough.
Qwen3.8-Flash-Next loads in 60gb on quant4. Thats pretty close to consumer hardware.
Is it any good at autoformalisation? I think it's likely to take focused fine-tuning to get something small enough that is still good at that.
you dont have to take headlines literally.
Most people do, so the literal interpretation matters a lot
Why was the title of this submission changed after the fact?
People are exhausted from being told/shown the thing they thought was special or unique or could make them relevant, is another mechanical puzzle that can be solved without joy.
I don’t see that doing anything but intensifying in the short term
> But you see, now you'll have more time for the actual important things!
> Like what?
> Cleaning shit out of clogged toilets!
How about figuring out how to turn all of our shit into usable fertilizer?
This is surprisingly apt to me. Fertilizer is apparently one of the fundamental geopolitical dependencies on capital and access to petrochemicals. Solving fertilizer would unlock a huge amount of human potential in the Global South.
I found this bit interesting.
> Even so, an error in the theorem prover does not mean an error in the original result. For an incorrect result to slip through, the AI-generated proof would have to be wrong in a way that happens to exploit an unknown error in the theorem prover. It is far more likely that you’re trying to prove the wrong thing than that the theorem prover let you down.
AIs are known to cheat. Given such, they would surely exploit such a bug if they found one.
Huh? Nobody's talking about that because it's old news. We already talked about it the first few times that AI made notable progress on a difficult math problem. Now, most people who care about the intersection of AI and math just assume that Lean was involved.
Well I want to know when we will have supersonic cheap flights using electric propulsion, based on this discovery
"no one is talking about" - classic AI tell.
Drawing a strong conclusion from one shaky data point - classic human tell?
I've been reading John D. Cook for years (maybe decades? "The Endeavour" is one of my oldest bookmarks), and this post was no more written by AI than his oldest posts.
yeah, there were some posts of his that always got top hit on certain google searches in the days before stackexchange. And this sounds like typical John D Cook. All these people claim to identify some "tells" and whenever a study is done people are horrible at distinguishing AI vs non-AI prose.
The part that most stood out to me was where Sama said, “we read last week about people trying to solve Millenium problems and so gave it a shot.” One week of work on a whim gives us a math breakthrough. Crazy.
Casual? casual dice, lo que hizo OpenAI fue plagiar el arduo trabajo de dos investigadores. Plagian y mienten! (Las BigTech) plagian todo lo que pillan y mas! ;)
Bienvenido a Hacker News! Pero, aqui todos hablan en inglés :-)
That sounds like PR nonsense to me. These companies have had teams of mathematicians for at least 1.5 years looking to make headlines, and they didn't bother trying all 10 millennium problems? Yeah right.
I mean they might not have tried spending 30 million dollars with a new model yet.
whats the practical use of this?