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.

Curriculum Vitae

Education

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

Research

  • Nazrin (under review): Atomic Tactics and Transposing Atomization

    Icon

    Nazrin: Atomic Tactics for Graph Neural Networks for Theorem Proving in Lean 4

    Leni Aniva, Iori Oikawa, David Dill, Clark Barrett

    In this work, we introduce several novel concepts and capabilities to address obstacles faced by machine-assisted theorem proving: Atomic Tactics which are a small finite, and complete set of tactics; Transposing Atomization which turns arbitrary proofs into atomic tactic traces; ExprGraph, which is a graph representation of expression; Nazrin Prover, which is a GNN-based theorem proving agent.

    matp lean

    Can rigorous reasoning be broken down into atomic steps? In this article, I’ll prove it.

  • PyPantograph / Pantograph, TACAS’25): A machine-to-machine interaction interface for Lean 4.

    Icon

    Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4

    Leni Aniva, Chuyue Sun, Brando Miranda, Clark Barrett, Sanmi Koyejo

    In this paper, we introduce Pantograph, a tool that provides a versatile interface to the Lean 4 proof assistant and enables efficient proof search via powerful search algorithms such as Monte Carlo Tree Search. In addition, Pantograph enables high-level reasoning by enabling a more robust handling of Lean 4's inference steps.

    matp lean

    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