Lean 4 programming language and theorem prover

The math library of Lean 4

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

Scientific computing in Lean 4

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

White-box automation for Lean 4

A simple raytracer written in Lean 4

A formal proof of the independence of the continuum hypothesis

Helper toolkit for creating your own Lean 4 UserWidgets

Natural Number Game

A gamification of the theorems in MATH40002 Analysis 1

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

Document Generator for Lean 4

A project to digitalise results from high energy physics into Lean.

Learn Lean 4 with PLFA proofs.

Ground Zero: Lean 4 HoTT Library

Datatypes as quotients of polynomial functors

Reference compiler for c0

Formalizing Euclidean Geometry in Lean

A blueprint for a formalization of infinity-cosmos theory in Lean.

Lean4 backend using `libgccjit`!

A toy implementation of the EVM in Lean4.

A calculus of constructions in Lean

Json Schema lean implementation