Research

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.

Research Topics

I’m currently interested in developing hybrid theorem proving agents. With my tool PyPantograph, we can now port other theorem proving works from Isabelle and Coq to Lean 4.

Prospective Collaborators

Please send me an email at aniva at stanford dot edu and we can discuss about collaborations. Undergraduate and master students are welcome.