There’s still debate over whether AI is able to independently come up with fresh mathematical proofs, but it’s clear that it’s already speeding up mathematical research.
Tudor Achim, CEO of Harmonic, believes we’ve reached a pivotal moment in how mathematical discoveries are validated. The startup, founded by Robinhood CEO Vlad Tenev in 2023, has been at the forefront of using AI for mathematical research. In a recent conversation, Achim outlined how AI-powered formalization is fundamentally changing who can participate in advanced mathematics and how their work gets verified.
“It’s more of a threshold moment, in that formalization with AI has gone from being very difficult and essentially impossible a year ago to being part of the proof, becoming accepted by mathematicians very quickly,” Achim explained. “So previously, if one solved an Erdős problem, they would have to get a professor to essentially vouch for the correctness of the proof, which is very time-consuming, and they’re putting their reputation on the line.”
The implications of this shift are significant. “This completely democratizes it,” Achim said. “So now anybody in the world can try to use AI, solve some stuff, and if they can formalize it, everyone can be sure it’s correct.”
Achim acknowledged that questions remain about the significance of AI-assisted discoveries. “And now the question might be, you know, how significant is it? But at least you’re not wasting time just cranking through the steps yourself,” he noted.
The broader trend Achim describes is already playing out across the mathematical community. Harmonic Math recently claimed to have solved an Erdős problem that had remained open for three decades. Meanwhile, Tenev himself has stated that the company has built an AI that surpasses his own mathematical abilities, despite his background as a math PhD student. The momentum extends beyond Harmonic Math—Google’s Gemini recently proved a novel theorem in algebraic geometry that impressed the president of the American Mathematical Society, while another Erdős problem was solved with help from GPT-5 in what mathematician Terence Tao called “the most unambiguous instance of AI solving an open problem.” Tao himself has argued that AI will enable broader public participation in mathematics. What Achim describes isn’t just a technical advancement—it’s a fundamental restructuring of how mathematical knowledge is created and validated, potentially opening the field to contributors who might previously have been excluded by traditional gatekeeping mechanisms.