Math AI Lab University of Washington Papers published and in progress by UW Math AI Lab members, spanning AI for mathematics, formal verification, plasma physics, and quantum error correction.
Peer-reviewed and workshop papers by Math AI Lab members across machine learning, theorem proving, plasma physics, and mathematical search.
Estimating probability density and its score from samples remains a core problem in generative modeling, Bayesian inference, and kinetic theory. DiScoFormer bridges classical kernel methods and neural score models with a plug-in transformer-based estimator.
OpenReviewSearching for mathematical results remains difficult because most tools retrieve entire papers, while mathematicians and theorem-proving agents often seek a specific theorem. This work introduces semantic theorem retrieval across a unified corpus of 9.2 million theorem statements.
OpenReviewAs neural theorem provers become increasingly agentic, the ability to interpret and act on compiler feedback is critical. This work studies a fine-tuned repair model trained on erroneous Lean proofs paired with compiler diagnostics and corrections.
OpenReviewMotivated by auto-proof generation and Valiant's VP vs. VNP conjecture, this project formulates arithmetic circuit discovery as a single-player game where a reinforcement learning agent builds a circuit within a fixed number of operations.
OpenReviewPlasma modeling is central to the design of nuclear fusion reactors, but simulating collisional plasma kinetics from first principles remains computationally challenging. This work introduces a neural score-based approach for the Vlasov-Maxwell-Landau system.
OpenReviewA semi-autonomous formalization effort targeting the equilibrium theory of the Vlasov-Maxwell-Landau system in Lean 4, combining human-guided proof structure with AI-assisted tactic search.
arXivCurrent preprints and project papers from the lab.
A benchmark suite for evaluating AI systems on synthesizing quantum error-correcting stabilizer circuits, with systematic coverage of code families and circuit constraints relevant to near-term quantum hardware.
arXiv:2604.21287Software, formalization contributions, and manuscripts connected to current lab projects.
A mathlib contribution supporting the monogenic extensions project, generalizing an existing adjoined-root theorem by replacing an integrally closed hypothesis with a freeness hypothesis.
Mathlib PR #36421A formalization of finite étale local-ring monogenicity from arXiv:2503.07846, including supporting intermediate lemmas for broader monogenic extensions work.
Mathlib PR #37527A mechanistic interpretability study of how small transformers learn modular multiplication over composite moduli, extending group-composition explanations to non-invertible monoid structure.
PDFEssays and public-facing research perspectives connected to the lab.
A perspective piece on integrating large language models and formal proof assistants into mathematical practice, drawing on experiences from the UW Math AI Lab.
AMS