Tudor Achim, CEO at Harmonic, discusses how AI is rapidly advancing in mathematics, from solving Olympiad problems to tackling open research problems like the Erdős problems. He explains the concept of mathematical superintelligence (MSI) and how formally verified math in languages like Lean ensures correctness, transforming collaboration and trust.
Summarized by Podsumo
AI achieved gold at the International Math Olympiad (IMO) in 2024, a milestone for formal reasoning.
AI is exceptionally good at finding counterexamples to conjectures, as it can relentlessly explore possibilities without tiring.
The use of Lean, a programming language for formally verified math, is a phase transition away from imprecise human language proofs.
Math has infinite demand, and AI progress will lead to solving long-standing problems like unifying quantum mechanics and general relativity.
Training models on formally verified math improves their general reasoning abilities due to the high signal-to-noise ratio.
"AI seems to be really weirdly good at cranking and cranking where a human might just falter and say, 'I'm too tired to prove this right now. I'm gonna go get a coffee.'"
— Tudor Achim
"We define a math superintelligence as an AI system that can do math at a higher level than the sum total of all humans."
— Tudor Achim
"The most important thing mathematicians do besides solving problems is posing the problems."
— Tudor Achim