therefore
Sign up
Open navigation

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 search
Repository catalogLean tool

SciLean

An experimental framework for symbolic and numerical computing, automatic differentiation, differential equations, and optimization in Lean.

Declarations not yet indexedLean 4

Curated repository record · checked 2026-07-25

OptimizationScientific computing
Repository catalogLean tool

TorchLean

Typed tensors, neural-network graph semantics, finite-precision reasoning, runtime integration, and certificate checking.

Declarations not yet indexedLean 4

Curated repository record · checked 2026-07-25

Finite precisionMachine learning
Package metadataLean tool

aesop

White-box automation for Lean 4

Declarations not yet indexedLean 4.33.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean tool

verso

Lean documentation authoring tool

Declarations not yet indexedLean 4.33.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean tool

auto

Experiments on automation for Lean

Declarations not yet indexedLean 4.32.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean tool

loogle

Mathlib search tool

Declarations not yet indexedLean 4.30.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean tool

Canonical

A Lean tactic for Canonical, a search procedure for terms in dependent type theory.

Declarations not yet indexedLean 4.32.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean tool

jixia

A static analysis tool for Lean 4.

Declarations not yet indexedLean 4.29.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package 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 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 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 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
Package metadataLean tool

Parser

Parser Combinator Library for Lean 4

Declarations not yet indexedLean 4.33.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean tool

leanInk

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

Declarations not yet indexedLean 4.6.0-rc1

Pinned Reservoir package record · checked 2026-07-25

AlectryonInteractive Theorem ProvingVisualization
Package metadataLean tool

mathport

Mathport is a tool for porting Lean3 projects to Lean4

Declarations not yet indexedLean 4.10.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean tool

ssreflect

LeanSSR: an SSReflect-Like Tactic Language for Lean

Declarations not yet indexedLean 4.26.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean tool

reap

General neural tactic for Lean 4

Declarations not yet indexedLean 4.28.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean tool

tryAtEachStep

Try a tactic at each step in a Lean proof.

Declarations not yet indexedLean 4.32.0

Pinned Reservoir package record · checked 2026-07-25

Lean package