Projects
All 76 Math AI Lab projects by academic quarter.
Fall 2026
14 projects 9 new · 5 returning
AI-Assisted Proof Discovery in Inverse Boundary Problems · Mathematical Taste: Recognizing Progress Beyond Generation · Lean Refactor · Albilich v2: Math Metaharness · and 10 more
Summer 2026
15 projects 8 new · 7 returning
Autoformalizing Mathematical Benchmarks · Improving Mathematical Chain-of-Thought Reasoning of LLMs · Chain-of-Thought Reasoning in Lean 4 · Machine Learning Meets Algebraic Combinatorics 2 · and 11 more
Spring 2026
16 projects 4 new · 12 returning
OpenMath: autoformalizing undergraduate textbooks · LeanGCD: stabilizing Lean generation · Mathematician's copilot: Semantic Theorem Search · Mathematician's copilot: Math2Vec · and 12 more
Winter 2026
14 projects 6 new · 8 returning
Lean error correction with LLMs · Mathematician's copilot: Semantic Theorem Search · Mathematician's copilot: Math2Vec · How good are LLMs at Lean? · and 10 more
Fall 2025
11 projects 9 new · 2 returning
AI for Quantum Code Compilation · Deep learning of number theory · Formalizing Geometric Measure Theory · Formalizing Stacks · and 7 more
Spring 2025
10 projects 6 new · 4 returning
Formalizing Polyhedral Geometry · Reinforcement Learning for Efficient Arithmetic Circuit Generation of Polynomials · Metaprogramming and Writing New Tactics · Neural Theorem Proving · and 6 more
Winter 2025
8 projects 5 new · 3 returning
Formalizing Central Limit Theorem · Examples and Counterexamples in Commutative Algebra · Formalizing Polyhedral Geometry · Metaprogramming and Writing New Tactics · and 4 more
Fall 2024
5 projects 5 new · 0 returning
Formalizing examples and counterexamples in commutative algebra · Metaprogramming and Tactics in Lean · Generating Functions · Central Limit Theorem · Topology for Algebraic Geometry
Winter 2024
4 projects 1 new · 3 returning
FRACTRAN · Continued Fraction Expansion for e · Witt's Cancellation Theorem · Formalizing Math 300
Fall 2023
4 projects 4 new · 0 returning
Continued Fraction Expansion for e · Witt's Cancellation Theorem · Random Graphs · Formalizing Math 300
Spring 2023
9 projects 9 new · 0 returning
Lagrange's Theorem · Abstract term rewriting · Simplicial homology / tactics · Linear algebra · and 5 more
Winter 2023
5 projects 5 new · 0 returning
Identities of the Fibonacci sequence Fₙ · Group theory exercises from Herstein Abstract Algebra · Topology · Commutative algebra · Sequences
Fall 2022
Fall 2022 undergraduate research projects run through WXML.
Spring 2022
The early XLL-era project archive.