Awesome Lean Programming

Dependently typed functional programming language and interactive theorem prover.

Lean 4 is largely written in Lean, it compiles to C, and it can prove things about the programs you write in it. Most existing lists focus on formalized mathematics. This one looks at Lean from a programmer's point of view: libraries, tooling, program verification, interop, and software that people have actually built.

• Official
• Learning Resources
• Editors & Environments
• Build, Packaging & CI
• Developer Tools
• Testing
• Libraries
  • Standard Library Extensions & Data Structures
  • Parsing & Text
  • Serialization
  • Web & Networking
  • Databases
  • Cryptography & Compression
  • Date & Time
  • CLI & Terminal
  • Effects, Concurrency & Streams
  • Graphics, GUI & Games
  • Mobile
  • Scientific Computing & Machine Learning
  • FFI & Language Interop
  • Hardware & Embedded
  • Metaprogramming & DSLs
• Automation, Solvers & Tactics
• Program Verification
• Compilers, Kernels & Language Implementations
• AI & Agent Tooling
• Applications & Showcases
• Community

Core projects maintained by the Lean FRO and the Lean community.

• Lean 4 - The compiler, language server, the Lake build system, and the standard library (Std: async I/O, TCP, HTTP, Std.Time, hash maps, iterators, and more).
• elan - Toolchain manager for Lean, similar to rustup.
• Reservoir - Package registry and index for Lean packages.
• Batteries - "Batteries included" extended library with data structures, utilities and tactics beyond core.
• Lean 4 Web - Online Lean editor running in the browser (source).
• Lean on Compiler Explorer - Inspect the IR, C and assembly that Lean generates on godbolt.org.
• Verso - Documentation authoring tool used for the Lean manual, books and websites, with elaborated and highlighted Lean code (website).
• doc-gen4 - API documentation generator for Lean 4 packages.
• CSLib - The Lean Computer Science Library: algorithms, semantics, automata, and models of computation.

Books & Guides

• Functional Programming in Lean - The standard introduction to Lean as a programming language.
• Theorem Proving in Lean 4 - Dependent type theory and proofs in Lean.
• The Lean Language Reference - The official reference manual.
• Metaprogramming in Lean 4 - Book on macros, elaborators, tactics and the MetaM stack.
• From Zero to QED - Informal introduction to Lean 4 for programmers.
• Lean by Example - Lean and its main libraries explained through code examples (Japanese).
• Lean (meta-)programming Cookbook - Recipes for common programming and metaprogramming tasks.
• Tactic Programming Guide - Beginner's guide to writing tactics.
• Lean Symbol Reference - Searchable list of Unicode symbols and their input abbreviations.
• Lean Snippets - Functional programming patterns in Lean 4, from lazy evaluation and continuations to category-theory-inspired techniques.

Programming Languages & Verification

• Software Foundations in Lean - The Software Foundations textbooks, being translated from Rocq to Lean.
• Programming Language Foundations in Lean - Learn Lean 4 with PLFA.
• Essentials of Compilation in Lean - An incremental compiler following "Essentials of Compilation".
• CPDT in Lean - Lean implementations of material from "Certified Programming with Dependent Types".
• Aeneas Tutorial - Verifying Rust programs in Lean with Aeneas (ICFP tutorial).
• Human-eval-lean - Hand-written, verified Lean solutions to the HumanEval benchmark, useful as idiomatic examples.

Practice

• leetproof.org - Practice platform with Lean challenges and community solutions.

• vscode-lean4 - Official VS Code extension with infoview, widgets and Unicode input.
• lean.nvim - Neovim support for Lean 4, including an infoview.
• lean.vim - Port of lean.nvim to Vim.
• lean4-mode - Emacs major mode for Lean 4.
• lean-ts-mode - Tree-sitter-based Emacs mode.
• tree-sitter-lean - Tree-sitter grammar for Lean 4.
• lean4ij - IntelliJ platform plugin for Lean 4.
• acme-lsp-lean - Lean support for the Acme editor.
• lean-tui - Terminal infoview built with Ratatui, driven by an LSP proxy.
• xeus-lean - Jupyter kernel for Lean 4 built on the xeus protocol.
• lean4_jupyter - Jupyter kernel for Lean 4 using the REPL.
• ProofWidgets4 - Build custom interactive UI widgets (React) for the infoview.
• bubble - Open Lean projects and PRs in sandboxed VS Code containers so untrusted code can't touch your machine.
• Paperproof - Infoview that shows proofs as pen-and-paper-style trees.

• lean-action - GitHub Action to build, test and lint Lean projects.
• LeanProject - Repository template with CI, docs and blueprint setup.
• lean-update - GitHub Action to keep Lean toolchains and dependencies up to date.
• hopscotch - CLI that bisects a dependency version range to find where your project breaks (action).
• lev - Package and toolchain manager for switching between Lean projects and versions, inspired by uv.
• lean4-nix - Nix flake for Lean 4 and lake2nix.
• rules_lean - Bazel rules for Lean 4 and Lake, focused on cross-language native builds.
• setuptools-lean - Plugin for setuptools that packages Python modules written in Lean.
• lean-churn-bot - Opens PRs that fix upstream breakage using only compiler suggestions, no LLM.
• intentions - GitHub Action for claiming issues and reporting who is working on what.
• lean-optimizations - Proposed optimizations that speed up builds and interactive use (paper).

Documentation & Literate Programming

• Verso Slides - Verso genre for reveal.js slide decks with checked Lean code.
• SubVerso - Extracts highlighted Lean code for use in Verso and other tools.
• mdgen - Generates Markdown files from Lean sources.
• LiterateLean - Files that are valid Markdown and valid Lean at the same time, with no preprocessor.
• lean-slides - Renders reveal.js slides from Markdown comments inside the infoview.
• LeanTeX - DSL for writing LaTeX Beamer presentations in Lean.
• versotreedoc - Generates a Verso document skeleton that mirrors a source tree.
• doc-verification-bridge - Documentation tool that extracts verification relationships from Lean code.
• lean-i18n - Translate Lean projects with PO files.

Formatting & Linting

• leanfmt - Structure-preserving code formatter.
• lean-fmt - Code formatter and linter with editor and CI integration.
• leaner - Linter, formatter and whole-program dead-code eliminator.
• lint-llm-proofs - Linters for patterns common in LLM-generated proofs.

Analysis & Inspection

• import-graph - Analyze and visualize a package's import structure (lake exe graph).
• jixia - Static analysis tool that extracts declarations, dependency graphs and tactic states.
• FlameTC - Flame graphs for debugging type class synthesis performance.
• leaff - Diff tool for Lean environments.
• lean4export - Plain-text export of declarations for external checkers and tools.
• ast_export - Exports Lean 4 ASTs.
• lean2sexp - Converts .olean files to s-expressions.
• NodeGraph - Generates dependency graphs between declarations.
• lean4-dep-audit - Traces a constant's transitive dependencies down to axioms, externs and their C sources.
• Lean Fuzz - Grammar-based fuzzing for Lean DSLs, using parser tables extracted from the compiler.

Kernels & Proof Checking

• lean4checker - Replays an environment to check that the kernel accepts every declaration (archived).
• Comparator - Checks that a solution proves exactly the stated challenge theorem, using only allowed axioms.
• Lean Kernel Arena - Test suite and leaderboard for independent Lean kernel implementations (source).
• SafeVerify - Robustly checks submitted proofs and implementations against a reference.
• axiom-audit - Axiom allowlist check that fails CI on sorry, native_decide or custom axioms.

• Plausible - Property-based testing and counterexample search.
• LSpec - Specification testing framework.
• nest - Extensible test framework inspired by Haskell's tasty (unit tests).
• LTest - Fixture-based test framework in the style of pytest.
• LeanTest - Unit testing framework with a wide range of assertions.
• lean4-assert-command - Simple #assert command for inline checks.

• LeanColls - Collections library with a uniform interface.
• hashbrown4lean - Port of Rust's hashbrown SwissTable hash map.
• CCtx - First-class constructor contexts for writing tail-recursive builders.
• itertools - Iterator library.
• ac-library - Port of AtCoder Library for competitive programming.
• Algorithm - Verified efficient algorithms.
• pod - Low-level utilities: single-precision floats, byte spans, unboxed vectors, finalizers.
• bitmap - Image utilities with verified PNG encoding and decoding.

• lean4-parser - Parser combinator library.
• Megaparsec.lean - Port of Haskell's Megaparsec.
• prim-parser - Total parser combinators whose termination is guaranteed by graded monads.
• leansec - Total parser combinators.
• Partax - Compiles Lean syntax and parser definitions into standalone parsers.
• lean-regex - Regular expression engine with correctness proofs.
• Regex - PCRE2-compatible regular expression engine.
• UnicodeBasic - Basic Unicode character properties.
• lean-markdown - CommonMark and GFM implementation that passes the official test suites and is proved total and HTML-safe.
• lean4-markdown - Typed DSL for building and rendering Markdown documents.
• MD4Lean - Wrapper for the MD4C Markdown parser.
• L4YAML - YAML 1.2.2 parser and dumper with verified properties.
• lean-url - URL parsing based on the WHATWG standard.
• lean-semver - Semantic versioning.
• printiest - Pretty printer library.
• BibtexQuery - Command-line BibTeX query utility.

• lean-json - JSON library with no partial functions or panics, proved against the RFC 8259 grammar, with small binaries.
• lean4-json-schema - Derives JSON Schema from types, with kernel-checked proofs that serialization validates.
• protobuf - Protocol Buffers implementation.
• binary - Serialization and deserialization of binary data, inspired by Haskell's binary.
• LeanSerde - Serialization framework with deriving handlers.
• ln-messagepack - MessagePack serialization in pure Lean.
• lean4-base64 - RFC 4648 Base64 encoding and decoding.
• protovalidate-lean - Turns CEL constraints on protobuf fields into refinement types.
• leanxml2 - libxml2 bindings: DOM parsing, namespaces, serialization and XPath.

Servers & Frameworks

• LeanIO - HTTP router for Std.Http with compile-time checked routes, JSON handling and middleware.
• LeanTEA - Full-stack web and TUI framework based on The Elm Architecture.
• Qed - Frontend framework with JSX-style components, typed events and state invariants proved at compile time.
• lean-html - Typed HTML5 (lean-htmx adds typed hx-* attributes).
• lean-routing - Typed router and route table.
• lean-middleware - Sessions, sealed cookie store, anti-forgery, static files and request tracing.
• lean-forms - Web forms library.
• lean-authentication - Magic-link authentication, sessions and rate limiting.
• datastar-lean - Datastar SDK for real-time hypermedia apps over server-sent events, with optional compression.
• LeanRPC - Expose Lean functions as JSON-RPC endpoints over HTTP with @[rpc].
• lithe - Simple web service framework.
• LeanAPI - API server in the style of Express and FastAPI, with typed routing, field-level validation errors, middleware and auth (experimental).

Protocols & Clients

• socket.lean - BSD socket bindings.
• http2-lean - HTTP/2 protocol foundation and managed transports.
• ws-lean - WebSocket protocol and networking library.
• LeanWs - WebSocket library (RFC 6455) in pure Lean over Std.Http.Transport, with a server and a client.
• tls13-lean - TLS 1.3 client and server built on HACL* verified crypto primitives.
• grpc-lean - Protobuf code generation and a gRPC client/server runtime.
• lean-grpc - Pure Lean gRPC stack (HTTP/2, HPACK, gRPC).
• leancurl - libcurl bindings (see also leanCurl).
• LeanHttp - HTTP and WebSocket client in Std.Http's own types, backed by libcurl (TLS, redirects, HTTP/2).
• lean-llmclient - Provider-agnostic LLM chat client with tool calling.
• lean-mcp - Model Context Protocol server library for writing MCP servers in Lean.

Cloud & Observability

• lean-aws - AWS SigV4 signing (lean-aws-lambda implements the Lambda runtime interface).
• lean-telemetry - OpenTelemetry traces and logs.
• otel-lean - OpenTelemetry logs API, proved batch SDK and OTLP exporters.
• infra - Terraform-style infrastructure as code with dependent types.
• iam-lean - Formal models of AWS IAM policies (catalog).

• leansqlite - SQLite bindings from the Lean FRO.
• leanpostgres - libpq bindings with a connection pool, in the style of leansqlite (leanmigrate runs plain-SQL migrations).
• lean-pq - libpq bindings with a pq! query DSL: columns are checked against the schema at compile time, values always become parameters, and read, write and DDL permissions are tracked in types.
• pg-lean - PostgreSQL client with a pure Lean wire protocol, SCRAM, TLS, COPY and pipelining.
• lean-pgx - Checked Lean types and query runners generated from PostgreSQL DDL and SQL.
• lean-linq - Type-safe LINQ-style SQL query DSL that compiles to parameterized SQL.
• LeanDB - Strongly typed SQL over SQLite: the compiler checks query inputs and result types, and schema changes produce migration plans.
• LeanMySQL - MySQL API.
• lean-redis - Async Redis client written in pure Lean on the Std TCP stack.
• redisLean - Bindings to the hiredis Redis client.
• mini-redis - Implementation of the mini-redis server.

• leancrypto - Pure-Lean SHA-2, HMAC, RSA signature verification, DER and encodings, with proofs that the encodings round-trip.
• leancrypto (Theoric) - OpenSSL-backed SHA-256, HMAC, secure random bytes and scrypt password hashing with a ready hash/verify API.
• lean-crypto - Cryptographic routines.
• lean-jose - JSON Web Signature, JSON Web Key and JSON Web Token in pure Lean.
• jose-libcrypto - OpenSSL backend for lean-jose that adds ECDSA, EdDSA and asymmetric signing.
• lean-libcrypto - Bindings to OpenSSL 3's libcrypto through its generic EVP interfaces.
• Blake3 - Bindings to the BLAKE3 hash function (see also Blake3Lean4, a pure Lean implementation).
• OpenSSL.lean - OpenSSL bindings.
• lean-cryptolib - Verified Montgomery and Barrett modular reduction.
• lean-zip - Pure-Lean DEFLATE and zlib with a kernel-checked proof that decompression inverts compression (blog post: "Why Lean is faster than Rust").
• lean-zlib - Bindings to system zlib for zlib, gzip and raw DEFLATE streams, plus CRC-32 and Adler-32.
• lean-zstd - Zstandard decompression, via C bindings or a pure-Lean implementation with proofs.
• lean-archive - Tar and ZIP archives, hardened against hostile input.
• lean-brotli - Brotli bindings with whole-buffer and streaming APIs.
• LeanHuffmanCoding - Huffman coding with correctness proofs.
• LeanBWT-Bzip2 - bzip2 via the Burrows-Wheeler transform, in pure Lean with proofs.

• Std.Time - Dates, times, time zones and formatting in the core standard library.
• DateTime - ISO 8601 date and time utilities.
• timelib - Date and time library.
• time - Port of Haskell's time library, with verified date calculations.

• lean4-cli - Configure command-line interfaces and parse arguments (used by Lake).
• Leansi - Terminal formatting.
• Pigment - Terminal colors and styling.
• asciiplot - Plot functions as ASCII art in the infoview.

• flow - Reactive streams (Flow, SharedFlow, StateFlow).
• Straume - Streams library.
• lean-eff - Small extensible-effects library.
• lean-effects - Algebraic effects.
• lean-reducers - Parallel, fused reducers.
• EffSpec - Effect monads with specifications (Dijkstra monads).
• lentil - Compile-time dependency injection.
• lean-cloud - Parallel and distributed programming with monadic workflows over shared blob storage.

• lean-sdl3 - SDL3 bindings.
• lean-sdl3 (philnguyen) - Comprehensive SDL3 bindings (lean-compose-ui is a cross-platform UI library built on them).
• SDL.lean - SDL2 bindings.
• Raylib.lean - Bindings to the raylib game library.
• raylean - Bindings to the raylib game library.
• lean-vulkan - Proof-of-concept Vulkan bindings.
• lean-wgpu - WebGPU bindings via wgpu-native.
• Hesper - Verified GPU programming with type-safe WebGPU shaders.
• LeanPlot - Plotting with deterministic SVG and PNG backends.
• Illuminate - Compositional 2D diagrams rendered to SVG, with previews in the infoview (experimental).
• vizagrams - Visualization library.
• LeanReact - Write React components in Lean that compile to JavaScript (experimental).
• lean4-godot - Experimental bindings to the Godot 4 game engine.

• lean-ios - Build iOS apps with Lean: patched runtime, SDL3 bindings and build scaffolding.
• lean4-android - Cross-compiles the Lean runtime for Android (aarch64) with the NDK.
• lean-compose - Typed DSL for authoring Jetpack Compose UI in Lean (example app calling Lean over JNI).

• SciLean - Scientific computing: arrays, automatic differentiation and numerical methods.
• TorchLean - Neural networks with typed tensors, autograd, CUDA support and verification.
• TensorLib - Verified tensor library.
• Tables - Dataframe library compatible with the B2T2 benchmark, with provable invariants.
• Hex - Verified computational algebra: matrices, row reduction, polynomial factoring, LLL, graph isomorphism.
• lp - Verified linear programming solver that returns proof-carrying results, plus an lp tactic.
• LeanBLAS - BLAS bindings with specifications.
• EigenLean - Eigen linear algebra bindings.
• NumLean - Numerical matrix computations.
• FloatLib - Verified floating-point arithmetic across formats.
• FloatSpec - Formally verified float implementation.
• fp-lean - Floating-point semantics mechanization.
• LeanCert - Verified interval arithmetic: bounds, root finding and optimization.
• interval - Conservative floating-point interval arithmetic.
• lean-units - SI physical unit system.
• lean-autograd - Automatic differentiation following JAX's autodidax.
• lean4-mlir - Neural architectures specified in Lean, with verified GPU codegen.
• ginac-lean - GiNaC computer algebra bindings.
• LeanSage - Call SageMath from Lean.
• Tgrad - Demo bf16 matrix-multiply runtime on Apple Silicon Metal, owned by Lean and driven from Python.

• Alloy - Write C shims inline in Lean code.
• lean-sys - Rust bindings to the Lean runtime (lean-rs is a safe wrapper).
• RustFFI.lean - Template for Lean-Rust FFI.
• Nerodia - Write Python modules in pure Lean, inspired by PyO3 (preview, Lean FRO).
• lean.py - Two-way Lean/Python interop with automatic marshalling.
• Extism Lean SDK - Call WebAssembly plugins from Lean.
• lean-bindgen - Generates @[extern] declarations and C shims from a concise spec of a C header.

• Sparkle - Type-safe, verifiable HDL compiler inspired by Clash.
• Circuitlib - Digital circuit verification using categorical semantics.
• LNSym - Armv8 native-code symbolic simulator.
• MRiscX - Certified RISC-V interpreter with Hoare logic.

• Qq - Intuitive, type-safe expression quotations.
• Thyme - Typed, staged metaprogramming with dependent types and reasoning about metaprograms.
• Leanduction - Generates usable induction principles for nested inductive types.
• MutualInduction - Mutual induction tactic.
• QPF - (Co)datatype package built on quotients of polynomial functors.
• Coinductive - Library for coinductive types built on polynomial functors, used to define interaction trees.
• leanses - Lenses with custom notation.
• lean-subst - Substitution library inspired by Autosubst.
• HexLuthor - Hex color literal syntax with inline VS Code preview.
• Imperia - Alternative do notation for imperative code over non-monadic types (experimental).
• LeanBitsyntax - Erlang-style <<...>> bit syntax for building and matching BitVec values (experimental).

Tactics and solver integrations that are useful when proving properties of programs.

• grind - Built-in SMT-style tactic combining congruence closure, E-matching and arithmetic.
• bv_decide - Built-in bit-blasting decision procedure for BitVec goals, backed by a verified SAT proof checker (LeanSAT).
• Aesop - White-box, rule-based proof search.
• lean-smt - Discharge goals to SMT solvers with proof reconstruction.
• lean-cvc5 - FFI bindings to the cvc5 SMT solver.
• lean-auto - Interface between Lean and automated theorem provers.
• Duper - Superposition-based automatic prover.
• LeanHammer - Hammer combining premise selection, ATPs and proof reconstruction.
• Canonical - Exhaustive term search in dependent type theory.
• Leanwuzla - Connects bv_decide to SMT-LIB.
• Blaster - SMT-based reasoning core.
• egg - Equality saturation tactic based on egg (deprecated).
• OptiSat - Verified equality saturation engine.
• Saturn - SAT solvers with proofs.
• trestle - SAT utilities: encodings, solver APIs, and file format parsers and printers.
• CLeanGo - Bindings and DSL for the Clingo answer set programming solver.
• waterfall - ACL2-style proof search for inductive goals.
• sos - Sum-of-squares tactic for nonlinear real arithmetic.
• SmtLibDsl - Typed SMT-LIB DSL with backends for Z3, cvc5, Kissat and CaDiCaL.
• cpsat - Bindings to the OR-Tools CP-SAT constraint solver.
• deriving such that - Port of Rocq's program derivation tactic.
• BetterFind - Extended #find for searching declarations by pattern, closer to Rocq's Search.

Frameworks

• Std.Do / mvcgen - Built-in monadic program logic and verification condition generator for do code.
• Loom - Framework for building multi-modal verifiers of effectful programs.
• Velvet - Auto-active program verifier.
• Veil - Automated and interactive verification of distributed protocols and transition systems.
• Iris-Lean - Port of the Iris higher-order concurrent separation logic framework.
• Lentil - LTL reasoning infrastructure.
• LeanSSR - SSReflect-style tactic language.
• lean-machines - Modelling and refinement of stateful systems.
• leanSpec - Program specification in Lean 4.
• WybeCoder - Agentic verified imperative code generation on Loom/Velvet.

Verifying Other Languages

• Aeneas - Translates safe Rust to Lean for verification.
• hax - Extracts Rust code to Lean (and other backends).
• Strata - Platform for formalizing language syntax and semantics through extensible dialects and building automated reasoning tools on them.
• LemmaScript - Verification toolchain for TypeScript (tech preview).
• rust-lean-models - Lean models of Rust standard library functions.
• ACL2Lean - Replay ACL2 proofs as kernel-checked Lean theorems.
• Talos - WebAssembly interpreter and weakest-precondition calculus for verifying WebAssembly modules.
• lean-mlir - MLIR semantics and verified peephole rewrites.

Semantics & Specifications

• Wasm.lean - WebAssembly implementation.
• lean-wasm - Formalization of the WebAssembly spec.
• haskell-spec - Formal specification of the Haskell Language Report.
• graphql-lean - Formalization of the GraphQL specification.
• ELFSage - ELF parser and validator.
• SHerLOC - StableHLO analyzer.
• TenCert - Verified tensor compilation.
• graphiti - Verified graph rewriting for dataflow circuits.
• lean-yjs - Verification of the Yjs CRDT integration algorithm.
• langlib - Esoteric programming languages, formally.

Industrial & Security

• cedar-spec - Lean specification and verification of AWS's Cedar authorization language, used for differential testing of the production implementation.
• SampCert - Verified differential privacy, used in production by AWS Clean Rooms.
• VCVio - Machine-checked cryptographic proofs with oracle computations.
• DyLean - Symbolic analysis of cryptographic protocols.
• verified-3d-mesh-intersection - Verified 3D constructive solid geometry.
• bitrep - Rust crate for bit-identical float reductions, with the merge algebra proved in Lean.

Blockchain & Zero Knowledge

• EVMYulLean - Executable formal model of the EVM and Yul.
• evm-smith - Framework for AI systems to write EVM bytecode and prove it safe.
• Blanc - Minimal EVM contract language, with proofs about the deployed bytecode.
• Clean - DSL for ZK circuits with soundness and completeness proofs (zk.golf).
• ArkLib - Formally verified arguments of knowledge.
• zkLean - DSL for specifying zero-knowledge statements.
• risc0-lean4 - Model of the RISC Zero zkVM.
• aegis - Verify Cairo contracts.
• btc-verified - Verified Bitcoin serialization, txids and Merkle commitments.

• lean4lean - Lean 4 kernel written in Lean 4.
• nanoda - Independent Lean 4 type checker written in Rust.
• con-leche - External Lean checker with a consistency proof (con-ron is a Rust port proved with Aeneas).
• Metalean - Verified type checker for an idealized Lean type theory.
• Lean4Less - Translates Lean into smaller theories by eliminating definitional equalities.
• lean2agda - Exports elaborated Lean code to Agda.
• thales - TypeScript compiler and JavaScript engine in Lean.
• leanexe - Compiler for a Lean dialect that targets verified WebAssembly.
• lean2wasm - Compile Lean to WebAssembly.
• lean-vir - Runs Lean in the browser via Lean's IR interpreter compiled to WebAssembly, with a runtime under 200 KiB (early, Lean FRO).
• lean-gccjit - Bindings to libgccjit, a basis for alternative backends.
• QED64 - Lean and Mathlib running in the browser via wasm64.
• yatima - Zero-knowledge Lean 4 compiler and kernel.
• ix - Zero-knowledge proof-carrying code for Lean 4.
• mm-lean4 - High-performance Metamath verifier.
• Soma - Dependently typed language powered by interaction nets.
• lapis - Concurrent Language Server Protocol framework.
• qdt - Query-based dependent type elaborator.
• DeBruijnSSA - Formalization of SSA.
• verified-compiler - Toy verified compiler.
• Lyre - Write Lean IR as Lean syntax.
• LRT - Model of Lean's runtime primitives in Lean, partly porting the C runtime (work in progress).
• LeanPy - Experimental implementation of Python in Lean.

Agents & MCP

• lean-lsp-mcp - MCP server that gives agents diagnostics, goals, hovers and search through the Lean LSP.
• lean4-skills - Claude Code skills and plugins for Lean work.
• Lean Beam - Extends the Lean LSP server for agent- and tool-driven workflows.
• LeanTool - "Code interpreter" for Lean that LLMs can call.
• AXLE - Axiom's Lean engine for proof verification, manipulation and runtime tasks (MCP).
• Archon Horizon - Workspace-first orchestration for long-running Codex or Claude Code sessions on Lean.
• Archon - Multi-agent coding and proving workflows over a Lean project, driven by blueprint DAGs.
• Lean skills - Official agent skills for proofs, toolchain setup, bisection and more.
• LeanSlop - Call LLMs from inside Lean code as black-box automation.
• Aristotle - Harmonic's formal reasoning agent, available via web, CLI and API.

Programmatic Access to Lean

• REPL - JSON REPL that reports errors, sorries and proof states.
• Pantograph - Machine-to-machine interaction interface for Lean 4.
• PyPantograph - Python interface to Pantograph.
• leanclient - Drive Lean from Python via the LSP.
• Kimina Lean Server - Fast, scalable server for checking Lean code in batches.
• LeanDojo - Extract data from and interact with Lean repositories programmatically.
• LeanCopilot - LLMs as copilots inside Lean.
• llmlean - LLM tactic suggestions from local or cloud models.

Search

• Loogle - Search declarations by name, type pattern or constant (web).
• LeanSearchClient - #search syntax for LeanSearch, Loogle and LeanStateSearch from the editor.
• LeanExplore - Semantic search engine with an MCP server.

Verified Code Generation Benchmarks

• Verina - Benchmark for verifiable code generation (code, specs and proofs).
• CLEVER - Curated Lean benchmark for verified code generation.
• Vericoding - Tools and benchmarks for verified coding.
• SorryDB - Continuously updated benchmark built from sorrys in real projects.

Apps & Services

• lean-todomvc-max - Production-style TodoMVC with passwordless sign-in, migrations, telemetry, an LLM panel and AWS Lambda deployment.
• LeanToDo - Web app built with leansqlite, Verso and htmx.
• lean-acme-widgets - CRUD service combining gRPC, refinement-typed protobuf validation, PostgreSQL and TLS.
• viper - Python environment manager written in Lean.
• lean4-raytracer - Simple raytracer.
• Shirika-RPC - TypeScript worker RPC library whose protocol layer is checked in Lean.

Games

• flappy - Clone of Flappy Bird built with raylean.
• LeanDoomed - Raycasting demo using SDL3.
• lean4-maze - Maze game encoded in Lean syntax.
• Chess.lean - Chess in Lean 4.
• ChessProver - Chess engine with a theory for proving endgame statements.
• PuzzleLean - PuzzleScript engine: play grid puzzles in the infoview and prove them solvable.
• EleanvatorSaga - Elevator Saga played in the infoview.
• lean-snakebird - Snakebird implementation.
• Functorio - Build Factorio factories in Lean with types, functions and recursion.
• lean4game - Engine and server for interactive Lean games (live).
• LeanChess - Chess server where the rules are a Lean program and each game is a fold over its move log (live).

• Lean Zulip - Main community chat; see the #Project announcements, #Program verification and #lean4 channels.
• Lean Community website - Community resources, installation guides and documentation overview.
• Leangineer Discord - Chat for software engineers building with Lean, alongside leangineer.com.
• Lean FRO - The Focused Research Organization developing Lean, including roadmaps.
• Awesome Logic Formalization - Related list about formalized logic.

Contributions welcome! Read the contribution guidelines first.

Most entries were collected from project announcements on the Lean Zulip, mainly the #Project announcements, #AI authored projects, #Program verification and #General announcements channels. Thanks to everyone who shares their work there. Many others come from the Reservoir package index.