Lean 4 programming language and theorem prover

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

Demo for high-performance type theory elaboration

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.

💧 Liquid Tensor Experiment

Lean Library currently studying for a degree at Imperial College

Some Lean tutorials

A formal proof of the independence of the continuum hypothesis

A simple raytracer written in Lean 4

Perfectoid spaces in the Lean formal theorem prover.

M4 algebraic geometry course in Lean

An experimental category theory library for Lean

repository for material for Jan-Mar 2023 course on formalising mathematics

Datatypes as quotients of polynomial functors

Some examples of Lean projects, for undergraduate mathematicians.

Formal verification of parts of the Stacks Project in Lean

Extra and extended datatypes for Lean 4

Learning material for mathematicians who want to learn Lean

Formalization of the proof of ABC conjecture for polynomials (Mason-Stothers theorem) in Lean 4

Experiments in algebraic geometry as part of the EPSRC Taught Course Centre course on formalising number theory and geometry

Some experiments with the Lean proof assistant

Describes formalization of p-adic L-functions in Lean 3

Learning metric spaces by doing them in Lean!