OpenAI says an internal model solved ten decades-old open problems in math and theoretical CS

Honestly the doom talk about mathematicians feels off to me. This actually seems like it's bringing math into the mainstream, and I'm genuinely curious to see human mathematicians interpret and contextualize these results. For every conjecture that falls, seven or eight new questions open up, and where we point these tools next is still a human, creative decision.

Given we weren't anywhere near this two years ago, this is really about the speed of change more than anything else.

The chess comparison makes me sick every time. Chess is basically a spectator sport kept alive by a handful of rich eccentrics, and only about 30 players actually make a real living at it. If math goes the same way, what happens to the tens of thousands of non-Fields-medal mathematicians out there?

I see two camps here just like with chess, go, and coding over the last year: the disappointed who lost their edge, and the enthusiastic who are excited for what's next. I'm mostly in the enthusiastic camp for programming but still pretty terrified of the pace.

The chess analogy just doesn't hold up. Chess survives as a human competition where the engine is basically factored out except for training and cheat detection. Translate that to math and all you get is math competitions, not math as a career, since the mathematical universe is way too vast to be cranked out mechanically.

The old way of building career credibility is getting wrecked here. Something like Bill Gates writing a math paper in college used to mean something, now you can't tell if it's AI or human, and it correlates more with who has compute access than who has talent.

Can mathematicians just say no AI PRs, like open source maintainers do when the volume gets out of hand? Feels like every new proof becomes a burden dumped on human reviewers with no way to turn off the hose.

That line about OpenAI taking responsibility for correctness cracks me up. Volunteering to be the fall guy if a Lean proof has a flaw feels a bit rich.

No, the responsibility isn't for bugs inside the Lean kernel itself, it's for correctly translating the human language math into the formal Lean statement.

There are known ways to cheat a Lean proof, like using sorry, so I think they mean they verified none of those tricks were used and the formalized statements actually match the real theorems.

Worth noting a bug in the Lean kernel itself was found last week, where an LLM tricked itself and its handler into thinking it had a non-constructive proof of a Collatz cycle.

I'd like to know the total cost of this research including salaries for the mathematicians and engineers involved, not just the API bill.

The actual number floated is that generating proofs for all 10 results combined cost under $2,000 at Sol API prices, per Noam Brown's tweet.

Sure, employee stock comp makes the real number way bigger, but once the infrastructure and training are done that $2,000 marginal cost isn't very meaningful anymore. Even if AI capability froze right here, this would still be disruptive.

Why even count salary unless the model needed constant babysitting? You'd only tally the hours spent building the harness and checking outputs, since training cost gets amortized elsewhere.

My real complaint is the lack of transparency about the full experiment. I doubt they pointed the model at exactly these 10 problems and got it right in one shot, so that $2,000 figure might be as misleading as p-hacking if they don't disclose how many problems failed and at what cost.

Also curious whether anyone outside OpenAI has replicated anything like this, and whether OpenAI just quietly hired strong combinatorics researchers and the model's role is more incidental than advertised.

I get wanting more rigor, but demanding an RCT for literally everything is a bit much. Some healthy skepticism is fine without turning it into a whole controlled-trial circus.

Don't bring pure cost into this debate. Even if it cost $1 million for these 10 problems, that's roughly 10 to 20 human researchers for a year, and I doubt a team of that size delivers the same results in that time.