Lean 4 programming language and theorem prover

The math library of Lean 4

Lean 3's obsolete mathematical components library: please use mathlib4

Scientific computing in Lean 4

Simple verification of Rust programs via functional purification in Lean 2(!)

White-box automation for Lean 4

Lean 3 material for Kevin Buzzard's 2021 TCC courrse on formalising mathematics. Lean 4 version available here: https://github.com/ImperialCollegeLondon/formalising-mathematics-2024

Tactics for discharging Lean goals into SMT solvers.

Blueprint for the PNT+ Project

Theorem Proving in Lean 4

A verifier for automated and interactive proofs about transition systems.

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

Lean 4 port of Iris, a higher-order concurrent separation logic framework

Document Generator for Lean 4

Formalizing stochastic doubly-efficient debate

**(Deprecated: Merged into Lean 4)** Lean 4 build system and package manager with configuration files written in Lean.

Intuitive, type-safe expression quotations for Lean 4.

A Lean 4 library for configuring Command Line Interfaces and parsing command line arguments.

SampCert : Verified Differential Privacy

Write C shims from within Lean code.

Formally proving the security of Fast Reed-Solomon interactive oracle proofs of proximity

maze game encoded in Lean 4 syntax

LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.

Experiments with SAT solvers with proofs in Lean 4

LLVM support for the lean theorem prover

Materials for the course "theorem prover lab: applications in programming languages" at KIT, SS2021 edition

embedding MLIR in LEAN

A prototype for a monadic program logic in Lean that has since been upstreamed into the Lean 4 repo

An LLVM interface for Lean 4. (WIP)