AI for Mathematics
XMUM General Elective — April Semester 2026
Instructor: Ma Jiajun · Tuesday 3:00–6:00pm · A4#G11
Week 1: From Counting to AI
Week 2: Dependent Type Theory + LLM Reasoning (coming soon)
Week 3: Reading Proofs in Lean (coming soon)
Week 4: Functional Programming in Lean (coming soon)
Week 5: Prompting and Agent-Based Proving (coming soon)
Week 6: LLM Proof Generation Pipeline (coming soon)
Week 7: Tactics, Metaprogramming, Tools (coming soon)
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)