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 progress in the field, and develop a sense for what lies ahead for the future of mathematics.
Assignments
- Complete the Natural numbers game by Thursday, Jan 29, and send a screenshot to Kunal.
- Prove there are infinitely many primes in Lean before class on Friday, Feb 13. Further instructions on Zulip.
Schedule
| Date | Topic | Notes/References |
|---|---|---|
| Jan 23 | Overview and Introduction to Lean | Code from today |
| Jan 30 | FLT project, terms and types in Lean, live demo. | FLT Project Frontier math |
| Feb 6 | Types, continued. Proving infinitude of primes in Lean. | Kunal's primer on types David Cheikhi's notes on types |
| 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 |