Course website
Course schedule, lecture slides, reading lists, and other course material will be posted here.
Course description
Many problems in mathematics and computer science amount to finding a formal object (e.g., a proof, a program, or a combination of both) that satisfies certain verifiable properties. This special topics course surveys AI methods for discovering such objects, the problems these methods have helped solve, as well as the foundational tools grounded in formal methods that let us verify the results with strong guarantees. We will trace several decades of ideas in AI for mathematical and algorithmic discovery, including logic-based methods, automated conjecturing, reinforcement learning for algorithmic problems, LLM-guided evolutionary search (e.g., FunSearch, AlphaEvolve), and recent multi-agent AI systems that have helped resolve long-standing open problems in mathematics. Students will also gain hands-on experience with Lean 4, an interactive theorem prover widely used to verify large-scale mathematical proofs, whether human- or AI-written.
Format. Subject to change.
- 4 homework assignments (8% of the grade each: SAT, Lean, generative models for constructions, evolutionary program search)
- Final project (38%)
- Paper presentation (20%)
- Attendance and participation (10%)
About 5-6 lectures will be given by the instructor, covering technical content. The other lectures will be student presentations on selected research papers. We will give a list of papers at the beginning of the course, and students will sign up to present on a given day. Attending other student presentations will be required and part of the grade will go to engagement with the presentations either during the lecture or on Ed.
Prerequisites: Upper-level course in AI/Machine Learning (e.g., EECS 445/545, CSE 492/592) or equivalent experience. We will assume solid programming experience and comfort with mathematical proofs. Prior exposure to proof assistants (e.g., Lean) is not required.
Readings: Most readings will be research papers. We will also use Theorem Proving in Lean 4 and Mathematics in Lean in the beginning of the course.