About

I am a CS PhD student at Stanford University’s Centaur Lab. Prior to entering Stanford, I studied at the University of Waterloo and graduated in 2022. My main research interests are in SMT solvers and machine-assisted theorem proving (MATP). MATP refers to using machine-learning agents to automatically prove theorems within Proof Assistants. The term MATP was coined by me and Dr. Clark Barrett to avoid confusion with an existing term, Automated Theorem Proving (ATP) which refers to first order logic only.

• Ph.D. in Computer Science, Stanford University (2022-)
• Bachelor of Computer Science (Data Science), University of Waterloo (2017-2022)

Feel free to contact me by e-mail (listed on this page) if you have any questions, requests for collaborations, and comments.

Projects

• PyPantograph /Pantograph (Main Developer): A machine-to-machine interaction interface for Lean 4.

  This interface overcomes several issues in preceding works such as LeanDojo and repl. It supports branching tactics (have, let, calc), and can handle metavariable coupling with no comproimise.

• Trillium (Main Developer): A machine-assisted theorem proving program for using GNNs to search for proofs.

  Trillium which trains and evaluates AIML agents. Due to the scant availability of code in this field, one of the program’s fundamental requirements is being compatible with other theorem proving works.

  This is a massive engineering project with multiple languages and frameworks being involved (Rust, Lean, Svelte, Nix, Python).

• cvc5: An SMT Solver

  I created the bitvector RARE rewrite rules.

• verus: A Rust program verifier

  I work on monomorphization of its type system and integration with cvc5.

I sometimes contribute to the open source community. See GitHub.

Others

• I play the violin (see OpenMusicScores).
• I make (mostly Touhou) cosplay props.
• I do film grade postprocessing for cosplayers.
• I make diagrams for course notes and visualizations.