Fall 2026 Projects

Fall 2026 projects. (September 30 – December 11).

Project member application — Deadline: Tuesday, September 22, 2026.

Autoresearch

AI-Assisted Proof Discovery in Inverse Boundary Problems

• Area: Autoresearch
• Project Leaders: Ruirui Wu ruirwu@uw.edu, Zihong Lin zhlin@uw.edu
• Abstract: Inverse problems seek to determine properties of a medium by exterior measurements. As a prototypical example, the Calderón problem asks whether we can determine the electrical conductivity of a medium by making voltage and current measurements on the boundary. This project investigates how AI can assist in the discovery of proof in inverse boundary problems. Our main target is to relax the data observation set geometry requirement for the partial data Calderón problem in dimension 3 or higher: when both applied voltages and measured currents are restricted to the same arbitrary open subset of the boundary. We will use AI to analyze existing results and proofs, identify obstacles to extending them, and develop and attempt new proofs. The mathematical correctness will be audited by the project leader and possibly team members with corresponding math background.
• Planned contributions: We plan two connected contributions: An open-source workflow for AI-assisted proof development, including retrieval of relevant results and iterative proposal and criticism of candidate arguments. A formalization of new intermediate results for the partial data Calderón problem with applied voltages and measured currents restricted to the same arbitrary open subset of the boundary, which can be included in a mathematical paper.

Mathematical Taste: Recognizing Progress Beyond Generation

• Area: Autoresearch
• Project Leader: Zihong Lin zhlin@uw.edu
• 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 Leaders: Evan Wang aurasoph@uw.edu, Dean Light deanlcs@cs.washington.edu, Michael Theologitis mthe@cs.washington.edu
• 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 + Internal Tools

• 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 [Dean and Michael T. on the recursive self-improvement (RSI) aspects]
• 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
• 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.

Formalization & Autoformalization

Formalizing Algebra of Resultants and Determinantal Polynomials

• Area: Formalization
• Project Leaders: Joe Rogge jwrogge@uw.edu, Bryan Boehnke boehnkeb@uw.edu, Shaoda Ji shaodj@uw.edu
• 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 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. 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. This project provides an accessible entry point both to cutting edge mathematics and to formalization, with some easy results ready to be formalized and a clear ladder of results of increasing difficulty.
• 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
• 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
• Members (continuing): Michael R. Zeng zengrf@uw.edu, Pei Li peilinli@uw.edu
• 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.

Mathematical Machine Learning

PermuFormer 2

• Area: AI and machine learning for math
• Project Leaders: Henry Kvinge hjk3@uw.edu, Michael R. Zeng zengrf@uw.edu, Junaid Hasan junaid01@uw.edu; graduate mentors Treanungkur Mal maltreanungkur@gmail.com, Ron Cherny rcherny@uw.edu
• 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 emerge from modern LLMs; - new conjectures and theorems from patterns captured by these specialized models.

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

• Area: AI and machine learning for math
• Project Leader: Yue Wu yuew29@uw.edu
• Members (continuing): Zhi Chen, Jayme Kim hyungoo@uw.edu
• Abstract: 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.

Math Education

Math Tutor / Polya

• Area: AI for math learning and education
• Project Leaders: Eric Klavins klavins@uw.edu; Dan Mikulincer danmiku@uw.edu [tentative — intent to be confirmed]
• 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 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 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
• 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.

Code Certifications

• Area: AI for math learning and education
• Project Leaders: Eric Klavins klavins@uw.edu, Dhruv Bhatia dbhatia1@uw.edu
• 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.

Formalizing the Scientific Method

• Area: AI for math learning and education
• Project Leader: Eric Klavins klavins@uw.edu
• 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?