Lean 4 programming language and theorem prover

White-box automation for Lean 4

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

Catalog Of Math Problems Formalized In Lean

A Lean library for Computer Science

Lean 4 port of Iris, a higher-order concurrent separation logic framework

Document Generator for Lean 4

Learn Lean 4 with PLFA proofs.

maze game encoded in Lean 4 syntax

Draft mechanized soundness proof for variants of the capture calculus