Lean 4 programming language and theorem prover

Tactics for discharging Lean goals into SMT solvers.

A minimal development of SSA theory

Experiments on automation for Lean

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

A zero-knowledge Lean4 compiler and kernel

A formal proof of the independence of the continuum hypothesis

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

Document Generator for Lean 4

Intuitive, type-safe expression quotations for Lean 4.

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

Write C shims from within Lean code.

Parser Combinator Library for Lean 4

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

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

Markdown file of the list and explanations of all mathlib4 tactics

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

A WIP definitional (co)datatype package for Lean4

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 formal specification of the Yul IR semantics in the Lean proof assistant.

A Lean 4 library for iterators.