AI for Mathematics

XMUM General Elective — April Semester 2026

Instructor: Ma Jiajun · Tuesday 3:00–6:00pm · A4#G11

• Assignment 1: Proof-Agent Natural-Language Proof

• Week 1: From Counting to AI 📄 PDF
• Session 2: Type theory and Lean 📄 PDF
• Week 3: Constructive Math → Lean in Practice 📄 PDF
• Weeks 4-5: AI for Mathematics — Foundations and Projects 📄 PDF
• Week 5: Building Proof Agents with LLMs and Lean 📄 PDF
• Week 6: Natural-Language Proof Systems 📄 PDF
• Week 7: Lean Deep Dive: Structures, Classes, Induction, Recursion 📄 PDF Lean code
• Week 8: RL for Proof Generation + Benchmarks (coming soon)
• Week 9: Pattern Mining and Discovery (coming soon)
• Week 10: Literature Search and Knowledge Extraction (coming soon)
• Week 11: Conjecture Generation + Case Studies (coming soon)
• Week 12: Project Guidance (coming soon)
• Week 13: Student Presentations (coming soon)
• Week 14: Student Presentations + Summary (coming soon)