A project to digitalise results from physics into Lean.

The Lean Computer Science Library (CSLib)

Tactics for discharging Lean goals into SMT solvers.

A verifier for automated and interactive proofs about transition systems.

A Lean tactic for Canonical, a search procedure for terms in dependent type theory.

Armv8 Native Code Symbolic Simulator in Lean

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

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

Framework for specifying and proving properties—such as robustness, fairness, and interpretability—of machine learning models using Lean 4.

The Hitchhiker's Guide to Logical Verification and Associated Materials (2024 Edition)

Experiments with SAT solvers with proofs in Lean 4

LLVM support for the lean theorem prover

Lean for Scientists and Engineers, course taught in Summer 2024

SMT-based reasoning core for Lean4

zkLean is a domain specific language (DSL) in Lean for specifying zero-knowledge statements

A template repository with an example of using Veil verifier as a Lean library.