I’m a computer science PhD candidate at UMN advised by Favonia.

Previously, I was a math student at UPenn and Northwestern.

My research is in homotopy type theory, proof assistants,
and machine-checked mathematics. In particular, I work on
computer-checked proofs in synthetic homotopy theory and in
associated aspects of category theory.

I also build mathematical software, including:

  • an open-source semidefinite programming solver in Rust
  • an open-source cyclic coordinate descent solver for computing
    risk parity portfolios, also in Rust.

I am on the job market for Fall 2026 roles in formal verification,
mathematical software, optimization, and computational finance.
I’d be happy to chat about roles that may be a good fit.