Mathematics: the Rise of the Machines
Yang-Hui He
TL;DR
AI for Mathematics investigates how artificial intelligence can aid mathematical discovery along three axes: bottom-up formalization with proof assistants, top-down data-driven conjecturing, and meta-mathematics with large language models. The paper surveys historical context, milestones (Lean/Mathlib, auto-formalization, Ramanujan machine, murmuration conjectures, FrontierMath benchmarks, Birch Test) and presents a concrete vision for AI-assisted proof search and conjecture generation. It argues that AI can accelerate pattern detection, conjecture formulation, and literature/code retrieval while preserving rigor and interpretability, outlining a near-term coevolution of human and AI researchers. The outlook emphasizes staged progress toward a jointly human-AI mathematical enterprise, with auto-formalization and AI-guided proofs as central components rather than full mechanization in the near term.
Abstract
We argue how AI can assist mathematics in three ways: theorem-proving, conjecture formulation, and language processing. Inspired by initial experiments in geometry and theoretical physics in 2017, we summarize how this emerging field has grown over the past years, and show how various machine-learning algorithms can help with pattern detection across disciplines in the mathematical sciences. At the heart is the question how does AI help with theoretical discovery, and the implications for the future of mathematics.