AI in Mathematics

AI in mathematics refers to the use of artificial intelligence systems to solve mathematical problems, prove theorems, verify proofs and discover new algorithms. Since 2024, systems built by Google DeepMind and OpenAI have reached medal standards at the International Mathematical Olympiad (IMO) and produced results of interest to research mathematicians.^[1][3]

History

Machine assistance in mathematics has a long history, from computer-assisted proofs such as the four-colour theorem to computer algebra systems. The current wave combines large language models with reinforcement learning and, in some systems, with formal proof assistants that verify every logical step mechanically.^[2]

In January 2024, Google DeepMind published AlphaGeometry, a neuro-symbolic system for olympiad geometry that paired a language model with a symbolic deduction engine. Its successor, AlphaGeometry 2, could solve 83 per cent of historical IMO geometry problems from the previous 25 years, compared with 53 per cent for the first version.^[1] At the IMO 2024 competition, DeepMind's combined system of AlphaProof — which searches for proofs in the Lean theorem prover — and AlphaGeometry 2 solved four of the six problems, including the hardest problem, which only five human contestants solved, for a total of 28 points and silver-medal-level performance.^[1][2]

A year later, at IMO 2025, experimental systems from both OpenAI and Google DeepMind achieved gold-medal-standard scores of 35 points out of 42, each solving five of the six problems in natural language within the 4.5-hour competition limit; neither system solved the sixth problem.^[3][4] DeepMind later published its AlphaProof work in Nature.^[2]

In May 2025, DeepMind announced AlphaEvolve, a Gemini-powered coding agent for algorithm discovery. Among its results, AlphaEvolve found a procedure for multiplying two 4×4 complex-valued matrices using 48 scalar multiplications — the first improvement in 56 years over Strassen's 1969 algorithm in that setting — and proposed optimisations for hardware designs.^[5][6]

Key Concepts and Technology

Two broad approaches are used. Formal systems such as AlphaProof express problems and proofs in a formal language (Lean, with its mathematical library Mathlib) so that every step is machine-checked; because formal training data is scarce, AlphaProof was trained by generating and proving millions of problems in a reinforcement-learning loop. Informal systems, such as the models that reached gold-medal standard in 2025, write proofs directly in natural language, which are then assessed by expert human judges.^[2][3]

Both approaches depend on reinforcement learning and large-scale search. In the formal setting, rewards come from verified proofs — an instance of reinforcement learning with verifiable rewards; in the informal setting, models are trained on large text corpora and refined with reward signals for correct, well-structured reasoning.^[2]

Applications and Impact

Beyond competitions, AI systems are used to assist research: suggesting proof strategies, formalising theorems in Lean, discovering counterexamples and optimising algorithms and hardware. DeepMind reports that AlphaEvolve also improved data-centre scheduling and chip-design problems, and academic groups increasingly use AI tools to explore conjectures and check long proofs.^[5] Risks are also noted: natural-language models can produce plausible but incorrect arguments, and journals and competition organisers have adapted their verification practices in response. The IMO confirmed that the 2025 solutions were complete and correct before results were announced.^[3]

>See Also

• Reasoning Models
• Reinforcement Learning
• AI Benchmarking
• Malaysia AI Talent
• AlphaFold

References