Math AI Lab University of Washington

Math AI Lab People

The people of the UW Math AI Lab during the 2025-26 academic year (Fall 2025 - Spring 2026). For the projects themselves, see the quarterly pages under Projects.

Leadership

Michael R. Zeng Michael R. Zeng Acting DirectorDhruv Bhatia Dhruv Bhatia Vice DirectorGiovanni Inchiostro Giovanni Inchiostro Faculty AdvisorVasily Ilin Vasily Ilin Founding DirectorJarod Alper Jarod Alper Founding Director

Project Leaders

Samuel Ainsworth Samuel Ainsworth JAX in LeanBryan Boehnke Bryan Boehnke Algebraic GeometryHaocheng Cai Haocheng Cai Monogenic ExtensionsArkamouli Debnath Arkamouli Debnath Geometric Invariant TheoryJunaid Hasan Junaid Hasan Deep Learning for Number TheoryAllison Henrich Allison Henrich Teaching a Computer to KnotEric Klavins Eric Klavins Zero-Knowledge Proofs, Formalizing StacksTyson Klingner Tyson Klingner How Good Are LLMs at Lean?Henry Kvinge Henry Kvinge Math2VecJohn Leo John Leo Monogenic ExtensionsDean Light Dean Light LeanGCDLeo Mayer Leo Mayer Geometric Invariant Theory, Commutative AlgebraHaoming Ning Haoming Ning Commutative AlgebraNelson Niu Nelson Niu Category TheoryAndres Paz Andres Paz AI for Quantum Code CompilationAndrew Tawfeek Andrew Tawfeek Teaching a Computer to KnotIgnacio Tejeda Ignacio Tejeda Geometric Measure TheoryMichael Theologitis Michael Theologitis LeanGCDBianca Viray Bianca Viray Algebraic Geometry

Members

Undergraduate and graduate researchers, with the project(s) they contribute to.

TA
Trey Adams RL for Polynomials
AA
Alexandra Aiello Zero-Knowledge Proofs
DA
Dowland Aiello Formalizing Stacks
LA
Luke Alexander Semantic Theorem Search
HB
Hemkesh Bandi Deep Learning for Number Theory
SB
Saharsh Bhargava Math2Vec
BB
Ben Bioren LeanGCD
DB
Drew Bladek LLMs at Lean
AB
Alexandre Borentain RL for Polynomials
JB
Jacob Boyce Geometric Invariant Theory
AC
Annie Cao Geometric Measure Theory
LC
Leo Carlin Math2Vec
C
Cecilia Math2Vec
AC
Alan Chang Provable Computation
AC
Andrew Chen Deep Learning for Number Theory
BC
Bohao Chen LLMs at Lean
SC
Simon Chess Lean Error Correction
KC
Kedar Chintalapati Math2Vec
EC
Escher Crawford LLMs at Lean
JD
Jared Darlington Math2Vec
ZF
Zeyin Feng Provable Computation
MF
Merav Frank CayleyPy
XF
Xinyue Fu LLMs at Lean
SG
Sambhu Ganesan CayleyPy
SG
Siyuan Ge OpenMath, Lean Error Correction
NG
Nailin Guan Commutative Algebra
TG
Ted Guan Semantic Theorem Search
NH
Nicole Ham Teaching a Computer to Knot
EH
Eric Hur Quantum Code Compilation
RJ
Rachit Jaiswal Math2Vec
JJ
Junye Ji Provable Computation
KJ
Kaijie Jin RL for Polynomials
J
Josh Geometric Measure Theory
SJ
Saumi Joshi OpenMath
DK
Dora Kassabova Commutative Algebra
SK
Sean Kawano Teaching a Computer to Knot
RK
Ruslana Korolov Provable Computation
SK
Sathvik Kurapati Algebraic Geometry
SK
Simon Kurgan Semantic Theorem Search
SL
Sylvie Lausier Quantum Code Compilation
DL
Daniel Lee Lean Error Correction
HL
Hansel Lee RL for Polynomials
EL
Eric Leonen Semantic Theorem Search
CL
Cordelia Li Quantum Code Compilation
JL
Jiahe Lu Math2Vec
JM
Jeremy Ma JAX in Lean
AM
Ajit Mallavarapu Lean Error Correction
JM
James Martin Formalizing Stacks
TM
Theo Meek OpenMath, Geometric Measure Theory
BM
Bhaumik Mehta RL for Polynomials
EM
Emily Meng Geometric Invariant Theory
AM
Abel Mesfin Teaching a Computer to Knot
M
Michael Math2Vec
NM
Naomi Morato RL for Polynomials
RM
Rithikesh Muddana CayleyPy
KN
Kaira Nair LLMs at Lean
RP
Rohan Pandey RL for Polynomials
NP
Nathan Pao Geometric Measure Theory
SP
Sarju Patel Quantum Code Compilation
GP
Gaurang Pendharkar CayleyPy
GP
George Peykanu Algebraic Geometry
NP
Nhan Pham LeanGCD
EP
Evan Porter RL for Polynomials
JQ
Joseph Qian Provable Computation
NP
Naren P Ramakrishnan LeanGCD
SR
Samarth Rao Math2Vec
AR
Artemii Remizov Semantic Theorem Search
VS
Veer Shukla Provable Computation
SS
Sukhman Singh Category Theory
AS
Akhil Srinivasan Deep Learning for Number Theory
SS
Solden Stoll Teaching a Computer to Knot
MS
Mayee Sun Quantum Code Compilation
SS
Sophie Szeto Semantic Theorem Search
CT
Christian Tarta Quantum Code Compilation
NT
Nina Tharamal Deep Learning for Number Theory
EW
Evan Wang LeanGCD, Lean Error Correction
TW
Tianshuo Wang Algebraic Geometry
YW
Yiran Wang Lean Error Correction, Semantic Theorem Search
AW
Annis Wu Provable Computation
DQ
Di Qiu Xiang OpenMath
CX
Claire Xu RL for Polynomials, Deep Learning for Number Theory
GY
Grant Yang Algebraic Geometry
XY
Xuanyu Yang Geometric Invariant Theory
DZ
Danny Zhang CayleyPy
IZ
Ivonne Zhang Deep Learning for Number Theory
KZ
Kyle Zhang RL for Polynomials
XZ
Xiaoxing Zhang CayleyPy
BZ
Bohan Zhao Geometric Invariant Theory
XZ
Xinyi Zhi Algebraic Geometry

Lab Photos

Fall 2025 Math AI Lab
// Fall 2025 Math AI Lab
Winter 2025 Math AI Lab
// Winter 2025 Math AI Lab
UW Lean Hackathon
// UW Lean Hackathon
ICLR 2026, Rio de Janeiro
// ICLR 2026, Rio de Janeiro
UW Lean Hackathon team
// UW Lean Hackathon