AI Agents for Mathematicians: A Practical Guide to Proof, Computation, and Discovery

Mathematics has always advanced with instruments — tables and calculators, computers and computer algebra systems — and the instrument of our moment is the AI agent: a system that can read mathematics, propose and search for proofs, compute and explore, surface conjectures, and even, in narrow but real ways, discover results no human had found.

AI Agents for Mathematicians is a practical, code-first guide to working with that instrument well. It is written for the mathematician — researcher, graduate student, or teacher — who wants to understand what agents can and cannot do, and to use them with craft rather than credulity. It assumes mathematical maturity but no prior experience with AI tools.

Running through every chapter is a single conviction: an agent is a fallible generator made safe and useful only by verification — absolute where a proof assistant’s kernel provides it, disciplined and graduated where it cannot — and the understanding, judgement, and responsibility that verification serves remain irreducibly human. An agent can propose, compute, and search; it cannot comprehend, and comprehension is what mathematics is for.

The book runs to 12 chapters in four parts — Foundations; Computation and Exploration; Proof; and Practice and Future — with worked code listings in Python (SymPy, mpmath) and the Lean proof assistant, clear figures of every key mechanism, and “In Practice” case studies drawn from real, documented milestones and checked against their primary sources: the Bailey–Borwein–Plouffe formula, the Ramanujan Machine, zbMATH Open, the Flyspeck formalization of the Kepler conjecture, AlphaProof at the International Mathematical Olympiad, FrontierMath, the Polynomial Freiman–Ruzsa formalization with Blueprint, Khanmigo and Bloom’s two-sigma problem, and FunSearch’s genuinely new discoveries.

Readers will learn to talk mathematics to a machine and avoid the statement-correctness trap; drive computer algebra and high-precision numerics and place every result on a trust hierarchy; generate and stress-test conjectures; ground literature search in real sources and catch hallucinated citations; understand proof assistants and the trusted kernel; use agents to autoformalize and search for proofs, and verify what they produce; and build research and teaching workflows around agents without bypassing understanding.

The tools of this discipline will change beyond anyone’s predicting; the fundamentals it rests on — proposing freely, verifying relentlessly, and keeping the understanding one’s own — will not. Those fundamentals are the real subject of this book. Part of The Practical Guide Series.