Winter 2026 Math AI Lab Projects

Project teams meet Mondays and Wednesdays from 4–5:30 pm in Denny Hall 303.
Lean Together meets Fridays 3:30–6 pm in CMU B-006.

The goal of projects is a publication or a significant open-source contribution, e.g. to mathlib4. Students are expected to commit at least 5 hours per week to their project outside of meeting times.

Autoformalization Projects

The goal of autoformalization projects is to use Lean-specific AI assistants such as Harmonic’s Aristotle to formalize large chunks of mathematics, and contribute to mathlib4.

Geometric Measure Theory

• Project Leader: Ignacio Tejeda
• Formalization target: Theorem 4.2 in Falconer’s Geometry of Fractal Sets.
• Code: GitHub repo
• Mathlib PRs: 1, 2
• Members: Theo Meek, Nathan Pao, Annie Cao, Josh
• Prerequisites: Lean

Commutative Algebra

• Project Leaders: Haoming Ning and Leo Mayer
• Formalization target: The theorem that a regular local ring is a UFD, referred by some as the Auslander-Buchsbaum theorem. See Stacks Project 0AG0.
• Members: Nailin Guan, Dora Kassabova
• Prerequisites: Lean

Algebraic Geometry

• Project Leaders: Bianca Viray and Bryan Boehnke
• Formalization target: Monogenic extensions of regular local rings following arXiv:2503.07846, lemmas 3.1 and 3.2.
• Members: George Peykanu, Grant Yang
• Prerequisites: Lean

Category Theory

• Project Leader: Nelson Niu
• Formalization target: Nelson Niu & David Spivak’s Polynomial Functors textbook.
• Members: Sukhman Singh
• Prerequisites: Lean

Formalization: zero-knowledge proofs

• Project Leaders: Eric Klavins and Alexandra Aiello
• Description: We would outline a framework for verifying mathematical theorems while keeping the respective proofs secret by leveraging dependent combinatory logic as a host language for Zero-Knowledge (ZK) proof circuits. Specifically, we would interpret the axioms of the dependent SK combinator calculus as a universal ZK circuit capable of checking mathematical proofs encodeable in the calculus. We would target ZK-STARKs as our ideal ZK scheme, enabling quantum resistance of the proofs without trusted setup [Ben+18]. This would be a first-of-its kind result, with wide applications. Goal: publication
• Prerequisites: Lean, type theory

Metaprogramming: Provable Computation in Lean

• Project Leader: Dhruv Bhatia
• Description: While Lean has seen extensive use as a theorem-proving assistant, its capabilities as a computational programming language have been underutilized. The goal of this project is to begin filling that gap. Along the way, we will learn the basics of functional programming, monads, and Lean’s metaprogramming framework to implement algorithms that can both be run efficiently and be reasoned about. Our main goal is to implement basic algorithms with applications to linear algebra while also proving (in Lean) correctness of said algorithms.
• Members: Joseph Qian, Junye Ji, Veer Shukla, Alan Chang
• Code: GitHub repo

AI Projects

The goal of AI projects is to use AI and ML to advance mathematical research. For example, by helping mathematicians find relevant theorems, or by training models to learn mathematical functions or by creating math-specific datasets or models. AI projects are expected to result in a publication in a submission to a major ML conference such as ICML, ICLR, EMNLP or Neurips.

Lean error correction with LLMs

• Project Leader: Vasily Ilin
• Description: Fine-tune LLMs to correct Lean errors, using compiler feedback. Create a diverse dataset of errors and train on it. Submit to ICML 2026 in January.
• Members: Evan Wang, Simon Chess, Daniel Lee, Siyuan Ge, Ajit Mallavarapu
• Code: GitHub repo

Mathematician's copilot: Semantic Theorem Search

• Project Leaders: Giovanni Inchiostro and Vasily Ilin
• Description: We help research mathematicians find relevant theorems quickly. We collected the dataset of all theorems on ArXiv, Stacks Project and other sources, and built vectorized search over it. Goal: submit to ICML 2026 in January.
• Demo: HF link
• Members: Eric Leonen, Sophie Szeto, Artemii Remizov, Luke Alexander
• Code: GitHub repo

Mathematician's copilot: Math2Vec

• Project Leader: Henry Kvinge (PNNL)
• Members: Saharsh Bhargava, Cecilia, Jiahe Lu, Michael, Kedar Chintalapati, Rachit Jaiswal, Samarth Rao, Jared Darlington, Leo Carlin
• Description: Train a text embedder that understands math, LaTeX and Lean. This will improve search over Lean, and natural language theorem search. It can be used for RAG as well. Use arXiv, MathOverflow, mathlib, Lean Reservoir, and possibly other sources. Create an evaluation benchmark as well. Goal: submit to EMNLP 2026 in May.

CayleyPy: search on massive combinatorial graphs

• Project Leaders: TBD
• Description: Optimize CayleyPy, make a CLI, and use it on various combinatorial problems, such as estimating diameters of symmetric groups. Goal: submission to ICLR 2027 in September. See project proposal document.
• Members: Danny Zhang, Gaurang Pendharkar, Merav Frank, Sambhu Ganesan, Xiaoxing Zhang
• Prerequisites: solid Python, some group theory or combinatorics.

Reinforcement Learning for Polynomials

• Project Leader: Michael Zeng
• Description: Use RL to find efficient arithmetic circuits for polynomials.
• Members: Kyle Zhang, Rohan Pandey, Naomi Morato
• Code: GitHub repo

AI for Quantum Code Compilation

• Project Leader: Andres Paz
• Description: Quantum error correction (QEC) codes are traditionally described using stabilizers, which define the subspace preserved by the code. However, implementing these codes requires translating stabilizers into fault-tolerant quantum circuits—an inherently nontrivial task that depends on the constraints and capabilities of the underlying hardware architecture.
  
  This project aims to develop an AI agent capable of synthesizing such circuits in a way that:
  1. In the ideal (noiseless) setting, the resulting circuits implement the intended stabilizer structure of the code on the target architecture.
  2. In the noisy setting, the agent searches over circuit variations to optimize fidelity, taking into account realistic noise models and architectural constraints.
  The outcome would be a toolchain bridging the gap between abstract QEC code design and concrete, high-performance circuit implementations, enabling better exploration of architecture-specific tradeoffs in fault-tolerant quantum computing.
• Members: Christian Tarta, Sylvie Lausier, Mayee Sun, Sarju Patel

How good are LLMs at Lean?

• Project Leader: Tyson Klingner
• Description: Design an evaluation procedure for various Lean tasks such as next step generation or entire proof generation. Run our algorithms on frontier models to see which LLMs perform the best, providing guidance to the Lean community on which LLMs to use. Use a scalable architecture so that our algorithms can be rerun when new models are released.
• Members: Escher Crawford, Drew Bladek

Deep learning for number theory

• Project Leader: Junaid Hasan
• Description: The goal is to explore to what extent modern machine learning algorithms (e.g., feedforward neural networks, transformers, LLMs) can learn number-theoretic functions such as modular arithmetic, the Möbius function, or gcd. We can first attempt to replicate results from the literature (arXiv:2502.10335, arXiv:2308.15594) and then explore our own functions and algorithms. We aim to submit to one of the major ML conferences such as ICML or ICLR.
• Prerequisites: Python (must have), ML experience (desired)
• Members: Hemkesh Bandi, Akhil Srinivasan, Andrew Chen, Nina Tharamal, Claire Xu
• Code: GitHub repo