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 machine-learning agents to automatically prove theorems within Proof Assistants.

• 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 on the research 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 flexibly handle metavariable coupling.

• 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

• How I got into Computer Science
• I play the violin (see OpenMusicScores).
• I 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.