Lean 4 programming language and theorem prover

The math library of Lean 4

A collection of formalized statements of conjectures in Lean.

Cosette is an automated SQL solver.

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

An introduction to theorem proving in Lean for the impatient.

White-box automation for Lean 4

Lean documentation authoring tool

A minimal development of SSA theory

コード例で学ぶ Lean 言語

Hitchhiker's Guide to Logical Verification (2023 Edition)

The Lean reference manual

A Lean 4 library for configuring Command Line Interfaces and parsing command line arguments.

Intuitive, type-safe expression quotations for Lean 4.

Canonical is a performant sound and complete type inhabitation solver for dependent type theory.

Write C shims from within Lean code.

Ground Zero: Lean 4 HoTT Library

Parser Combinator Library for Lean 4

Files associated with the course Interactive Theorem Proving at LMU SoSe 2024

A WIP definitional (co)datatype package for Lean4

Datatypes as quotients of polynomial functors

Lean 4 port of Megaparsec

Some Lean proofs

Extism Lean4 Host SDK - easily run WebAssembly modules / plugins from Lean4 applications

Total parser combinators library for Lean4

protobuf implementation for Lean 4

a language of the ML family