This course covers the mathematical foundations of machine learning: what can be learned from data, how many samples are needed, and when efficient algorithms exist. Topics include PAC learning, VC theory, boosting, regularization, online learning, and computational hardness. Alongside the theory, students formalize selected theorems in Lean 4 with AI assistance and develop human-readable proof presentations that bridge formal verification and mathematical exposition.
Probability, linear algebra, machine learning, and comfort with proof-based mathematics. No prior Lean experience assumed.
| Date | Topic | Links | |
|---|---|---|---|
| 1 | Apr 1 | No-free-lunch theorem | Slides |
| 2 | Apr 8 | PAC learning, ERM, concentration | |
| 3 | Apr 15 | VC dimension, shattering, growth functions | |
| 4 | Apr 22 | Non-uniform learning, hardness | |
| 5 | Apr 29 | Agnostic learning, neural networks | |
| 6 | May 6 | Compression, AdaBoost | |
| 7 | May 13 | Rademacher complexity, covering numbers | |
| 8 | May 20 | Stability, convex optimization | |
| 9 | May 27 | Online learning, regret, OGD | |
| 10 | Jun 3 | Optimization and synthesis |
CLAUDE.md, AGENTS.md, skills, and other AI artifacts you develop along the way| HW | Topic | Released | Due | Link |
|---|---|---|---|---|
| 1 | TBA | TBA | TBA |
AI use is encouraged in this course — for both assignments and the project. Part of the mathematical training here is learning how to use AI well in the context of rigorous work, which is different from using AI for general writing or coding tasks.
Use AI for learning the material, exploring proof structure when you are unsure how to decompose a theorem, checking candidate proof steps, writing and debugging Lean code, suggesting alternative helper-lemma decompositions, and improving explanation and presentation. A productive pattern is to use AI iteratively: ask for a candidate helper lemma, test it in Lean, and if it fails, ask the AI to explain why the approach did not work.
Develop your AI workflow throughout the quarter. Refine your CLAUDE.md, AGENTS.md, and skills as you learn what works. These artifacts are part of your project deliverables and reflect how your process evolves over the course.
Verification responsibility is yours. A student who asks an AI to generate a complete Lean proof and submits the result without reading it carefully has not learned the theorem. You must stand behind every proof step, every formalization choice, and every explanation you submit.
AI is a collaborator, not an oracle.