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

Syllabus

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

  1. Complete the Natural numbers game by Thursday, Jan 29, and send a screenshot to Kunal.
  2. Prove there are infinitely many primes in Lean before class on Friday, Feb 13. Further instructions on Zulip.
  3. By Friday, Feb 20: Finish the proof of infinitely many primes. Sign up for case studies. Submit a problem statement to Prove2Me.

Schedule

DateTopicNotes/References
Jan 23Overview and Introduction to LeanCode from today
Jan 30FLT project, terms and types in Lean, live demo.FLT Project
Frontier math
Feb 6Types, continued. Proving infinitude of primes in Lean.Kunal's primer on types
David Cheikhi's notes on types
Feb 13Discuss Lean formalization of infinitely many primes. Prove2Me.
Feb 20Overview of Transformers and Attention.
Feb 27Case studies I.Omar Shehab on AI Scaling Laws for Math
Erin Jaen and Matthew Sun on AI-assisted Research
Benny Attar on Math Data for AI.
Mar 6Ethics discussion.Slides
Mar 13Case studies II.Oren Hartstein, Ye Yu, Aaditya Bhaskar Baruah on Formal verification for hardware design
Natnael Mulat, Will Yang, Shuze Chen on Future of Math with AI
Thomas Moulin, Célio Boulay, Alex Chai on AlphaProof and the IMO
Mar 20Spring break
Mar 27Case studies III.
Apr 3Rajesh Jayaram guest lecture.
Apr 10Alex Meiburg guest lecture.
Apr 17Case studies IV.
Apr 24
May 1