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), which refers to using a mixture of formal methods and machine-learning agents to automatically prove mathematical theorems within Proof Assistants.

Feel free to contact me by e-mail on the research page if you have any questions, requests for collaborations, and comments.

Education

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

Projects

• PyPantograph /Pantograph (arXiv): 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 flexibly handle metavariable coupling.

• Trillium (Main Developer): A machine-assisted theorem proving program to train and evaluate hybrid (SMT + GNN/LM) proving algorithms.

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

• cvc5: An SMT Solver

  I created the bitvector RARE rewrite rules. I’m working on its Rust interface

• verus: A Rust program verifier

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

Trivia

• How I got into Computer Science
• I play the violin (see OpenMusicScores).
• I lead the Cosplay division of Stanford Anime club and make (mostly Touhou) cosplay props. I do film grade post-processing for cosplayers.
• I make visualizations. It is a vestige from my art student days.