The math library of Lean 4

A Lean companion to Analysis I

Scientific computing in Lean 4

The Lean Computer Science Library (CSLib)

White-box automation for Lean 4

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

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

Building the natural numbers in Lean 3. The original natural number game, now frozen. See README for Lean 4 information.

Tactics for discharging Lean goals into SMT solvers.

Formalising Mathematics; a course for undergraduate mathematicians. Ran between January and March 2024.

Lean Library currently studying for a degree at Imperial College

Helper toolkit for creating your own Lean 4 UserWidgets

A simple REPL for Lean 4, returning information about errors and sorries.

Some Lean tutorials

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

Lean 3 material related to Imperial College's "Introduction to University Mathematics" course

A simple raytracer written in Lean 4

The matrix cookbook, proved in the Lean theorem prover

A sudoku game where you have to prove that your deductions are valid

Logic and Mechanized Reasoning

Tools based on AI for helping with Lean 4

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

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

Companion files for Logical Verification 2020–2021 at VU Amsterdam

SampCert : Verified Differential Privacy

tool for turning Lean proofs into Blender animations