Lean 4 programming language and theorem prover

The math library of Lean 4

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

Scientific computing in Lean 4

Metamath Zero specification language

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

Building the natural numbers in Lean 3. The original natural number game, now frozen. See README for Lean 4 information.

Natural Number Game

Lean Library currently studying for a degree at Imperial College

Theorem Proving in Lean 4

💧 Liquid Tensor Experiment

Some Lean tutorials

Helper toolkit for creating your own Lean 4 UserWidgets

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

Functional Programming in Lean

Tools based on AI for helping with Lean 4

A quick reference for mapping Coq tactics to Lean tactics

A partial formalization of Geometric Algebra in the Lean formal proof verification system.

Lean 4 tutorial files

Formalization of Gröbner basis theory in Lean4 (WIP)