Lean 4 programming language and theorem prover

The math library of Lean 4

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

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

A project to digitalise results from physics into Lean.

Scientific computing in Lean 4

Metamath Zero specification language

The "batteries included" extended library for the Lean programming language and theorem prover

Lean Library currently studying for a degree at Imperial College

Formalization of Mathematical Logic

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

A simple raytracer written in Lean 4

Interactive neural theorem proving in Lean

Natural language tactics to teach mathematics using Lean 4

**(Deprecated: Merged into Lean 4)** Lean 4 build system and package manager with configuration files written in Lean.

Armv8 Native Code Symbolic Simulator in Lean

A small collection of formally verified junk theorems provable in Lean4 + Mathlib.

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

A formalized proof of Carleson's theorem in Lean

A formal consistency proof of Quine's set theory New Foundations

HoTT in Lean 3

Code samples for Lean 4

Formalisation of the Cambridge Part II and Part III courses Graph Theory, Combinatorics, Extremal and Probabilistic Combinatorics in Lean

comparative formalizations of the Yoneda lemma for 1-categories and infinity-categories

A quick reference for mapping Coq tactics to Lean tactics

Building group theory from scratch in Lean

A WIP definitional (co)datatype package for Lean4