Events

Past Event

(Fun)damental Uses of AI in Math:Formalization and Autoformalization

April 6, 2026
11:30 AM - 1:30 PM
America/New_York
Schapiro CEPSR, 530 W. 120 St., New York, NY 10027 Davis Auditorium (Room 412, 4th Floor)

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.

Contact Information

Data Science Institute