COMS 6998: Machine Assisted Mathematics
Spring 2026
Course Number: COMS 6998
Date/Time: F 10:10am - 12:00pm
Room: CEPSR 415
First meeting: January 23, 2026
Description
This class will explore contemporary developments in machine-assisted mathematics. Topics include: the Lean proof assistant/interactive theorem prover, other infrastructure and tools for computer-assisted mathematics, AI for autoformalization, theorem proving, and other forms of mathematical discovery. The goal of the class is to explore the latest developments in this field, and develop a sense for what lies ahead for the future of mathematics.
Schedule
| Date | Topic | Notes/References |
|---|---|---|
| Jan 23 | ||
| Jan 30 | ||
| Feb 6 | ||
| Feb 13 | ||
| Feb 20 | ||
| Feb 27 | ||
| Mar 6 | ||
| Mar 13 | ||
| Mar 20 | Spring break | |
| Mar 27 | ||
| Apr 3 | ||
| Apr 10 | ||
| Apr 17 | ||
| Apr 24 | ||
| May 1 |