Math AI Lab People
The people of the UW Math AI Lab through Summer 2026. For the projects themselves, see the quarterly pages under Projects.
Project Leaders
Samuel Ainsworth JAX in Lean
Bryan Boehnke Algebraic Geometry
Haocheng Cai Monogenic Extensions, Shortest Vector Problem
Arkamouli Debnath Geometric Invariant Theory
Ting Gong Albilich
Junaid Hasan Deep Learning for Number Theory, Mechanistic Interpretability, CayleyPy
Allison Henrich Teaching a Computer to Knot
Eric Klavins Zero-Knowledge Proofs, Formalizing Stacks
Tyson Klingner LLMs at Lean, Learning and Formalizing Commutative Algebra
Henry Kvinge Math2Vec, Machine Learning Meets Algebraic Combinatorics
John Leo Monogenic Extensions
Dean Light LeanGCD
Zihong Lin Shortest Vector Problem
Leo Mayer Geometric Invariant Theory, Commutative Algebra Theodore Meek Autoformalizing Mathematical Benchmarks, Geometric Measure Theory
Haoming Ning Commutative Algebra
Nelson Niu Category Theory Rohan Pandey Improving Mathematical Chain-of-Thought Reasoning, RL for Polynomials
Andres Paz AI for Quantum Code Compilation
Andrew Tawfeek Teaching a Computer to Knot
Ignacio Tejeda Geometric Measure Theory
Michael Theologitis LeanGCD
Bianca Viray Algebraic Geometry Evan Wang Chain-of-Thought Reasoning in Lean 4, LeanGCD
Yue Wu ProofMem, Conditional Return Laws
Freda Zhang Conditional Return LawsMembers
Undergraduate and graduate researchers, with the project(s) they contribute to.
TA
Trey Adams RL for PolynomialsAA
Alexandra Aiello Zero-Knowledge ProofsDA
Dowland Aiello Formalizing StacksLA
Luke Alexander Semantic Theorem SearchHB
Hemkesh Bandi Deep Learning for Number TheorySB
Saharsh Bhargava Math2VecBB
Ben Bioren LeanGCDDB
Drew Bladek LLMs at Lean, Learning and Formalizing Commutative AlgebraAB
Alexandre Borentain RL for PolynomialsJB
Jacob Boyce Geometric Invariant TheoryAC
Annie Cao Geometric Measure TheoryLC
Leo Carlin Math2VecC
Cecilia Math2VecAC
Alan Chang Provable ComputationAC
Andrew Chen Deep Learning for Number TheoryBC
Bohao Chen LLMs at LeanZC
Zhi Chen ProofMemSC
Simon Chess Lean Error CorrectionKC
Kedar Chintalapati Math2VecEC
Escher Crawford LLMs at Lean, Learning and Formalizing Commutative AlgebraJD
Jared Darlington Math2VecNF
Noah Feinberg Improving Mathematical Chain-of-Thought ReasoningZF
Zeyin Feng Provable ComputationMF
Merav Frank CayleyPyXF
Xinyue Fu LLMs at LeanSG
Sambhu Ganesan CayleyPySG
Siyuan Ge OpenMath, Lean Error CorrectionNG
Nailin Guan Commutative AlgebraTG
Ted Guan Semantic Theorem SearchNH
Nicole Ham Teaching a Computer to KnotEH
Eric Hur Quantum Code CompilationRJ
Rachit Jaiswal Math2VecJJ
Junye Ji Provable ComputationKJ
Kaijie Jin RL for PolynomialsJ
Jolie Improving Mathematical Chain-of-Thought ReasoningJ
Josh Geometric Measure TheorySJ
Saumi Joshi OpenMathDK
Dora Kassabova Commutative AlgebraSK
Sean Kawano Teaching a Computer to KnotJK
Jayme Kim ProofMemRK
Ruslana Korolov Provable ComputationTK
Tanmay Kuchhal Chain-of-Thought Reasoning in Lean 4SK
Sathvik Kurapati Algebraic GeometrySK
Simon Kurgan Semantic Theorem SearchSL
Sylvie Lausier Quantum Code CompilationDL
Daniel Lee Lean Error CorrectionHL
Hansel Lee RL for PolynomialsEL
Eric Leonen Semantic Theorem SearchCL
Cordelia Li Quantum Code CompilationPL
Pei Li Autoformalizing Mathematical BenchmarksJL
Jiahe Lu Math2VecJM
Jeremy Ma JAX in LeanAM
Ajit Mallavarapu Lean Error CorrectionJM
James Martin Formalizing StacksBM
Bhaumik Mehta RL for PolynomialsEM
Emily Meng Geometric Invariant Theory, Machine Learning Meets Algebraic CombinatoricsAM
Abel Mesfin Teaching a Computer to KnotM
Michael Math2VecSM
Sarthak Mitra Improving Mathematical Chain-of-Thought ReasoningNM
Naomi Morato RL for PolynomialsRM
Rithikesh Muddana CayleyPyKN
Kaira Nair LLMs at LeanNP
Nathan Pao Geometric Measure TheorySP
Sarju Patel Quantum Code CompilationGP
Gaurang Pendharkar CayleyPyGP
George Peykanu Algebraic GeometryNP
Nhan Pham LeanGCDEP
Evan Porter RL for PolynomialsJQ
Joseph Qian Provable ComputationNP
Naren P Ramakrishnan LeanGCDSR
Samarth Rao Math2VecAR
Artemii Remizov Semantic Theorem SearchS
Shree Improving Mathematical Chain-of-Thought ReasoningVS
Veer Shukla Provable ComputationSS
Sukhman Singh Category TheoryAS
Akhil Srinivasan Deep Learning for Number TheorySS
Solden Stoll Teaching a Computer to KnotMS
Mayee Sun Quantum Code CompilationSS
Sophie Szeto Semantic Theorem SearchCT
Christian Tarta Quantum Code CompilationNT
Nina Tharamal Deep Learning for Number TheoryTW
Tianshuo Wang Algebraic GeometryYW
Yiran Wang Lean Error Correction, Semantic Theorem SearchAW
Annis Wu Provable ComputationDQ
Di Qiu Xiang OpenMathCX
Claire Xu RL for Polynomials, Deep Learning for Number TheoryGY
Grant Yang Algebraic GeometryXY
Xuanyu Yang Geometric Invariant Theory, Machine Learning Meets Algebraic CombinatoricsCZ
Chaoxiang Zhang Chain-of-Thought Reasoning in Lean 4DZ
Danny Zhang CayleyPyIZ
Ivonne Zhang Deep Learning for Number TheoryKZ
Kyle Zhang RL for PolynomialsXZ
Xiaoxing Zhang CayleyPyBZ
Bohan Zhao Geometric Invariant TheoryXZ
Xinyi Zhi Algebraic GeometryLab Photos
