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.

433 of 636 projects

Clear search
Package metadataLean library

eocia-lean

Essentials of Compilation: An Incremental Approach in Lean 4

Declarations not yet indexedLean 4.16.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

GL

Craig interpolation for GL in Lean

Declarations not yet indexedLean 4.28.0

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataLean library

Heights

An attempt at formalizing the theory of heights in Lean

Declarations not yet indexedLean 4.32.0

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataLean library

ExistentialRules

This repo contains formalizations around Existential Rules (aka. Tuple-Generating Dependencies) with disjunctions and the Chase algorithm. Mostly this will be about (basics of) my own formal works.

Declarations not yet indexedLean 4.32.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

LeanRPC

Serve Lean 4 functions as RPC methods over HTTP

Declarations not yet indexedLean 4.25.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

paranoia

Lean 4 proof verification without reference

Declarations not yet indexedLean 4.25.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

CHANGE

Repository hosting the resources for the Lean demo session of my talk presented at the weekly research seminar on CHallenges in ANalysis and GEometry (CHANGE) at the University of Trento on February 11, 2025.

Declarations not yet indexedLean 4.24.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

import-all

This script can check and auto-generate import statements in a lean4 repository.

Declarations not yet indexedLean 4.33.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

quicksort

Implementation and Formal Verification of the Quicksort Algorithm

Declarations not yet indexedLean 4.30.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

GinacLean

A work-in-progress Lean 4 binding to GiNaC

Declarations not yet indexedLean 4.8.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

lean4-ctypes

FFI for Lean 4

Declarations not yet indexedLean nightly-2023-11-21

Pinned Reservoir package record · checked 2026-07-25

Ffi
Package metadataLean library

AsciiPlot

ASCII/Unicode plotting library for Lean 4 with legends and braille rendering

Declarations not yet indexedLean nightly-2025-01-31

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

chromatic_polynomial

Chromatic polynomial in Lean4

Declarations not yet indexedLean 4.11.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

OpenSSL.lean

OpenSSL bindings for Lean

Declarations not yet indexedLean nightly-2022-09-11

Pinned Reservoir package record · checked 2026-07-25

OpensslOpenssl Bindings
Package metadataLean library

LeanSha256

Pure-Lean SHA-256 reference implementation: NIST CAVP-validated, kernel-reducible, no FFI.

Declarations not yet indexedLean 4.29.1

Pinned Reservoir package record · checked 2026-07-25

CryptographyFips 180 4Lean4Sha256
Package metadataLean library

extra

Supplements to the Lean 4 Standard Library

Declarations not yet indexedLean 4.29.0-rc3

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

Seminar

Past contents of Lean Seminars in Bonn

Declarations not yet indexedLean 4.13.0-rc3

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

mini-redis

An implementation of mini-redis in Lean 4

Declarations not yet indexedLean pr-release-8003

Pinned Reservoir package record · checked 2026-07-25

Lean package