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

The talk surveys how artificial intelligence is changing mathematics through three intertwined paths: bottom-up, top-down, and meta mathematics. It traces a history from Descartes and Ada Lovelace to modern AI, explains how formal libraries like Lean's Mathlib enable machine-verified proofs, and discusses AI-driven conjecture formation via the Birch test. It also explores the role of large language models in mathematical discovery and the frontier math benchmarks that push research beyond traditional boundaries. Rich with personal anecdotes and historical milestones, the talk offers a nuanced view of both the promise and the limits of AI in mathematics.

Overview

This talk examines how artificial intelligence is reshaping mathematics, proposing a threefold framework: bottom-up, top-down, and meta mathematics. It blends historical context with current initiatives to show how AI can assist mathematicians without replacing them.

Bottom-Up Mathematics

Bottom-up mathematics builds from axioms to complex theorems. The speaker traces this tradition from Euclid to the 20th century foundations, then moves to modern implementations in computer proof systems, notably Lean and the Mathlib library. The Mathlib Lean project is described as a modern reimagining of Principia Mathematica, formalizing undergraduate mathematics and beyond. The Xena project demonstrates progress in axiomatizing mathematics on computers, capturing thousands of pages of definitions and proofs. This section emphasizes the necessity of machine-checked proofs for ensuring logical consistency in a mature mathematical literature.

Top-Down Mathematics

Top-down mathematics focuses on discovery, pattern recognition, and conjecture. The Birch test is introduced as a stringent criterion for AI-assisted mathematical discovery: automatic, interpretable, and non-trivial. The talk surveys notable near-misses and near-successes, including AI-generated conjectures related to elliptic curves and BSD conjectures, highlighting how data-driven approaches can inspire human mathematicians to pursue new questions.

Meta Mathematics

Meta mathematics centers on large language models and AI systems that operate beyond traditional proofs. The speaker discusses frontier math benchmarks for IMO-level problems and research-level questions, showing how AI can tackle complex, precise problems and even propose new lines of inquiry. The tiered Frontier Math program and the Epoch AI initiative illustrate the current state and future potential for AI in high-level mathematical reasoning and discovery.

Personal Journey and Implications

The speaker shares how parenthood spurred an entry into machine learning, culminating in influential papers and textbooks on AI for pure mathematics. The discussion covers the balance between mathematical rigor and AI-assisted exploration, the role of funding and institutional support, and the evolving landscape of how mathematicians collaborate with machines.

Future Outlook

Concluding with a call for robust, trusted AI-enabled mathematical tools, the talk emphasizes collaboration between human creativity and machine precision, and urges sustained investment in AI for mathematics research and education.