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)