Math AI Lab University of Washington
Summer 2026

Summer 2026 Projects

All projects
theorem mgf_of_iid
{Y : ℕ → Ω → ℝ}
{Z : ℕ → Ω → ℝ}
(h_meas : ∀ (i : ℕ), Measurable (Y i))
(h_indep : ProbabilityTheory.iIndepFun (fun (i : ℕ) => inferInstance) Y μ)
(hident : ∀ (i j : ℕ), ProbabilityTheory.IdentDistrib (Y i) (Y j) μ μ)
(Z_def : ∀ n : ℕ, Z n = (Real.sqrt n)⁻¹ • (∑ i ∈ Finset.range n, Y i)) :
  ∀ n : ℕ, n > 0 →
    ∀ t : ℝ, mgf (Z n) μ t = (mgf (Y 0) μ ((√n)⁻¹ * t)) ^ n := by
  intro n hn t
  rw [Z_def]
  rw [ProbabilityTheory.mgf_smul_left]
Source: uw-math-ai/central_limit_theorem, CentralLimitTheorem/main.lean

Summer 2026 brings nine new projects alongside six returning projects from Spring. Together, the teams span autoformalization, AI and machine learning for math, autoresearch, and AI-supported mathematics learning.

The goal of projects is a publication or a significant open-source contribution, e.g. to mathlib4.

New Projects

These nine projects are launching in Summer 2026 across four areas: autoformalization, AI and machine learning for math, autoresearch, and AI for math learning and education.

Autoformalizing Mathematical Benchmarks

  • Area: Autoformalization
  • Project Leader: Theodore Meek
  • Members: Michael R. Zeng, Pei Li
  • Description: Formalize research-level conjectures from LemmaBench and OpenConjecture using a simple agentic workflow in which AI agents check and refine one another's work. Every resulting statement will also receive human review and be classified as faithful, uncertain, or unfaithful, producing a useful benchmark with clear quality signals.

Improving Mathematical Chain-of-Thought Reasoning of LLMs

  • Area: AI and machine learning for math
  • Project Leader: Rohan Pandey
  • Members: Sarthak Mitra, Noah Feinberg, Jolie, Shree
  • Description: Study how mathematical reasoning traces form and how they can be made more efficient and reliable. Building on recent work on scientific reasoning in language models, the team will explore reinforcement learning, prompt optimization, and Lean-based verification as feedback for improving chain-of-thought reasoning.

Chain-of-Thought Reasoning in Lean 4

  • Area: AI and machine learning for math
  • Project Leader: Evan Wang
  • Members: Chaoxiang Zhang, Tanmay Kuchhal
  • Description: Validate language-model reasoning by translating chain-of-thought traces into Lean 4 rather than relying only on first-order logical checks. The initial proof of concept will define a constrained, state-driven domain in Lean and use formal errors as feedback, helping models identify and correct contradictions, invalid state changes, and other logical mistakes in their reasoning traces.
  • Profiles: Evan Wang, Chaoxiang Zhang, Tanmay Kuchhal

Machine Learning Meets Algebraic Combinatorics 2

  • Area: AI and machine learning for math
  • Project Leaders: Henry Kvinge, Michael R. Zeng
  • Members: Emily Meng, Xuanyu Yang
  • Description: Train a small language model on a broad curriculum of algebraic combinatorics tasks. Building on prior work with permutations, the team will construct balanced training and evaluation sets for partitions, Young tableaux, and other core combinatorial objects, with the goal of learning rich, domain-aware representations.

ProofMem: Separating Proof Replay from Proof-Pattern Generalization in Lean Theorem Proving

  • Area: AI and machine learning for math
  • Project Leader: Yue Wu
  • Members: Zhi Chen, Jayme Kim
  • Description: Build a controlled Lean evaluation framework to distinguish exact proof replay from genuine proof-pattern generalization. The project will test whether models remain robust under superficial theorem perturbations, transfer proof ideas to sibling theorems, and retain those abilities after further fine-tuning. Evaluation will combine Lean verification with proof-script matching, token loss, tactic edit distance, and retention curves.
  • Profiles: Zhi Chen, Jayme Kim

Learning Conditional Return Laws from Financial Trading Signals

  • Area: Autoresearch
  • Project Leaders: Freda Zhang, Yue Wu
  • Description: Learn the full conditional distribution of future asset returns from trading signals, going beyond expected return to model volatility, tail risk, and downside probability. The learned distributions will be evaluated using calibration, probability integral transform diagnostics, value-at-risk violations, and proper scoring rules.

Albilich

  • Area: Autoresearch
  • Project Leaders: Ting Gong, Michael R. Zeng
  • Description: Investigate open problems in finite group theory using AI systems connected to computer algebra tools such as GAP. The project will draw problems from the field's regularly updated open-problem literature and combine agentic research methods with symbolic computation to search for new examples, patterns, and proofs.

Autoresearch: The Shortest Vector Problem

  • Area: Autoresearch
  • Project Leaders: Zihong Lin, Haocheng Cai
  • Description: Search for unusually short vectors in lattices arising from the Arakelov geometry of Grassmannians, beginning with the first unknown case, Gr(2,4). The team will develop a reliable program for computing lattice norms and, in parallel, adapt an autoresearch-style agentic loop to improve candidate vectors using explicit evaluation metrics. New computational evidence may lead to improved bounds or a new conjecture for the Grassmannian's essential minimum.
  • Code: GitHub repo

Learning and Formalizing Commutative Algebra

  • Area: AI for math learning and education
  • Project Leader: Tyson Klingner
  • Members: Drew Bladek, Escher Crawford
  • Description: Learn commutative algebra while formalizing a fundamental result in Lean. This summer primer will prepare the team to begin a larger formalization in Autumn with the goal of contributing it to mathlib.

Returning Projects

These six teams are continuing projects from Spring 2026, carrying established formalization, evaluation, and machine-learning work into the summer.

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

LeanGCD: Stabilizing Lean Generation

  • Project Leaders: Dean Light and Michael Theologitis
  • Description: LeanGCD aims to improve Lean proof generation by frontier large language models using inference-time stabilization methods rather than retraining. The project adapts grammar-constrained decoding techniques with Lean's syntax extensions. Planned contributions: a Lean-specific GCD implementation that plugs into HuggingFace/vLLM inference pipelines, and empirical evaluation on MiniF2F, ProverBench, and PutnamBench. Goal: ICML 2026 (October) or 2027 (January).
  • Code: GitHub repo
  • Members: Evan Wang, Ben Bioren, Naren P Ramakrishnan, Nhan Pham
  • Prerequisites: Python, ML / LLM inference experience

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

Mechanistic Interpretability beyond Groups

  • Project Leader: Junaid Hasan
  • Description: Transformers can learn modular arithmetic, but prior mechanistic work focused on invertible operations like cyclic addition and group composition: cases with clean, global algebraic structure. Modular multiplication over composite moduli (a monoid) breaks this: zero-divisors make the operation non-invertible, and no single global representation space suffices. The authors show that transformers handle this by partitioning inputs into local hierarchical regions where group-like structure is preserved, enabling localized Fourier mechanisms.
  • Members: Andrew (Zitong) Chen, Akhil Srinivasan, Hemkesh Bandi
  • Paper: Draft PDF

Reinforcement Learning for Polynomials

CayleyPy: Search on Massive Combinatorial Graphs

  • Project Leaders: Michael R. Zeng, Junaid Hasan, Vasily Ilin
  • 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.
  • Continuation: Continued through Summer 2026.
  • Members: Merav Frank, Sambhu Ganesan, Gaurang Pendharkar, Rithikesh Muddana, Danny Zhang
  • Prerequisites: solid Python, some group theory or combinatorics.