OpenAI's AI cracks decade-old math problems, including a major group theory question

Any computable problem will eventually fall to computers.

LLMs have made math proofs more computable, in the sense that a computer can both generate potential solutions and check the validity of its solutions on its own, with a reasonable chance of converging on something correct. I assume this was already doable to some extent, but it seems like it’s now exponentially easier. That still doesn’t mean that all math is automatically solved.

This is somewhat similar to things like molecular dynamics or protein folding or finite element simulations, etc. Some problems that were previously intractable via computation became tractable. Others - the vast majority of other problems - remain unsolvable by these computational techniques, because the scale of compute required is beyond imagination. These are simple things like simulating the dynamics of a cubic millimeter of water molecules for 1 second. Unfathomably beyond current capabilities (and LLMs aren’t going to change that).

I think LLMs are great, I use them every day and I think they have a ton of value. But if these things were as revolutionary as people promote/fear them to be, you should immediately point them at the highest value math problems and see progress. Like the Millenium Prize problems. Haven’t seen a solution to those.

So there are limits - but we’re about to learn a lot about the new normal of what constitutes a layup math proof vs the truly difficult.

Replace philosophers for mathematicians and Douglas Adams was spot on again.

Whilst current models can't 'intuit' and come up with conjectures, they can certainly disprove some of them very quickly through the kind of grind that humans can't do. I suppose there really are some mathematicians out there today, whose last few years of study, have just been up-ended by this.

--

"Yes we are," insisted Majikthise. "We are quite definitely here as representatives of the Amalgamated Union of Philosophers, Sages, Luminaries and Other Thinking Persons, and we want this machine off, and we want it off now!"

"What's the problem?" said Lunkwill.

"I'll tell you what the problem is mate," said Majikthise, "demarcation, that's the problem!"

"We demand," yelled Vroomfondel, "that demarcation may or may not be the problem!"

"You just let the machines get on with the adding up," warned Majikthise, "and we'll take care of the eternal verities thank you very much. You want to check your legal position you do mate. Under law the Quest for Ultimate Truth is quite clearly the inalienable prerogative of your working thinkers. Any bloody machine goes and actually finds it and we're straight out of a job aren't we? I mean what's the use of our sitting up half the night arguing that there may or may not be a God if this machine only goes and gives us his bleeding phone number the next morning?"

Pretty cool. The impact of AI is getting undeniable, there aren’t many positions left to move the goalposts to at this stage, next they’ll have to be outside the stadium entirely.

The sooner people can be broken out of their denial about all this the better, and we can start actually taking it seriously.

problem number 1 and 9 are surprisingly very intuitive

check here :

1. high dimensional sphere packing

https://muchmirul.github.io/conjectures/sphere-packing/

2. multicolor ramsey number

https://muchmirul.github.io/conjectures/multicolor-ramsey

Not being an expert in any of the fields OpenAI has "advanced" I don't want to prematurely downplay the significance of this contribution. However, I am worried that the language they are using in this blog post is exaggerating for the sake of marketing.

It is true there hasn't been a reliable computational approach to solving these problems before. But do these proofs contribute new ideas to the mathematical corpus, or are they simply an effective method to exhaustively search the literature for the right combination of existing tools to apply to the problem?

Essentially, did these problems seem like they had an intuitive answer and were feasible to prove before, just not high enough value targets for an expert to invest time into? Or were they fundamentally difficult prior to this point and it appears that AI has done something more than just throw the problem into a big solver.

The GitHub repo with the Lean formalizations just came out a couple of hours ago: https://github.com/openai/ten-proofs

It also links to a paper written by an LLM where the model "reconstructs how the proof came together" based on the unpublished reasoning traces: https://cdn.openai.com/pdf/reasoning-walkthroughs.pdf

I wish they'd publish the prompts though!

Henry Yuen's (whose work problem 6 builds on) comments on this are worth reading IMO: https://bsky.app/profile/henryyuen.bsky.social/post/3ms2jpch...

one of the early premises of how ai takeoff would go was that a system that could solve open problems in advanced mathematics would also discover novel advances in math and computer science that directly unlock drastically better software performance.

we are seeing frontier level math breakthroughs (ie performance that would put it in the top 100 or 1000 mathematicians in the world if it were a human, meaning top .00001% or 800/8B).

we are also seeing incredible advances in software performance. open ai announced like 15% improvement by fixing gpu kernel issues.

these are clearly linked in the sense of scaling laws and generalization of intelligence: a huge model gets capabilities in both math and software engineering that isn't possible at smaller scales.

but it seems less likely to me than before that the types of math/science discoveries will explicitly unlock better software performance. in some sense this fits our intuitions. when top tech companies use math PhD type employees, they have them stop doing pure math research and instead focus on software engineering. these people are often very good at software engineering but not due to recent discoveries in academic mathematics, it's due to their general intelligence.

to me, this is evidence that the models are getting better but does not make me think we are on the cusp of a foom style fast takeoff enabled by revolutions in frontier math

(i also posted this on twitter @mlipman13)

While these advances are genuinely impressive, I'm curious when we will see practical implications for this work.

For example, will we see advances in material science, medical cures, etc?

Would love to read about some examples of practical impact.