Lean 4 programming language and theorem prover

The math library of Lean 4

Demo for high-performance type theory elaboration

Scientific computing in Lean 4

Simple verification of Rust programs via functional purification in Lean 2(!)

Metamath Zero specification language

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

White-box automation for Lean 4

Tactics for discharging Lean goals into SMT solvers.

An introduction to theorem proving in Lean for the impatient.

Helper toolkit for creating your own Lean 4 UserWidgets

A minimal development of SSA theory

Hitchhiker's Guide to Logical Verification (2023 Edition)

Intuitive, type-safe expression quotations for Lean 4.

Code samples for Lean 4

Very controlled natural language tactics for Lean

LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.

Learn Lean 4 with PLFA proofs.

maze game encoded in Lean 4 syntax

Lean 4 tutorial files

Supplement of the ICFP'22 paper "‘do’ Unchained: Embracing Local Imperativity in a Purely Functional Language"

Materials for my lecture at the 2023 International School on Interactions of Proof Assistants and Mathematics in Regensburg