Papers With

← All papers
First page of Mathematicians in the age of AI

Mathematicians in the age of AI

Jeremy Avigad

math.HO Mar 4, 2026 · v3 cs.AI
meta-study ai-agents mathlib
Read PDF arXiv abstract
TL;DR
Essay discussing the Lean/Mathlib formalization of E8 sphere packing, its completion by Math Inc.'s Gauss agent, and the Lean community's response.
Abstract
Recent developments show that AI can prove research-level theorems in mathematics, both formally and informally. This essay urges mathematicians to stay up-to-date with the technology, to consider the ways it will disrupt mathematical practice, and to respond appropriately to the challenges and opportunities we now face.
Problem

AI systems can now prove research-level theorems both informally and formally. This raises questions about how mathematical practice and the profession will change.

Approach

The author is director of the NSF Institute for Computer-Aided Reasoning in Mathematics. He surveys formalization, automated reasoning and machine learning in mathematics, and recounts the collaborative formalization of Viazovska's E8 sphere-packing proof. The formal proof was completed in secret by Math Inc.'s Gauss agent, a case of 'drive-by proving.' The essay then discusses concerns for academic mathematics and gives recommendations.

Results

The essay urges mathematicians to stay current with AI and formal tools such as Lean and Mathlib, to deploy and shape the technology actively, and to adapt teaching while keeping core mathematical understanding.