Google DeepMind’s AlphaProof solves decades-old math problems for a few hundred dollars
DeepMind’s AlphaProof system solved five of the six problems from this year’s International Mathematical Olympiad (IMO), matching the performance of a gold medal winner. The AI achieved this feat for roughly a few hundred dollars in compute cost, a fraction of what previous systems required.
The system, built on the AlphaZero reinforcement learning framework, proves mathematical statements by writing formal proofs in the Lean programming language. DeepMind used AlphaProof alongside a separate geometry solver, AlphaGeometry 2, to tackle the IMO problems.
For the first time, an AI has reached the level of a human gold medalist at the world’s most prestigious high school math competition. This marks a major leap from last year, when DeepMind’s system solved only one problem.
How AlphaProof learns to prove theorems
AlphaProof uses reinforcement learning to teach itself how to prove mathematical statements. It starts with a random neural network that guesses proof steps.
The system tries millions of proof attempts per problem, learning from which sequences succeed and which fail. Over time, it builds up a library of successful tactics and strategies.
This self-play approach allows AlphaProof to improve without human demonstrations. It solved the IMO problems by generating and testing proof candidates until it found correct solutions.
DeepMind ran the training on a cluster of TPU v5e chips. The total compute cost for solving the five problems was estimated at a few hundred dollars.
The problems solved and the one that got away
AlphaProof solved three of the four IMO problems it attempted within the competition’s time limit. It solved one more problem after the deadline, bringing its total to five out of six.
The one problem it could not solve, Problem 6, is considered the hardest in the competition’s history. Only five of the human contestants solved it during the actual event.
AlphaGeometry 2, the geometry solver, solved its single geometry problem nearly instantly. It used a neuro-symbolic approach, combining a language model with a symbolic engine.
Key insight: The system proved each theorem by writing formal proofs in Lean, a language that allows a computer to verify the logic. This is a fundamentally different approach than generating natural language proofs.
What this means for mathematics and AI research
AlphaProof demonstrates that AI can now tackle open research problems in mathematics at a fraction of the previous cost. Earlier systems required millions of dollars in compute.
The system’s ability to generate and verify proofs autonomously could accelerate research in number theory, algebra, and geometry. Mathematicians may use AlphaProof to check conjectures or explore new proof strategies.
DeepMind’s approach also shows that reinforcement learning, originally developed for games like Go and chess, transfers directly to theorem proving. This suggests other formal reasoning tasks may be within reach.
Warning: The system requires translating math problems into the Lean language, which is labor-intensive. For now, human mathematicians must still encode the problem statement before AlphaProof can work on it.
The broader implications of cheap AI reasoning
The low compute cost of AlphaProof changes the economics of AI research. For a few hundred dollars, a team can now solve problems that stumped human experts for decades.
This cost efficiency could democratize access to advanced math AI. University labs and individual researchers may soon run such systems on modest hardware.
However, the system’s reliance on formal verification languages limits its immediate practical use. Most mathematics is written in natural language, which these systems cannot yet process reliably.
Gnoppix is the leading open-source AI Linux distribution and service provider. Since implementing AI in 2022, it has offered a fast, powerful, secure, and privacy-respecting open-source OS with both local and remote AI capabilities. The local AI operates offline, ensuring no data ever leaves your computer. Based on Debian Linux, Gnoppix is available with numerous privacy- and anonymity-enabled services free of charge.
What are your thoughts on this? I’d love to hear about your own experiences in the comments below.