Lean 4 programming language and theorem prover

Demo for high-performance type theory elaboration

White-box automation for Lean 4

💧 Liquid Tensor Experiment

A simple raytracer written in Lean 4

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

Logic and Mechanized Reasoning

Code samples for Lean 4

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

M4 algebraic geometry course in Lean

A model of the RISC Zero zkVM and ecosystem in the Lean 4 Theorem Prover

embedding MLIR in LEAN

A Testing Framework for Lean

A static analysis tool for Lean 4.

Parser Combinator Library for Lean 4

The standard template to create a lean game

Formalising the WASM spec in Lean

Describes formalization of p-adic L-functions in Lean 3

Where we collect lean4 bugs