Simple Theorem Prover, an efficient SMT solver for bitvectors

Tactics for discharging Lean goals into SMT solvers.

Python library for monomial agnostic vanishing ideal computation

Official code for "Learning to compute Gröbner bases" (NeurIPS 2024)

Refreshing automation for inductive equational proofs using e-graphs

Lean 4 kernel / 'external checker' written in Lean 4

Integer Multiplier Generator for Verilog

Control Logic Synthesis: Drawing the Rest of the OWL

VSCode extension that is designed to help automate writing of Coq proofs.

A Lean formal proof of the Combinatorial Nullstellensatz

LLMs as Copilots for Theorem Proving in Lean

AMulet 2. - A better AIG Multiplier Examination Tool

Extracting Linear Relations from Gröbner Bases for Formal Verification of And-Inverter Graphs

Lecture notes for a course on writing proofs, on paper and in the Lean proof assistant

The Hitchhiker's Guide to Logical Verification (2025 edition) and associated materials

Code samples used on my blog

A minimal development of SSA theory

Logic Library for Lean 4

AlphaVerus: Formally Verified Code Generation through Self-Improving Translation and Treefinement

Algebra library for Lean 4

Tools for Recurrent Optimization via Machine Editing and related benchmarks

Armv8 Native Code Symbolic Simulator in Lean

Mixtape of computer algebra system (CAS) algorithms

The release for ICML 2023 paper

A (WIP) equality saturation tactic for Lean based on egg.