Lecture series

Frontiers of Mathematics and Computing.

Frontiers of Mathematics and Computing is a lecture series organized jointly by the Department of Mathematics and the newly formed College of Connected Computing at Vanderbilt.

This year the series focuses on AI and mathematics, bringing mathematicians and AI researchers into conversation about how the field will develop in the age of AI. Talks explore themes such as what makes a mathematical problem difficult for large language models, and how AI-written proofs differ from human-written ones.

All talks are at 4:00 pm in Buttrick Hall 102. Beyond the lecture, most speakers also hold office hours for students who want to talk with them; those times will be announced closer to each date.

Upcoming talks

October 26
next talk

Bryan Ward (Vanderbilt University)

Proof checking vs. Proofreading

Time 4:00 pm

Room Buttrick Hall 102

Abstract

Proof checkers such as Lean rigorously verify formally specified mathematical proofs, and their proof-assistant environments help mathematicians build those proofs. These tools establish that a statement is true. This talk presents Proofreader, an agentic LLM tool that acts as a counterexample assistant. Proofreader audits natural-language proofs for flawed logic and searches for counterexamples to theorem statements. The talk covers results from applying Proofreader to a textbook draft and to a corpus of peer-reviewed papers. It also will discuss the strengths and weaknesses of humans and machines, and how proofreading can empower mathematicians even as LLMs become more capable.

November 2

Andrew Wu (Amherst College)

AI-Assisted Automated Reasoning for Safe AI

Time 4:00 pm

Room Buttrick Hall 102

Office hours TBA

Abstract

AI can now generate complex artifacts at remarkable speed, but our ability to build trust in them has not kept pace. Formal verification can provide strong guarantees, yet its scalability often remains a bottleneck. Can AI do for verification what it is already doing for synthesis? In this talk, I will explore different ways of combining AI with automated reasoners to make formal verification more scalable. I will focus on two examples: using lightweight online learning to discover instance-specific strategies for SAT/SMT solving and using large language models to propose intermediate specifications that guide program verifiers through difficult verification tasks.

February 1

Jordan Ellenberg (University of Wisconsin–Madison)

Time 4:00 pm

Room Buttrick Hall 102

Office hours TBA

February 8

Rachel Ward (University of Texas at Austin)

Time 4:00 pm

Room Buttrick Hall 102

Office hours TBA

February 15

Rob Lewis (Brown University)

Time 4:00 pm

Room Buttrick Hall 102

Office hours TBA

March
date TBD

Talia Ringer (University of Illinois Urbana–Champaign)

Time 4:00 pm

Room Buttrick Hall 102

Office hours TBA

Past talks

2026–27

October 19

Pat Shafto (DARPA)

From Axiomatization to Contextualization: The Past and Possible Futures of Mathematics

Room Buttrick Hall 102

Abstract

Recent advances in AI and formal verification have brought machine-generated, machine-checked work to the research frontier of mathematics. These developments are remarkable, but they also expose questions that formal proof alone cannot answer: What should be formalized? Which abstractions are appropriate? How do formal results relate to one another, to mathematical practice, and to the world they are intended to describe? What, in other words, gives mathematics context? I will place this moment within a longer history and suggest new research frontiers in formalization, foundations, the structure and dynamics of mathematical knowledge, formal mathematics across the sciences, and mathematical theories of AI capability and safety.

Speaker bio

Patrick Shafto is Professor of Mathematics and Computer Science at Rutgers University–Newark and Program Manager at DARPA. His research is at the intersection of math and AI. He leads programs at DARPA focused on mathematics of AI (Artificial Intelligence Quantified, AIQ) and on AI and formalization for pure mathematics (Exponentiating Mathematics, expMath).

October 12

Dan Margalit (Vanderbilt University)

No, Math is not Solved

Room Buttrick Hall 102

Abstract

The recent contributions of AI to mathematics research are astounding. At the same time, these advances are seen by many as a threat to the discipline of mathematics. I will argue that, while the human practice of mathematics will change, it will remain as a cornerstone of scientific inquiry and the academic enterprise. I will also outline a vision for how mathematics might adapt to the new era and how we will pave a way for the next generation of mathematicians. There will be ample time and room for questions and conversation.

October 5

Alex Kontorovich (Rutgers University)

Interactions of Formalization, AI, and mathematics

Room Buttrick Hall 102

Abstract

We’ll discuss Lean verification, reliability, and related issues as they pertain to evaluating mathematics produced with/by AI.

September 28

Vasily Ilin (Axiom)

Formalizing All Math

Room Stevenson Center 1206

Abstract

How to formalize all math and why do it? We will attempt to answer this question and discuss the recent progress in mathematical autoformalization.

Speaker bio

Vasily Ilin obtained his PhD in math from the University of Washington in 2026. He founded the UW Math AI Lab and led several AI-for-math projects such as TheoremSearch, TheoremGraph, APRIL, Landau autoformalization, Sorrys are not the hard part, and formalizing numerical analysis. Vasily now works on autoformalization at Axiom Math, where he recently led the effort to obtain the highest position on the LeanEval leaderboard.