All work
Mathematical Theorem Retrieval
Worked on mathematical search across natural language, LaTeX, and Lean.
From statement to retrieved theorem. Select a stage.
The problem
Mathematical statements can express the same idea in very different language. Retrieval tools need representations that connect those forms, including formal statements written in Lean.
My contribution
At the UW Math AI Lab, I developed a fine-tuned embedder for theorem retrieval across natural language, LaTeX, and Lean under the guidance of Vasily Ilin and Henry Kvinge.
Research output
I coauthored the public preprint Does My Embedding Reflect That A = B? Evaluating Mathematical Equivalence in Embedding Models. The work was presented at the ICML 2026 AI for Math Workshop and accepted at the NeurIPS 2026 Math AI Workshop.