About
I am a postdoctoral researcher at the University of Edinburgh, working on AI for formal mathematics and verification.
My research sits at the intersection of programming languages, software engineering, and machine learning. I build tools that pair the guarantees of formal verification with modern machine learning, so that proving things — about mathematics and about software — takes less human effort. Most of that work targets interactive theorem provers, primarily Rocq and Isabelle, and spans proof automation (Proverbot9001), conjecturing (Lemmanaid), and autoformalisation (Sketchpad).
I completed my PhD in Computer Science at the University of California San Diego in 2025, advised by Sorin Lerner, with a thesis on automating formal verification in interactive theorem provers. Before that I earned a BA in Computer Science from Swarthmore College.
Feel free to get in touch — I am always glad to talk about proof automation, autoformalisation, or collaborations.
News
- Sep 2026 Attending the AI for Math convening for Renaissance Philanthropy grantees.
- Jul 2026 At FLoC 2026 in Lisbon, the 9th Federated Logic Conference.
- May 2026 At the CHAIR workshop at Chalmers, Gothenburg.
- 2026 Joined the University of Edinburgh as a postdoctoral researcher, working on Sketchpad.
- 2025 Defended my PhD at UC San Diego — Automating Formal Verification in Interactive Theorem Provers.
- Apr 2025 Lemmanaid: Neuro-Symbolic Lemma Conjecturing is out.