As of September 2026, I am a postdoctoral fellow at the Institute for Computer-Aided Reasoning in Mathematics, an NSF Mathematical Sciences Research Institute dedicated to the application of AI and formal methods to mathematics. The institute is hosted by Carnegie Mellon University.
At ICARM, I am currently working on building formally verified Rust code for numerical optimization and on using large language models to generate machine-checked mathematical proofs.
I completed my PhD in Computer Science at UMN, where I was advised by Favonia.
My PhD research was on homotopy type theory, proof assistants, and machine-checked mathematics. In particular, I worked on computer-checked proofs in synthetic homotopy theory and in associated aspects of category theory.
Before starting my PhD, I studied math at UPenn and Northwestern.
Beyond my research work, I maintain a serious personal interest in quantitative approaches to asset management. I have developed some end-to-end portfolio optimization engines in Rust and Python, based on a couple of open-source numerical optimization libraries I’ve developed: