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.
- By Friday, Feb 20: Finish the proof of infinitely many primes. Sign up for case studies. Submit a problem statement to Prove2Me.
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 | Discuss Lean formalization of infinitely many primes. Prove2Me. | |
| Feb 20 | Overview of Transformers and Attention. | |
| Feb 27 | Case studies I. | |
| Mar 6 | Ethics discussion. | Slides |
| Mar 13 | Case studies II. | |
| Mar 20 | Spring break | |
| Mar 27 | Rajesh Jayaram guest lecture. | |
| Apr 3 | Case studies III. | |
| Apr 10 | Alex Meiburg guest lecture. | |
| Apr 17 | Case studies IV. | |
| Apr 24 | ||
| May 1 |