Lecture series
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 Stevenson Center 1206. 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.
2026–27 talks
Formalizing All Math
How to formalize all math and why do it? We will attempt to answer this question and discuss the recent progress in mathematical autoformalization.
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.