Lean 4 programming language and theorem prover

The math library of Lean 4

A Lean companion to Analysis I

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

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.

Natural Number Game

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

The Lean Computer Science Library (CSLib)

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

Combinatorial game library in Lean 4

Simple Raycasting Example in Lean4 using SDL3

Formalization of "Analysis I" by Terence Tao

Lean formalisation of parts of Imperial College London's Introduction to University Mathematics course

A Henkin-style completeness proof for the modal logic S5

Lean 4 library of mathematics independent of Mathlib for autodidactic purposes.