(Fun)damental Uses of AI in Math: Formalization and Autoformalization
Artificial intelligence is beginning to transform how mathematical reasoning is expressed and verified.
As large language models and automated reasoning systems improve, researchers are making rapid progress in both formalizing mathematical arguments and autoformalizing them, converting informal mathematics into formal proof systems at increasing scale. Speakers Alex Kontorovich (Rutgers University) and Henry Yuen (Columbia University) will examine the technical challenges, research opportunities, and broader implications of this shift for both math and AI. The symposium will cover how advances in proof systems, formal methods, and machine learning may reshape the future practice of mathematical research.
This event was part of the Frontiers in Data Science and AI initiative at the Data Science Institute, Columbia University.
Event Details
Monday, April 6, 2026 (11:30 AM - 1:30 PM ET)
Davis Auditorium, CEPSR (4th Floor - Campus Level) - Campus Map
Speakers & Talk Information
Henry Yuen, Srivani Family Associate Professor of Computer Science, Columbia Engineering
Formalization and Autoformalization: Where We Are Today
Abstract: I will give an overview of Lean, a programming language and proof verification assistant, and survey ongoing mathematics formalization projects. I will then survey the latest developments in using AI to automatically formalize research-level mathematics.
Alex Kontorovich, Distinguished Professor, Department of Mathematics, Rutgers University
The Case for Formalization in Research Mathematics
Abstract: We will discuss what doing research math may look like, if/when AI and formalized libraries catch up to the frontier.
Agenda
Monday, April 6, 2026
11:30 AM: Doors Open for Attendees
11:40 AM: Presentation: Henry Yuen, Srivani Family Associate Professor of Computer Science, Columbia Engineering (50 min)
12:30 PM: Break (10 min)
12:40 PM: Presentation: Alex Kontorovich, Distinguished Professor, Department of Mathematics, Rutgers University (50 min)
1:30 PM: Event Ends
DSI Frontiers Awardees: (Fun)damental AI and Math Series
- Ivan Corwin, Professor of Mathematics and Statistics, Arts & Sciences, Columbia University
- Andrew J. Blumberg, Herbert and Florence Irving Professor of Cancer Data Research (in the Herbert and Florence Irving Institute of Cancer Dynamics and in the Herbert Irving Comprehensive Cancer Center) and Professor of Mathematics and Computer Science
- Kriste Krstovski, Associate Research Scientist, Data Science Institute
- Daniel Hsu, Associate Professor of Computer Science, Columbia Engineering