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.
600 of 636 projects
Clear searchA fork of openai/miniF2F adapted to Lean 4, with corrections to formalizations and informal descriptions. for human readers.
Declarations not yet indexedLean 4.27.0
Pinned Reservoir package record · checked 2026-07-25
Repository hosting resources for the "Lean Tutorial in Vienna" at TU Wien from September 18 to 20, 2024.
Declarations not yet indexedLean 4.16.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Formalization of Iwasawa Theory in LꓱꓯN (tentative)
Declarations not yet indexedLean 4.30.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Verifying curve25519-dalek using Lean
Declarations not yet indexedLean 4.30.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean playground for programming language modeling tooling.
Declarations not yet indexedLean 4.29.0
Pinned Reservoir package record · checked 2026-07-25
Lean coding problem solving challenge website with proof verification
Declarations not yet indexedLean 4.14.0-rc2
Pinned Reservoir package record · checked 2026-07-25
POP Memory Model in Lean
Declarations not yet indexedLean 4.30.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean implementations of things found in Certified Programming with Dependent Types
Declarations not yet indexedLean nightly-2022-06-05
Pinned Reservoir package record · checked 2026-07-25
A Lean 4 library for formal linguistics: semantics, syntax, pragmatics, morphology, phonology, and processing - formalized across competing frameworks for high interconnection density.
Declarations not yet indexedLean 4.32.0
Pinned Reservoir package record · checked 2026-07-25
i18n library for Lean.
Declarations not yet indexedLean 4.31.0
Pinned Reservoir package record · checked 2026-07-25
Plutus Core, CEK Machine in Lean 4, tailored for Blaster usage
Declarations not yet indexedLean 4.24.0
Pinned Reservoir package record · checked 2026-07-25
A certified checker for Datalog entailments, written in Lean
Declarations not yet indexedLean 4.32.0
Pinned Reservoir package record · checked 2026-07-25
SageMath integration for Lean4
Declarations not yet indexedLean 4.25.0
Pinned Reservoir package record · checked 2026-07-25
Information theory and hypothesis testing, in Lean
Declarations not yet indexedLean 4.13.0-rc3
Pinned Reservoir package record · checked 2026-07-25
An introduction to numbers
Declarations not yet indexedLean 4.31.0
Pinned Reservoir package record · checked 2026-07-25
Formalize "Logic Notes" by Lou van den Dries in Lean
Declarations not yet indexedLean 4.20.0-rc5
Pinned Reservoir package record · checked 2026-07-25
a Lean wrapper for the MD4C Markdown parser
Declarations not yet indexedLean 4.29.0-rc1
Pinned Reservoir package record · checked 2026-07-25
GOOSE in Lean4
Declarations not yet indexedLean 4.22.0
Pinned Reservoir package record · checked 2026-07-25