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). 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.
Feel free to contact me on Discord or by e-mail (listed on the webpage) if you have any questions.
Fun fact: My name can be written in Japanese (亜庭 れんに) and Russian (Лений Анива). I enjoy playing violin and photography.
(Photo credit: Jasmine Liu)