Lean 4 programming language and theorem prover

Lean documentation authoring tool

Tactics for discharging Lean goals into SMT solvers.

A minimal development of SSA theory

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

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

Experiments on automation for Lean

Document Generator for Lean 4

A zero-knowledge Lean4 compiler and kernel

A formal proof of the independence of the continuum hypothesis

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

Intuitive, type-safe expression quotations for Lean 4.

LeanHammer is an automated reasoning tool for Lean that brings together multiple proof search and reconstruction techniques and combines them into one tool.

Write C shims from within Lean code.

Parser Combinator Library for Lean 4

Executable formal model of the EVM and Yul in Lean 4.

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

Markdown file of the list and explanations of all mathlib4 tactics

A WIP definitional (co)datatype package for Lean4

A support library for working with zero knowledge cryptography in Lean 4.

Neural theorem proving toolkit: data extraction tools for Lean 4

Lean 4 port of Megaparsec

Syntax for searching with natural language from Lean, using https://leansearch.net/ (may extend to other services)

A Foreign Function Interface (FFI) to cvc5 solver in Lean.

Verify Cairo contracts in Lean 4

Verification of the gnark implementation of the Semaphore protocol using Reilabs' extractor to Lean.

A Lean 4 library for iterators.