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 is part of the Frontiers in Data Science and AI initiative at the Data Science Institute, Columbia University.

REGISTER

REGISTRATION DEADLINE: The Columbia Morningside campus is open to the Columbia community. If you do not have an active CUID, the deadline to register is at 12:00 PM the day before the event.

Event Details

Monday, April 6, 2026 (11:30 AM – 1:30 PM ET)

Location: Davis Auditorium (CEPSR) – 4th Floor (Campus Level)
Address: 530 W 120th St, New York, NY 10027

· · ─ · ─ · ·

11:30 AM: Doors Open for Attendees

11:40 AM – 12:30 PM: Presentation: Henry Yuen, Srivani Family Associate Professor of Computer Science, Columbia Engineering (50 min)

  • Talk: Formalization and Autoformalization: Where We Are Today

12:30 PM – 12:40 PM: Break (10 min)

12:40 PM – 1:30 PM: Presentation: Alex Kontorovich, Distinguished Professor, Department of Mathematics, Rutgers University (50 min)

  • Talk: The Case for Formalization in Research Mathematics

1:30 PM: Event Ends

Speaker Details

DSI Frontiers Awardee: Ivan Corwin
Professor of Mathematics and Statistics, Arts & Sciences, Columbia University

Henry Yuen
Srivani Family Associate Professor of Computer Science, Columbia Engineering

Talk: 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

Talk: 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.

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