Math AI Lab University of Washington
All projects

Fall 2026 Projects

Inaugural meeting slides

Dates: September 30 - December 11

Project meetings: Mondays & Wednesdays, 4:00 - 5:30 pm, OUG 136. Teams may use different meeting times, but must meet in person at least once a week. Project-specific schedules are listed below.

Social event: Wednesday, November 4

Final presentations: Wednesday, December 9

Rosters: 14 projects · 60 students

Autoresearch

AI-Assisted Proof Discovery in Inverse Boundary Problems

  • Area: Autoresearch
  • Project Leader: Ruirui Wu ruirwu@uw.edu
  • Student members: Annie Feng, Kevin Wei, Kushal Kothapalli, Shiqi Yang, Harrison Bruechert
  • Abstract: This project explores AI-assisted mathematical discovery in inverse boundary problems, focusing on the partial data Calderón problem. We will develop and evaluate AI workflows to analyze existing proofs, identify obstacles, and propose new lemmas and proof strategies, with experts reviewing mathematical claims. The project aims to advance understanding of partial-data uniqueness and produce open-source tools and documented experiments assessing AI’s contribution to research mathematics.
  • Suggested references:
    1. Sections 2.7 and 2.8 of the book "The Calderón Problem: An Introduction" by Feldman, Salo, and Uhlmann. Basic real analysis knowledge may be required to follow these sections directly.
    2. Introduction section of the core research paper "The Calderón problem with partial data" by Kenig, Sjöstrand, and Uhlmann.

Mathematical Taste: Recognizing Progress Beyond Generation

  • Area: Autoresearch
  • Project Leader: Zihong Lin zhlin@uw.edu
  • Co-mentor: Will Dudarov
  • Student members: Ganesh Ravichandran, David An, Annie Cao, Duc Huy Nguyen, Bhuvan Gundela, Armen Agalyan
  • Abstract: Can a language model recognize a breakthrough it cannot discover on its own? Mathematical research requires judging which incomplete arguments are worth pursuing before a full proof is available. We will build a benchmark to test how models distinguish promising partial arguments from plausible but unproductive reasoning, including ideas beyond their demonstrated solving ability. We will also test whether model hidden states contain signals of mathematical promise that predict later progress more reliably than verbal judgments or confidence reports. Such signals could help long-running AI proof agents choose which directions to pursue and how much computation to invest.
  • Goals: Build a benchmark of partial arguments with key insights and convincing but stalled attempts, with mathematical review and checks for possible prior exposure to solutions. Compare models' ability to generate promising ideas, recognize supplied ideas, and continue the arguments under a fixed compute budget. Test whether hidden-state probes in open-weight models generalize across problems and add information beyond correctness judgments, including on problems the model can already solve. Release an open-source benchmark and reproducible evaluation code, and prepare a paper. Follow-up work could use the findings to guide proof search.
  • Timeline:
    • Fall 2026: Build the dataset and evaluation setup, compare initial models, and present preliminary findings by quarter's end.
    • Winter 2027: Refine the evaluation, study generation, recognition, and continuation, and explore hidden-state probes.
    • Spring 2027: Complete the study and release the benchmark and code. Aim for a submission-ready paper by May 1, 2027, tentatively targeting NeurIPS 2027; its official deadline is not yet confirmed.
  • Prerequisites:
    1. Experience with coding agents or a comparable technical background, plus clear communication (strongly required).
    2. Familiarity with proof-based mathematics, linear algebra, and multivariable calculus (highly desirable).
    3. Strong understanding of transformer architecture (desirable).

Lean Refactor

  • Area: Autoresearch; Recursive Self Improvement
  • Project Leader: Evan Wang aurasoph@uw.edu
  • Student members: Kedar Chintalapati, David Javnozon, Chuhan Li
  • Schedule: Competition ends November 8.
  • Abstract: Participation in the Lean Refactor competition for AI for Verifiable Coding @ Neurips 2026. Given a compiling Lean proof, can we make it “better”? Better being defined along 3 dimensions: compilation time, length, and version-robustness. There are two tracks, Closed Source and Open Source, and we will approach them both. Required to have an interest in harness engineering or familiarity with tuning open source models. Lean familiarity not required, somewhat encouraged.

    Competition ends November 8th, so this is a fast paced project that encompasses the first half of the quarter. The second half will be focused on generalizing the harness to be useful for refactoring Lean in the context of general projects.

  • Links: Workshop · Competition

Albilich v2: Math Metaharness

  • Area: Autoresearch and autoformalization infrastructure
  • Project Leaders: Ting Gong tgong2@uw.edu, Michael R. Zeng zengrf@uw.edu, Dean Light deanlcs@cs.washington.edu, Michael Theologitis mthe@cs.washington.edu, Evan Wang aurasoph@uw.edu
  • Student members: No student members.
  • Schedule: Metaharness meets Mondays, 3–4 p.m.
  • Abstract (Albilich v2): This project develops Albilich v2, a recursively self-improving AI system for mathematical research. Building on Albilich v1's auditable proof-state architecture, v2 will turn research experience itself into a source of improvement: learning from successful reductions, failed strategies, verifier feedback, literature use, tool calls, and software failures. Some of the wanted outcomes are to study whether mathematical ability of harness can be improved recursively, as well as to study whether AI's ability in a specific area can be improved via learnt skills with small amount of data.
  • Internal tools: Host and maintain the lab's internal tools on EC2: the Albilich autoresearch system, autoformalization tools (Polya and the benchmark tool), MCP tool calling, and TheoremSearch.

Learning Conditional Return Laws from Financial Trading Signals

  • Area: Autoresearch
  • Project Leaders: Freda Zhang qzhang52@uw.edu, Yue Wu yuew29@uw.edu
  • Student members: Daran Xu, Belinda Krista, Rithikesh Muddana, Archit Ganapule, Chaoxiang Zhang
  • Abstract: 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.

Formalizing the Scientific Method

  • Area: Autoresearch
  • Project Leaders: Eric Klavins klavins@uw.edu, Bryan Boehnke boehnkeb@uw.edu
  • Student members: Kavi Mahajan, Rohith Kala, Aiden Hoang
  • Abstract: The goal of this project is to 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?

Formalization & Autoformalization

Formalizing Algebra of Resultants and Determinantal Polynomials

  • Area: Formalization
  • Project Leaders: Joe Rogge jwrogge@uw.edu, Shaoda Ji shaodj@uw.edu
  • Student members: Grant Yang, Anders Lewis, Liron Shani, Nhi Bach, David Javnozon
  • Schedule: Meets at an alternate time; coordinate with the project leaders.
  • Abstract: The principal minor map, sending an nxn matrix to its vector of 2^n principal minors, has been extensively studied, with many properties of its image and fiber understood. The primary tools used in studying this map are determinantal polynomials (multiaffine polynomials organizing principal minors) and resultants, allowing elementary but powerful analysis of principal minor questions. Principal minors are of special interest because of so-called determinantal point processes (DPP's), probability distributions on subsets of [n] defined by the principal minors of an nxn matrix, which have applications in pure math as well as physics and machine learning. In this project, we will formalize some recently published results on principal minors, and along the way we will formalize some classical theorems about determinants which are not yet in Mathlib. Students will learn some cutting edge math, build Lean programming skills, and contribute several pull requests to mathlib.
  • Prerequisites:
    • Linear algebra (208 or equivalent) is a must for this project
    • Having taken a proofs class is strongly preferred
    • Some lean experience would be helpful but is not necessary
  • Goal: Formalize theorems about resultants and multiaffine polynomials from the following paper: https://arxiv.org/abs/2309.00806. The natural starting point is theorem 2.1 (proven as theorem 3.1 in https://arxiv.org/abs/2205.05267 by ~3 pages of natural language), which should on its own provide a challenging but achievable goal. Formalizing this proof will involve formalizing the Desnanot–Jacobi identity, an important determinantal identity not yet in Mathlib; this project would contribute classical as well as cutting edge results to Mathlib. Natural extensions would be formalizing so-called principal minor equivalence, treated in https://arxiv.org/abs/2410.01961, or Hermitian determinantal representations, treated in https://arxiv.org/abs/2205.05267. Assuming sufficient progress is made, we will submit Mathlib PR's every quarter.

Formalizing Modern Techniques in Probability Theory

  • Area: Formalization
  • Project Leader: Brayden Letwin letwin@uw.edu
  • Co-mentor: Will Dudarov
  • Student members: Cosun Zhou, Aarush Sharma, Elisa Regueros, Owen Parks
  • Abstract: In 2012, Ronen Eldan introduced a remarkable new technique in probability theory, now broadly known as stochastic localization. Since its introduction, stochastic localization (and, more generally, the philosophy behind it) has become an extremely powerful tool, leading to major advances in probability, convex geometry, and theoretical computer science. The goal of this project is to formalize stochastic localization and related ideas from the literature in Lean/Mathlib.

    We will begin by formalizing the techniques developed in Eldan's foundational paper (https://arxiv.org/pdf/1203.0893). In addition to contributing directly to the formalization, the project leader will serve as a mentor and help coordinate the mathematical direction of the project. This will include explaining the underlying probability theory, and helping participants navigate the mathematical literature. At the same time, the project is intended to be a collaborative learning experience. Participants will be encouraged to learn the theory together, propose directions, take ownership of individual components, and contribute to the broader development of stochastic localization in Mathlib. Motivated students with an interest in probability theory, convex geometry, theoretical computer science, or formalization of mathematics are encouraged to participate.

Autoformalizing Mathematical Benchmarks

  • Area: Autoformalization
  • Project Leader: Theodore Meek theomeek@uw.edu
  • Continuing members: Michael R. Zeng, Pei Li, Simon Kurgan
  • Abstract: 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.

Code Certifications

  • Area: Formalization & Autoformalization
  • Project Leaders: Eric Klavins klavins@uw.edu, Dhruv Bhatia dbhatia1@uw.edu
  • Student members: Owen Fei, Sriram Marasanapalle-Kalle, Connor Zacharias, Yash Meher
  • Abstract: 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.

Mathematical Machine Learning

PermuFormer 2

  • Area: AI and machine learning for math
  • Project Leader: Henry Kvinge hjk3@uw.edu
  • Graduate mentors: Michael R. Zeng zengrf@uw.edu, Junaid Hasan junaid01@uw.edu, Treanungkur Mal, Ron Cherny
  • Student members: James Kwong, Emily Meng, Bhargava Perumalla, Onkit Samanta, Allen (Ailun) Shen, Yash Pratik Solanki, Mayee Sun, William Tran, Xuanyu Yang, Billy (Yinqi) Zhao
  • Schedule: First meeting: Wednesday, October 7, 4 p.m.
  • Start here: PermuFormer: Multi-Task Pretraining for Permutation Representation in Algebraic Combinatorics
  • Abstract: The continuation of Permuformer: 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. We might gain the following two kinds of results: - a better understanding of how complex reasoning ability emerges from modern LLMs; - new conjectures and theorems from patterns captured by these specialized models.

Mathematician's Copilot: Math2Vec

  • Area: Mathematical Machine Learning
  • Project Leader: Henry Kvinge
  • Student members: Cecilia (Jiaying) Ye, Samarth Rao, Vaibhav Jasti, George Peykanu, Arnav Jain, Prithvi Aravind
  • Continuing students: Cecilia (Jiaying) Ye, Samarth Rao
  • Schedule: First meeting: Wednesday, October 7, starting at 4:45 p.m.
  • Start here: Does My Embedding Reflect That A = B? Evaluating Mathematical Equivalence in Embedding Models
  • Abstract: 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.

Math Education

Math Tutor / Polya

  • Area: AI for math learning and education
  • Project Leaders: Eric Klavins klavins@uw.edu, Dan Mikulincer danmiku@uw.edu
  • Student members: Jake Malody, Hayden Guo, Amey Bharambe, Eshaan Kumar
  • Abstract: The goal of this project is to 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 control, 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.

AI Math Textbook

  • Area: AI for math learning and education
  • Project Leaders: Giovanni Inchiostro, Dhruv Bhatia dbhatia1@uw.edu
  • Student members: Ethan Wang, Aarnith Netrawali, Saksham Singh, Nicole Ham, Abel Mesfin
  • Abstract: 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.