OpenAI's Astra Solves Ten Long-Standing Problems in Mathematics and Computer Science
Ten advances in mathematics and theoretical computer science
We recently used our internal Astra model to solve ten major open problems in mathematics and theoretical computer science that had seen no progress for over a decade. These breakthroughs span fields like high-dimensional geometry, quantum complexity, and lattice cryptography. We have formalized these proofs in Lean and released the model's reasoning process, while committing to honest attribution and deep engagement with the mathematical community.
Claiming human authorship for a proof generated entirely by an AI system would misrepresent both the system's contribution and the nature of genuine human intellectual work.
- aabhay
My main gripe here is the lack of transparency around the total experiment and construction. I doubt that they simply pointed their model at these ten specific problems alone and gave the model one shot; therefore the $2000 number could be completely misleading, similar to P-value hacking by not disclosing the total experimental setup.
I want to know:
1. How many total problems were given to the model, and what percent were left unsolved at what cost before giving up?
2. How many attempts did you give the model at solving these problems?
3. How expensive was the harness, e.g. did the model have access to a job cluster?
- robinhouston
In a way the most remarkable thing about this is that it isn't even at the top of the HN homepage. Even if this is a step up from what we've seen before, we're no longer astonished by the idea that AI can make significant advances in mathematics and computer science.
- Chance-Device
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.
- ultimatefan1
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)
- kcexn
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.
- simonw
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!
- maxutility
New advances in sphere packing? Let’s make sure AI doesn’t inadvertently engineer ice-9.
- randomizedalgs
After skimming some of the writeups, I'm surprised that the frontier internal model still writes just as poorly as Sol.
Maybe good AI paper writing is further away than I thought...
- DrBazza
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?"
- artninja1988
Now that we've seen AI produce a fair number of proofs (and disproofs), I'm curious when we'll start seeing it build genuinely novel theory. Does anyone have predictions on when and how we'll get there and will it take new architectures/ training paradigms, or is the current approach enough?