Package metadataLean library
leanaide
Tools based on AI for helping with Lean 4
Declarations not yet indexedLean 4.28.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.
600 of 636 projects
Clear searchPackage metadataLean tool
Cli
A Lean 4 library for configuring Command Line Interfaces and parsing command line arguments.
Declarations not yet indexedLean 4.33.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
plfl
Learn Lean 4 with PLFA proofs.
Declarations not yet indexedLean 4.31.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
Putnam2025
Our solutions to Putnam 2025.
Declarations not yet indexedLean 4.21.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
Project
A template for blueprint-driven formalization projects in Lean.
Declarations not yet indexedLean 4.28.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
Intuitive, type-safe expression quotations for Lean 4.
Declarations not yet indexedLean 4.33.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
CombinatorialGames
Combinatorial game library in Lean 4
Declarations not yet indexedLean 4.31.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean library
junk-theorems
A small collection of formally verified junk theorems provable in Lean4 + Mathlib.
Declarations not yet indexedLean 4.26.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean library
lnsym
Armv8 Native Code Symbolic Simulator in Lean
Declarations not yet indexedLean nightly-2024-10-07
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
sampcert
SampCert : Verified Differential Privacy
Declarations not yet indexedLean 4.29.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataTeaching project
lean-math-workshop
数学系のためのLean勉強会
Declarations not yet indexedLean 4.26.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean tool
Hammer
LeanHammer is an automated reasoning tool for Lean that brings together multiple proof search and reconstruction techniques and combines them into one tool.
Declarations not yet indexedLean 4.32.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
sparkle
A type-safe, formally verifiable HDL compiler in Lean 4. Inspired by Clash, built for high-assurance hardware synthesis.
Declarations not yet indexedLean 4.28.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean tool
animate
tool for turning Lean proofs into Blender animations
Declarations not yet indexedLean 4.26.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
evmyul
Executable formal model of the EVM and Yul in Lean 4.
Declarations not yet indexedLean 4.22.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataTeaching project
tactic-programming-beginner-guide
Beginner's guide to Tactic Programming in Lean
Declarations not yet indexedLean 4.30.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Tutorial
Package metadataLean library
LeanTool
A "code intepreter" for Lean
Declarations not yet indexedLean 4.26.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean tool
egg
A deprecated equality saturation tactic for Lean based on egg.
Declarations not yet indexedLean 4.30.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean package