BlogArchivesGitAboutResearchNHF1

Leni Aniva

Leni Aniva

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 SMT solvers, neurosymbolic systems, 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.

For details about my academic contributions, or for collaborations, questions, and comments, see research page.

Education

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

Projects

  • 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).

  • PyPantograph / Pantograph (arXiv, TACAS’25): 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. It is used by multiple industry and academic labs including ByteDance, Amazon, MorphLabs, etc.

  • cvc5: An SMT Solver

    I created the BitVector RARE rewrite rules for proof generation (Springer, TACAS’24).

Teaching

In Spring 2025, I and Abdal designed and taught Stanford’s CS 99: Functional Programming and Theorem Proving in Lean 4. You can preview the course here. For the course’s infrastructure, see details.

Trivia