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.
> 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
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.
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.
> 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.
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.
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.
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.
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.
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.
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.
>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.
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.
> 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.
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.
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?
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...
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...
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.
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.
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 would really help.
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.
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?
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.
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?
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.
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.
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!
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 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! ;)
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.
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.
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.
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?
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.
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.
> 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
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.
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.
> 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.
> 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.
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.
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.
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.
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.
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.
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.
>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?!"
Yep
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.
> 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.
Well that happened already without AI to Mochizuki with his proposed solution to the abc conjecture.
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.
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?
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 .
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...
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
Maybe, but how many centuries would it take to prove it?
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.
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.
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...
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 would really help.
you dont have to take headlines literally.
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!
Regarding automatic formalization of proofs using AI, how do we know the formalization doesn't contain errors?
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?
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.
[delayed]
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?
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.
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.
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.
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 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.
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.
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! ;)
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.
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 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.
How could they possibly included in the previous training run which takes months to complete..
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?
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.
Maybe the boundaries of the memory subsystem are a bit fuzzy.