Lean 4 programming language and theorem prover

The math library of Lean 4

A Lean companion to Analysis I

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

White-box automation for Lean 4

The Lean Computer Science Library (CSLib)

💧 Liquid Tensor Experiment

Source code for the Mathematics in Lean tutorial.

The matrix cookbook, proved in the Lean theorem prover

Learn Lean 4 with PLFA proofs.

Write C shims from within Lean code.

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

Lean 函数式编程

Lean 4 port of Megaparsec

Lean 定理证明

📚 (WIP) Formal proofs of "An Infinitely Large Napkin"

Lean 4 元编程