AI had made rapid strides in math in recent times, with several models winning gold at the Math Olympiad, but it now seems to be solving math problems that were unsolved for decades.
Harmonic, a mathematical AI startup founded by Robinhood CEO Vlad Tenev, announced that its reasoning model Aristotle has solved Erdos Problem #124, a conjecture that has remained open for nearly 30 years since it was first posed in a 1995 paper titled “Complete sequences of sets of integer powers” in the journal Acta Arithmetica.
“We are on the cusp of a profound change in the field of mathematics. Vibe proving is here,” Tenev wrote in a post announcing the breakthrough. He added that the problem was solved entirely by Aristotle using a beta version with enhanced reasoning capabilities and a natural language interface.
Erdos problems refer to mathematical conjectures posed by Paul Erdős, one of the most prolific mathematicians of the 20th century who published over 1,500 papers during his lifetime. Erdős was known for formulating problems across various mathematical fields, particularly in number theory, combinatorics, and graph theory. Many of these problems remain unsolved decades after they were first proposed, and solving an Erdos problem is considered a significant achievement in the mathematical community. Erdős often offered monetary prizes for solutions to his problems, with the amount reflecting his assessment of their difficulty.
The achievement marks a significant milestone for Harmonic, which Tenev launched in 2023 with the mission of building mathematical superintelligence. Unlike other AI math systems, Harmonic’s approach centers on formal verification using Lean, a proof assistant that provides machine-checkable guarantees of correctness.
“We want to get really, really good at solving math problems. And the unique spin on it is that we’re using formal mathematics,” Tenev had previously explained. The system translates natural language mathematics into Lean, a formal language that allows every solution to be verified down to foundational axioms, eliminating the need for human mathematicians to manually check the accuracy of outputs.
Earlier this month, Harmonic had announced that Aristotle achieved Gold Medal-level performance at the 2025 International Mathematical Olympiad, generating verifiably correct solutions to five of six problems. The announcement positioned Harmonic alongside tech giants like Google DeepMind and OpenAI, both of which had reported similar gold medal results with their respective models.
Boris Alexeev, who ran the Erdos problem using the beta version of Aristotle, was credited with executing the test that led to the breakthrough.
Tenev expressed confidence that mathematical superintelligence is rapidly approaching and will transform not just mathematics but all fields that depend on it. “Mathematical superintelligence is getting closer by the minute, and I’m confident it will change and dramatically accelerate progress in mathematics and all dependent fields,” he wrote.
Tenev’s claim seemed to be backed up by the person who maintains the Erdos problems website, but with caveats. “This is a nice proof, which was provided by the AI from the formal statement with no human involvement and then formalised in Lean. This is already impressive!” wrote Thomas Bloom on X. “Some caveats though: The solution turns out to be quite easy and short in hindsight, making the problem on the level of the problems in mathematical competitions, where we’ve seen AI have great success. So this should be viewed on a par with this, rather than anything new,” he said.
“There are two different versions of this problem asked by Erdős. The one AI solved is the easier one. The one asked in the original paper is the harder one, which the AI solution (appears to) say nothing about. would not be surprised if the solved problem had in fact appeared in some mathematical competition (perhaps without knowing the Erdős connection), so it could have been part of some training data, and the solution not quite as novel as it seems,” he added.
But Harmonic’s claim, if broadly validated by the mathematical community, would represent one of the first instances of AI independently solving a longstanding open problem in mathematics, potentially signaling a new era where AI systems contribute original mathematical discoveries rather than simply mastering existing problem sets. And even if the problem had somehow been solved elsewhere and was in the AI’s training data, it is still an impressive achievement, showing that AI is already at the very threshold of doing novel research, if it hasn’t already crossed it.