Package metadataLean tool
MutualInduction
A mutual induction tactic for Lean 4.
Declarations not yet indexedLean 4.32.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Beyond Mathlib
The Lean research ecosystem, in one directory.
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.
35 of 636 projects
Clear searchPackage metadataLean tool
lean2wasm
Tool for compiling Lean to WASM
Declarations not yet indexedLean 4.6.1
Pinned Reservoir package record · checked 2026-07-25
Wasm
Package metadataLean tool
lean-slides
A tool to auto-generate and render slides from Markdown comments in the Lean editor.
Declarations not yet indexedLean 4.29.0-rc6
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean tool
leaff
Leaff is a diff tool for Lean environments
Declarations not yet indexedLean 4.11.0-rc3
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean tool
mdgen
Tool to generate markdown files from lean files.
Declarations not yet indexedLean 4.33.0-rc1
Pinned Reservoir package record · checked 2026-07-25
CliMarkdown
Package metadataLean tool
ELFSage
A toy ELF parser/validator
Declarations not yet indexedLean nightly-2024-10-07
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean tool
partax
Lean 4 library of tools for parsing and compiling syntax and parser definitions.
Declarations not yet indexedLean 4.3.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean tool
MD4Lean
a Lean wrapper for the MD4C Markdown parser
Declarations not yet indexedLean 4.29.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean tool
kimina
A Lean tactic that invokes the Kimina Prover Preview model to offer proof suggestions.
Declarations not yet indexedLean 4.18.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean tool
Parse
🧩 | Parser generation for Lean 4.
Declarations not yet indexedLean 4.8.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean tool
leansec
Total parser combinators library for Lean4
Declarations not yet indexedLean 4.20.0-rc5
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean tool
lapis
✏️ | A cutting-edge, concurrent & performant Language Server Protocol (LSP) framework for Lean 4.
Declarations not yet indexedLean 4.30.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean tool
UnicodeSkipListTableExample
A library that shows how to use the Unicode skip list tables generation tool to create a table to test if a codepoint is numeric.
Declarations not yet indexedLean 4.10.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean tool
webeditor
Helper tool for projects run in lean4web
Declarations not yet indexedLean nightly
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean tool
sos
A Lean 4 sum-of-squares tactic for nonlinear real arithmetic.
Declarations not yet indexedLean 4.31.0
Pinned Reservoir package record · checked 2026-07-25
MathReal ArithmeticSoftware VerificationTactic
Package metadataLean tool
Quave
Quantum Hoare Logic Lean 4 - A quantum program verification tool
Declarations not yet indexedLean 4.16.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean tool
leaner
🪶 | A linter, formatter and whole-program dead code eliminator for Lean 4
Declarations not yet indexedLean 4.29.0
Pinned Reservoir package record · checked 2026-07-25
Lean package