Bio

I am a PhD student at the University of Utah working with Professor Srikanth Iyengar. I graduated from the University of Washington in Spring 2022 with a BS in Computer Science & Mathematics. I work in commutative algebra and homotopy theory. Currently I have active projects in modular invariant theory, descent for spectra, and local/complete dualizability in tt-categories. I also formalize mathematics in the Lean proof assistant; logic and programming language theory have a special place in my heart.

Papers

Shumo Chu, Brendan Murphy, Jared Roesch, Alvin Cheung, Dan Suciu, Axiomatic Foundations and Algorithms for Deciding Semantic Equivalences of SQL Queries. arXiv:1802.02229 [cs.DB]

Talks

Analysis and calculus in Mathlib, Utah Lean Seminar, September 2026. Worksheet Solutions
Introduction and first functions (with Brian Nugent), Utah Lean Seminar, September 2026. Worksheet
Formalizing the Brouwer fixed point theorem in Lean, BIRS workshop 23w5124. Slides
The Lean theorem prover and formal mathematics, BIKES, 2023. Slides

Notes

Simplicial sets and the Quillen model structure, written for a seminar talk (2023). PDF
Spectra and the Spanier–Whitehead category (2024). PDF

Seminars

I co-organize the Utah Lean Seminar with Brian Nugent and Karl Schwede.
I co-organized BIKES, the graduate student commutative algebra seminar at Utah, in 2024.

Formalization

I am a Mathematical Research Engineer with the Mathlib Initiative, working on StacksLib.
Contributions to Mathlib, including regular sequences, associated primes, and the opposite of a braided monoidal category.
The Brouwer fixed point theorem, in Lean 3.
The Jordan–Hölder theorem, in Lean 3.