Math AI Lab University of Washington
Fall 2026

Fall 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

Applications for Fall 2026 project leaders are open through Monday, September 7, 11:59 pm! Apply through the Fall 2026 Project Lead form.

The goal of projects is a publication/workshop paper (e.g. ICLR, ICML, and NeurIPS) or a significant open-source contribution, e.g. PR to mathlib4 or open-source tool available on GitHub.

Continuing Projects

These teams began their work in previous quarters and continue into the fall. Several of them are looking for a new graduate student mentor.

Autoformalizing Mathematical Benchmarks

  • Area: Autoformalization
  • Project Leader: Theodore Meek
  • Members: Michael R. Zeng, Pei Li
  • Description: Formalize two natural-language, research-level benchmarks, LemmaBench and OpenConjecture, using an agentic workflow in which AI agents check and refine one another's work. Every resulting statement also receives human review and is classified as faithful, uncertain, or unfaithful.

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, using 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
  • Looking for: new members
  • Description: Validate language-model reasoning by translating chain-of-thought traces into Lean 4. The team defines a constrained, state-driven domain in Lean and uses formal errors as feedback, helping models identify and correct contradictions, invalid state changes, and other logical mistakes in their reasoning traces.

PermuFormer 2

  • Area: AI and machine learning for math
  • Project Leaders: Henry Kvinge, Michael R. Zeng
  • Looking for: new students and a graduate student mentor
  • Description: The continuation of Machine Learning Meets Algebraic Combinatorics: train a small language model on a broad curriculum of algebraic combinatorics tasks, building balanced training and evaluation sets for partitions, Young tableaux, and other core combinatorial objects.

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: Do LLMs memorize proof logic, or just do pattern matching? Build a controlled Lean evaluation framework that distinguishes exact proof replay from genuine proof-pattern generalization, testing robustness under theorem perturbations, transfer to sibling theorems, and retention after further fine-tuning.

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. In the fall the team also maintains the project's agent harness and MCP tooling.

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, with the goal of contributing the formalization to mathlib.

Proposed New Projects: AI for Math Learning

New projects looking for mentors and students!

AI Math Learning Environment

  • Area: AI for math learning and education
  • Description: A full-screen, distraction-free lecture environment with almost no controls, where mathematics appears gradually rather than as a wall of text, ideally in a handwritten-style visual format. The system supports voice commands, and the user can pause and ask questions, which are answered on a separate board and can be merged into the lecture board. The intended workflow: upload a piece of mathematics, such as a PDF, choose a number of minutes, and the tool builds a lecture of that length. Each user has a profile so the system knows what they already know and crafts lectures accordingly, and a feedback system tracks which interactions the user liked.

AI Math Textbook

  • Area: AI for math learning and education
  • Description: Turn an existing wall-of-text PDF into an interactive, HTML-based learning experience. Every piece of terminology becomes clickable, opening a hovering window with the full definition, and every cross-reference opens the full statement the same way. A chatbot holds the whole paper in context so the learner can ask questions in real time. The embellished version should contain far more flowcharts, mindmaps, and schematics, with two levels of presentation: undergraduate and graduate/researcher.

A New and Improved Natural Language Game

  • Area: AI for math learning and education
  • Description: A learning game that may combine with the textbook idea and serve as a testbed for the workflow, with each project leader bringing their own textbook. The experience resembles someone presenting a section of the textbook to you: main ideas come first, each clickable and expandable, with the material organized as a graph that zooms in all the way to the level of a proof tree. Both nodes and edges are clickable, definitions stay collapsed until clicked, and instant feedback is built in.

Math Tutor

  • Area: AI for math learning and education
  • Project Leader: Eric Klavins
  • Description: Teach mathematics to a student in a goal-directed approach informed by an estimation of the student's knowledge, built up from assessing their performance on a set of problems. Using a combination of agent-based LLMs, the Lean proof assistant, and model-predictive methods, students are served custom-made problems that extend their knowledge and skills optimally fast. A prototype of this approach, called Polya, has been developed by the Klavins lab and can teach basic topology among other subjects. Students working on this project will extend the approach by designing and testing new agentic harnesses and by developing new curricula.

The Scientific Method

  • Area: AI for math learning and education
  • Project Leader: Eric Klavins
  • Description: Formalize the scientific method in Lean and LLMs, in an attempt to answer the question: can the experiments done in a given scientific paper refute hypotheses derived from a mathematical model of the physics involved? For example, given a model of a gene network, a hypothesis about a particular gene interaction, and a molecular perturbation, does the perturbation provide information about the interaction?

Code Certifications

  • Area: AI for math learning and education
  • Project Leader: Eric Klavins
  • Description: When an LLM produces, say, Python code for your project, how do you know that code is correct? One approach is to have it also produce a logical specification of what the code should do, together with a proof that the code meets the specification. For example, if you asked for code that sorts lists, you would get a function from lists to lists and a proof that the function is decidable and correct. The team will build a custom agentic harness and a Lean evaluator, and use an off-the-shelf Lean to Python translator.

Infrastructure

Maintaining Internal Tools

  • Area: Autoresearch and autoformalization infrastructure
  • Project Leader: to be announced
  • Description: Host and maintain the lab's internal tools on EC2: the Albilich autoresearch system, the autoformalization stack (Polya and the benchmark tool), MCP tool calling, and TheoremSearch.

Possibly Returning

Continuation of these projects into the fall is still being confirmed.

  • LeanGCD (being revamped) - Dean Light, Michael Theologitis
  • Mechanistic Interpretability of Groups and Monoids (potential follow-up) - Junaid Hasan
  • Contact us if your project was missed!