Lean 4 programming language and theorem prover

The math library of Lean 4

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

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

A project to digitalise results from physics into Lean.

A minimal development of SSA theory

A verifier for automated and interactive proofs about transition systems.

Loom is a framework for automated generation of foundational multi-modal verifiers. This repository is a mirror with stable snapshots. Submit issues and PRs here.

Course notes for Formalising Mathematics 2025

A verified tensor library in Lean

Formalization of DBSP