Lean 4 programming language and theorem prover

The math library of Lean 4

Bug-free machine learning on stochastic computation graphs

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

Scientific computing in Lean 4

The "batteries included" extended library for the Lean programming language and theorem prover

White-box automation for Lean 4

A zero-knowledge Lean4 compiler and kernel

Benchmark for undergraduate-level formal mathematics

An introduction to theorem proving in Lean for the impatient.

Intuitive, type-safe expression quotations for Lean 4.

Code samples for Lean 4

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

embedding MLIR in LEAN

A formal verification of Linear PCP SNARKs.

Proof artifact co-training for Lean

Reference compiler for c0

A WebAssembly implementation in Lean4

A formally verified compiler for a simple language with numbers and sums

Superposition prover

An LLVM interface for Lean 4. (WIP)

Tool for compiling Lean to WASM

Program Specification in Lean 4

A Lean 4 library for iterators.

Basic Unicode support for Lean 4

Supplemental material for the "Beyond Notations" paper