They probably spent more than 3 hours on the failures, which could easily 10x that cost number. Still ridiculously cheap.

Yeah the README on OpenAI/Math says:

“On average, each result used three hours of ChatGPT Pro thinking compute with that model. Over the course of the evaluation, the model was posed approximately 4,000 problems.”

That leaves a lot of ambiguity. Is “result” exclusively “positive result shown here” or “all results”?

Since proving infeasibility is a valuable result, the unpublished problems must not have reached a valuable end state. Thus it’s an operator decision of when to turn the machine off and try another problem. I’d thought they had a three hour time box on this, but apparently not.

As bureaucracies look at AI and staffing, this is going to be the headline in the executive summary.

Sure yeah, today it's only a 5% solution (to the hardest problems), and we know it will top out somewhere.

But the cost reduction is just too good to ignore.

Terry Tao was saying that we need more mathematicians [0]. My paraphrase of his article is that we will need them to check the AIs, essentially (I missed things didn't I?).

But with a near 10,000X reduction in cost [1] today, it's really hard to argue for that when budgets are continuously tight.

[0] https://terrytao.wordpress.com/2026/09/24/were-gonna-need-a-...

[1] assume ~$150k/year for a mathematician of the caliber that can do this work. 2x that for overhead like healthcare, 401k, etc. Do this for 35 years of work = $10,500,000. Assume about 1 result of this caliber per mathematician. So ~$10M per result. OpenAi is saying they can do it for ~$1k, a 10^4 X decrease.

I think it's not just to check - it's to interpret, simplify, apply taste, basically get these proofs into a form that humans can grok and build on. AI could do all of that but the grok-ing -- as we are tapping the font of cheap proofs it still behooves humans to keep track of what we find interesting, keep internalizing and learning concepts and make sure whatever we're building right now will be generationally useful. At least that's my take

Seems similar to what is happening with software developers.

>I think it's not just to check - it's to interpret, simplify, apply taste, basically get these proofs into a form that humans can grok and build on.

Sure, but we are approaching a time at which we will have to answer a "why" here. I.e. anything beyond checking and validation becomes of mostly artistic value at some point. And there is nothing wrong with that.

I’d say the artistic value is the main value in general —- if you know mathematicians they will often refer to a ‘beautiful’ proof, aesthetics is a critical part of math.

An early (easy to understand) proof that fits the bill for me is proof that the sqrt(2) is irrational: a very natural thing to think about —- for a unit square, what is the measure of the diagonal? And people were killed in ancient Greece over the proof, but it’s comprehensible with basic algebra.

IMHO it's groking that allows higher level metaphors and eventually more powerful theories to be built. If all you are doing is proving everything reachable by construction, you aren't really learning, as this process won't be drawn to the more compressed expressions by necessity but only as a "please" from the humans.

> 5% solution (to the hardest problems),

Isn't that more likely the easiest problems in the set? I suppose the hardest problems compared to those that have been solved.

Otherwise your points stand.

If we have a jagged frontier inside the domain of math (very plausible, the jagged frontier concept seems to be quite fractal), the model solved the easier problems in his area of major strenght, some of them will be in the bottom 5% of the easiest problems in the full set, and some in remaining 95% of problems

But all of these proofs are unreadable and seemed to have hallucinated in a bunch of irrelevant stuff, making them not especially useful.

I agree with you.

The problem is getting the funding orgs to care.

You're off by an order of magnitude at least. A mathematician does much more than just prove theorems. Let's start by teaching and administration duties.

And then you're off an order of magnitude of the efficacy of OpenAI. We don't know how much work of mathematicians is behind all these results, what's the real cost (which includes those problems they couldn't solve), etc.

Oh I entirely agree! Mathematicians are full human beings.

But a soulless admin is not.

And they care only about the budget.

And the real danger here is that these large groups of blame avoidance mechanisms take at best half a look at the cost of an AI and the cost of a pre tenure track new assistant professor (or whatever), and they decide, oh maybe next year we can hire someone.

And then they do that again next year.

And then the next

It's "bury the lede" BTW

This comment seems to be a hypercorrection, where someone attempts to demonstrate superior linguistic knowledge by correcting something that isn't actually wrong in the first place. You've likely heard somewhere before, almost certainly on HackerNews in fact, "lede" is proper and "lead" is not but don't really have a genuine understanding of it and are just repeating what you've heard before.

In actuality both "lede" and "lead" are correct. "Lede" is mostly an American and recent respelling of the word "lead" and "lead" still remains the predominantly used term (while "lede" is predominantly an American journalistic spelling).

Language is dynamic and the meaning and spelling of words changes over time.

The expression comes from journalism, hence why lede is preferred. It's something one should not do when writing an article - bury the most important point in the middle of the text.

I heard they used lede to distinguish from (hot) lead. But since linotype has been dead for 50 years this is probably moot now.

Only in American English.

I don't speak en-US (or neighbours) and I'd also say lede.

They share an origin and both work, even if lede is the currently more frequently used one.

https://www.merriam-webster.com/wordplay/bury-the-lede-versu...

It's common in journalism to call to use lead.

This is with the unreleased model, which is probably significantly larger (thus costlier) than astra.

The argument is that it's not tens of $m.

There has been on independent verification. I am certain their Navier-Stokes proof is incorrect.

It provided a formal proof in Lean.

Which is not the same thing that was written in informal prose & their proof has 8k non-computable axioms so you can't even write a program to verify their blowup example is actually a valid instance of a smooth flow that blows up.

> I am certain their Navier-Stokes proof is incorrect.

How much are you willing to bet on this?

Whatever you want, further scrutiny will reveal an error among the noncomputable axioms (8k of them) that were used in the proof.

here you go

https://polymarket.com/event/openai-retracts-navier-stokes-s...

https://polymarket.com/event/openai-retracts-navier-stokes-s...

i hope to hear all about your riches in 2027

Is this a joke? What amount are you betting?

are you a joke? what exactly do these words mean?

> I am certain their Navier-Stokes proof is incorrect.

i at no point said anything so stupid so i'm not betting anything.

I see, so you have no idea if the proof is correct or not & you have no clue how many non-computable axioms are in the lean certificate. Seems like I have wasted enough time here so good luck to you.

i asked you a pretty "computable" question: what exactly do these words mean?

> I am certain their Navier-Stokes proof is incorrect.

Just assume standard semantics & it should make sense.

Sorry I need you to state your axioms here because as I stated above, "standard" semantical interpretation of the word "certain" implies you should be betting lots of money. Since you're not, I have to conclude you have some goofy unorthodox semantical interpretation.

By standard semantics, if you state that believing with certainty that the proof is incorrect is stupid, then you surely believe with certainty that it's correct.

Unless you want the negate the certainty part, but then the nudge to gambling is less coherent.

> By standard semantics, if you state that believing with certainty that the proof is incorrect is stupid, then you surely believe with certainty that it's correct.

you might want to think a little bit harder on this

You're failing to apply de Morgan's laws correctly:

(X and Y) => Z

<=>

~Z => (~X or ~Y)

i think what they are saying is that if you really so certain that the proof is incorrect, you would put on that claim and rest assured that you would win. Especially since the position you are claiming is currently at less than 10%, you stand to win a large amount of money.

The person you are arguing with made no such claim of certainty either one way or the other, so they have no reason to bet anything.

I understood what they were saying but if they're not willing to bet any money then they should refrain from commenting entirely since that seems to be the bar they are setting for others.

> since that seems to be the bar they are setting for others

this is a very simple exercise in propositional logic (simple enough that i don't need to write a lean proof):

"if you are certain then you should bet"

<=>

"if you're not betting then you're not certain"

so i don't have a "bar" and i'm not saying you shouldn't comment, i'm simply calling you a liar.

this argument clearly does not make sense

It can be summed up as ‘put your money where your mouth is’.

Turnabout is fair play.

I think you misunderstood. His mouth was not at "the proof is correct". His mouth was at "you are not really certain that the proof is incorrect". Those two are not the same thing, so flipping the accusation back at him and saying "you should've bet on the proof being correct then" does not actually make any sense.

edit: in other words, if there is anything that he should bet on, it's "the other guy wasn't really certain that the proof is wrong, he is just bloviating". That's a different bet than "the proof is correct".

It's amazing how thick these dudes are <shrug>

"I am 100% sure Microsoft stock will go up 20% tomorrow!"

"i call bs. Why don't you bet your money on it then?"

"well you shouldn't be talking either, you haven't bet money on the stock going down!"

"I am 100% sure Microsoft stock will go up 20% tomorrow!"

"i call bs. Why don't you bet your money on it then?"

"well you shouldn't be talking either, you haven't bet money on the stock going down!"

You also have to count the amount of tokens and human time spent afterward to verify these proofs. There's already been some papers retracted and it seems likely to me that there will be many more as people continue digging into the more dubious ones.

wild.

$8100 doesn't include the negative value of all the knowledge not gained along the way, and perhaps never to be gained in the future, since there is "no reason" to take the road to a known solution.

Many discoveries were made in search of something else.

I'll leave you with this:

"When I woke up just after dawn on September 28, 1928, I certainly didn't plan to revolutionize all medicine by discovering the world's first antibiotic, or bacteria killer. But I suppose that was exactly what I did."

What might we miss out on?

> doesn't include the negative value of all the knowledge not gained along the way, and perhaps never to be gained in the future,

I believe this is the thing many mathematicians are arguing as most people think "AI can do math" and think it doesn't have any downsides. Given the importance of math for science, this has also consequences for scientific and technological advances imo.