AI for Mathematics: Bottom-Up, Top-Down and Meta Mathematics

This talk examines the intersection of artificial intelligence and mathematics, tracing the development from foundational axioms to AI aided conjecture and discovery. It covers bottom-up approaches anchored in Euclid and Principia Mathematica, the shift to formalized proof with Lean and Mathlib, the rise of top-down experimental mathematics guided by computation and data, and the emergent field of meta mathematics driven by large language models. The speaker discusses key milestones, influential figures, and current benchmarks that shape AI assisted mathematical research while emphasizing human–AI collaboration rather than replacement.

Introduction

The presentation from the London Institute of Mathematical Sciences surveys AI's role in mathematics, arguing that AI is poised to change how mathematics is practiced rather than replace mathematicians. It outlines three complementary modes of doing mathematics: bottom-up, top-down, and meta mathematics, and situates these within a broader historical arc from Descartes and Ada Lovelace to modern AI research.

Bottom-Up Mathematics

The speaker begins with Euclid’s Elements as the archetype of building mathematics from axioms, then contrasts this with the 20th century Principia Mathematica project aiming to axiomatize mathematics completely. Gödel’s incompleteness theorem and the Church–Turing framework are discussed as fundamental limits to purely axiomatic programs. The talk then moves to modern computational formalization efforts such as the Lean theorem prover and Mathlib, a project that formalizes vast swaths of undergraduate and some advanced mathematics. The goal is to have machine-checked proofs and, eventually, AI assisted reasoning within a rigorous formal system. The Xena project and Tao’s advocacy for machine assisted proofs are highlighted as pivotal developments that push the field toward scalable formalization.

Top-Down Mathematics

Top-down mathematics emphasizes discovery and conjecture formation, often described as experimental mathematics. The talk traces how mathematicians historically used data and patterns to form conjectures, illustrated by Gauss’s early empirical work on primes and the prime number theorem. It then covers the Clay Millennium Problems, the Birch–Swinnerton-Dyer conjecture, and how early computer experimentation—such as the EPSAC computer at Cambridge—generated conjectures that guided subsequent proofs. The Birch test, conceived as a benchmark for AI assisted mathematical discovery, seeks automatic, interpretable, non-trivial conjectures that can engage human mathematicians. A near miss with a DeepMind collaboration conjecture and a successful but still open elliptic-curve conjecture demonstrate both progress and remaining challenges.

Meta Mathematics

Meta mathematics looks at the role of large language models and other AI tools that operate outside traditional proof systems. The talk highlights recent benchmarks, including the frontier math initiative and IMO style problems where AI systems have achieved notable success. It describes tiered evaluations and open challenges designed to push AI toward genuine mathematical reasoning, including the potential for AI to suggest new problems, not just solve existing ones. The speaker emphasizes ongoing collaboration between mathematicians and AI, with an eye toward establishing trusted, interpretable AI workflows for mathematical research.

Outlook

Throughout, the theme is human–AI collaboration, with AI amplifying mathematical creativity and efficiency while mathematicians provide critical interpretation, structure, and deep theoretical understanding. The talk ends with a call for more AI for mathematics centers and funding to advance formalization and AI-assisted discovery on a scale that complements traditional mathematical practice.