I am a senior applied mathematics student studying at the University of California, Berkeley. My primary research interests involve machine learning, particularly in image modeling, and formalizing computer science and AI concepts in verifiable code. I tend towards work that combines rigorous, mathematical theory with real-world applications.
This previous summer, I participated in the Polymath Jr REU program, where I learned to build scalable image generation models using modern machine learning techniques. Our work focused on drifting models, a new state-of-the-art image generation model which was introduced earlier this year. Check out my model and other details about the project on the machine learning tab.
Outside of research, I enjoy building projects, learning new areas of mathematics, and exploring applications of math in fields such as economics and quantitative finance. This site is a collection of my research, projects, writing, and other things I’m currently learning. I hope you enjoy!
Selected work
Applied research at the intersection of data, models, and mathematical structure.
Drifting without a pretrained encoder
Drifting compares real and generated samples to build a correction field, so it needs a way to judge when two images are alike. That normally means borrowing a pretrained encoder. This model judges similarity in its own learned features instead, and generates an image in a single network call.
Explore the projectFrom time series to trees
A model study comparing classical multivariate forecasting with random forests and nearest neighbors across six decades of quarterly economic data.
Explore the projectProofs & systems
Machine-checked mathematics: proving the things a method quietly assumes.
The assumption underneath drifting
A recent training method stops when a certain field vanishes, and treats that as proof the model has learned the data. Nobody had proved it does. This is a machine-checked proof that it does — for arbitrary probability measures, in every finite dimension, with no conditions attached.
Read the walkthroughReal analysis with filters
Written out with epsilons and deltas, "tends to" is about 169 separate definitions, and composing them needs some 2,197 lemmas. One filter definition replaces the lot. A directed reading project, with the definitions and proofs checked in Lean.
Read the walkthroughResearch experience
Two programs, the second built on the first: a semester reading pure mathematics with a graduate mentor, then a summer putting what it taught me to work on generative models.
May — Aug 2026
Machine learning research · Mentors Giulio Trigila and Ricardo Baptista
Sep — Dec 2025
Mathematics research · UC Berkeley · Mentor Thomas Browning
The reading program was pure mathematics and had nothing to do with machine learning. What it left me with was Lean.
Eight months later that turned out to be the useful thing. Drifting stops training when a certain field reaches zero and treats that as evidence the model has learned the data — but nobody had proved it. If two different distributions could cancel each other out, a model could report a perfect loss and be wrong, with nothing in the training loop able to tell. Writing that proof was only an option because a semester on filters had already taught me the language and the library it needed.
It also changed how I read the machine learning papers. Formalizing an argument makes you notice which steps are actually established and which are being waved through, which is the habit that found the gap in the first place.
Background
Applied mathematics at Berkeley, with research in generative models and machine-checked proof.
2025 — 2027
BS Applied Mathematics · Berkeley, CA
May — Aug 2026
Machine learning research
Sep — Dec 2025
Mathematics research · UC Berkeley
Each one has a full write-up on this site.
