Chris Kapulkin

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, every speaker also holds office hours for students who want to talk with them; those times will be announced closer to each date.

Upcoming talks

October 12

Dan Margalit (Vanderbilt University)

Time 4:00 pm

Room Buttrick Hall 102

Office hours TBA

October 19

Pat Shafto (DARPA)

Time 4:00 pm

Room Buttrick Hall 102

Office hours TBA

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.

November
date TBD

Boris Hanin (Princeton University)

Time 4:00 pm

Room Buttrick Hall 102

Office hours TBA

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

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.