Mathematics, computing & theater
I’m a fourth-year in the University of Washington’s computer science BS/MS program, also majoring in pure mathematics.
This summer I was an applied scientist intern at Madrona Venture Group, where I worked on large-scale data and ML problems and designed a founder-discovery model for the firm’s investors. My interests were previously in combinatorial optimization and probability; I’m now shifting toward empirical AI. I also write about musical theater.
I’m looking for a model-focused machine learning engineering role at a startup, or a research residency, for June 2027–June 2028, before returning to UW for the master’s year.
Computer vision · Personal tools
A wardrobe catalogue from a phone video.
Extracts garments from a closet walkthrough, groups multiple views of each piece, and adds generated flat-lays and descriptions. The interactive demo pairs a 34-piece catalogue with frames from the original recording.
Formal verification · Experimental
Your proof, checked step by step in Lean.
Maps the definitions, lemmas and theorems in an Overleaf paper, restates each step of a written proof in Lean 4, and shows exactly which step fails. It checks whether the proof works, not just whether the result is true. A Chrome extension and macOS app; Lean and Mathlib run locally.
Ising formulations for the traveling salesperson problem and related graph optimization problems. Mentored by Prof. Jerry Li (UW), collaborating with Medha Mittal (UW) and Devrath Iyer (Stanford), with guidance from Prof. Sara Achour (Stanford).
University of Washington.
The watch, the timer, and the limits of love in The Last Five Years.
Read the essayI sometimes expand lecture notes into a more systematic treatment, filling in proofs and connecting ideas. Here are a few of those notes.
Why does an optimal policy exist, and how can we find it? A fixed-point argument for finite discounted Markov decision processes leads to value iteration and policy iteration.
What can gradient descent guarantee, and what changes when gradients are noisy? Proofs trace how smoothness and convexity determine convergence and its speed.
How can we describe when and where a diffusion leaves a region? Starting with conditional expectation and Itô calculus, these notes connect stochastic paths to boundary-value problems.