Beyond Mathlib
Browse 636 source-backed Lean ecosystem records from curated repositories and a pinned Reservoir snapshot. Exact Therefore declaration coverage is labelled separately from package and repository discovery.
Reservoir index b6ac225af74c backs 600 directory records. Provider metadata is discovery evidence, not proof verification or authorship.
433 of 636 projects
Clear search⚗️ | Soma is a general-purpose dependently-typed functional programming language powered by Interaction Nets with a minimal runtime.
Declarations not yet indexedLean 4.30.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Verina (Verifiable Code Generation Arena) is a high-quality benchmark enabling a comprehensive and modular evaluation of code, specification, and proof generation as well as their compositions.
Declarations not yet indexedLean 4.18.0
Pinned Reservoir package record · checked 2026-07-25
maze game encoded in Lean 4 syntax
Declarations not yet indexedLean 4.22.0-rc2
Pinned Reservoir package record · checked 2026-07-25
verification toolchain for TypeScript (Tech Preview)
Declarations not yet indexedLean 4.24.0
Pinned Reservoir package record · checked 2026-07-25
RealAnalysisGame
Declarations not yet indexedLean 4.26.0
Pinned Reservoir package record · checked 2026-07-25
An auto-active verifier embedded into Lean
Declarations not yet indexedLean 4.24.0
Pinned Reservoir package record · checked 2026-07-25
A formal verification of Linear PCP SNARKs.
Declarations not yet indexedLean 4.30.0
Pinned Reservoir package record · checked 2026-07-25
Experiments with SAT solvers with proofs in Lean 4
Declarations not yet indexedLean 4.8.0
Pinned Reservoir package record · checked 2026-07-25
LeanArchitect extracts a blueprint directly from Lean source.
Declarations not yet indexedLean 4.32.0
Pinned Reservoir package record · checked 2026-07-25
TypeScript compiler and JavaScript engine in Lean
Declarations not yet indexedLean 4.29.0
Pinned Reservoir package record · checked 2026-07-25
This package provides an interface and foundation for verified SAT reasoning
Declarations not yet indexedLean nightly-2024-08-02
Pinned Reservoir package record · checked 2026-07-25
🌐 | HTTP primitives for Lean 4
Declarations not yet indexedLean 4.8.0
Pinned Reservoir package record · checked 2026-07-25
Towards Formalizing RL Theory
Declarations not yet indexedLean 4.22.0-rc3
Pinned Reservoir package record · checked 2026-07-25
Markdown file of the list and explanations of all mathlib4 tactics
Declarations not yet indexedLean 4.0.0-rc4
Pinned Reservoir package record · checked 2026-07-25
computable implementation of real numbers in Lean4
Declarations not yet indexedLean 4.17.0-rc1
Pinned Reservoir package record · checked 2026-07-25
A WIP definitional (co)datatype package for Lean4
Declarations not yet indexedLean 4.25.0
Pinned Reservoir package record · checked 2026-07-25
SMT-based reasoning core for Lean4
Declarations not yet indexedLean 4.24.0
Pinned Reservoir package record · checked 2026-07-25
Cryptographic routines for the Lean 4 language
Declarations not yet indexedLean nightly-2023-04-20
Pinned Reservoir package record · checked 2026-07-25