Lean 4 programming language and theorem prover

The math library of Lean 4

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

A Lean companion to Analysis I

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

A collection of formalized statements of conjectures in Lean.

Demo for high-performance type theory elaboration

A project to map out the relations between different equational theories of Magmas.

Scientific computing in Lean 4

A project to digitalise results from physics into Lean.

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

Natural Number Game

Formalization of Mathematical Logic

Some Lean tutorials

Helper toolkit for creating your own Lean 4 UserWidgets

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

A simple raytracer written in Lean 4

A formal proof of the independence of the continuum hypothesis

Document Generator for Lean 4

Learn Lean 4 with PLFA proofs.

Quantum information theory in Lean 4

A gamification of the theorems in MATH40002 Analysis 1

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

Ground Zero: Lean 4 HoTT Library

M4 algebraic geometry course in Lean

From Zero to QED: An informal introduction to formality with Lean 4