Abstract: For most of its history, mathematics has been informal: proofs are written in natural language to convince human experts. This process has served us well -- but as AI begins to generate persuasive mathematical text, it becomes harder to tell genuine insight from convincing error.

Formal verification offers a foundation for trust. These tools, first built for verifying hardware and software, now reach deep into research mathematics through projects like Mathlib.

Formalization and AI together hold great promise for mathematicians: verified automation of routine reasoning, new connections between disparate areas, and trustworthy collaboration and exploration. I will outline the current state and discuss ongoing efforts to help realize this vision.

Bio: Matthew Robert Ballard is Professor of Mathematics at the University of South Carolina and Associate Director at the Institute for Computer-Aided Reasoning in Mathematics. A Fellow of the American Mathematical Society, Ballard is also a maintainer of Mathlib, the library of formalized mathematics in Lean. He received his Ph.D. from the University of Washington in 2008.