Lean 4 programming language and theorem prover

A Lean companion to Analysis I

Ongoing Lean formalisation of the proof of Fermat's Last Theorem

Scientific computing in 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

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

Theorem Proving in Lean 4

Repository for formalization of the Polynomial Freiman Ruzsa conjecture (and related results)

Source code for the Mathematics in Lean tutorial.

Rewriting Principia Mathematica in Lean

Hitchhiker's Guide to Logical Verification (2023 Edition)

Formalisation of the Cambridge Part II and Part III courses Graph Theory, Combinatorics, Extremal and Probabilistic Combinatorics in Lean

A Cheat Sheet for Coq Developers who want to try LeanProver

Supplement of the ICFP'22 paper "‘do’ Unchained: Embracing Local Imperativity in a Purely Functional Language"

Course repository for GlaMS - Formalising Mathematics in Lean (2024)

Lean formalisation and textbook for Languages and Computation