Package metadataLean library
LogicQ
An IR language for fault-tolerant quantum programming
Declarations not yet indexedLean 4.29.1
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.
433 of 636 projects
Clear searchPackage metadataLean library
m2r-group-7
Classifying Groups of Order up to 31 in Lean 4 - Imperial Maths Year 2 Research Project Group 7 - 2026
Declarations not yet indexedLean 4.29.1
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean library
advents
Advent of Code
Declarations not yet indexedLean 4.26.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
huffman
Huffman coding in Lean 4 with a formal optimality proof and Unix pack/unpack (.z) compatibility.
Declarations not yet indexedLean 4.31.0
Pinned Reservoir package record · checked 2026-07-25
CompressionFormal VerificationHuffmanPack
Package metadataLean library
delphin
The Lean port of PyDelphin, a library to integrate DELPH-IN toolsets
Declarations not yet indexedLean 4.12.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
VerificationDemo
A temporary repository
Declarations not yet indexedLean 4.13.0-rc3
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
interest
Interest: a Lean library for financial mathematics
Declarations not yet indexedLean 4.31.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
math654
Homework and lecture notes from Math 654, Fall 2022
Declarations not yet indexedLean 4.27.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean library
lean4-project
A minimal Lean 4 development environment using VSCode DevContainer.
Declarations not yet indexedLean 4.28.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
Iterator
In this repository, I work on the Lean iterator library that is supposed to become part of the standard library.
Declarations not yet indexedLean 4.20.0-rc5
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
bppl
Probabilistic Separation Logic
Declarations not yet indexedLean 4.28.0
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean library
Crypto
Implementation of various cryptographic functions in Lean4
Declarations not yet indexedLean 4.7.0
Pinned Reservoir package record · checked 2026-07-25
CryptographyElliptic Curves
Package metadataLean library
Hoare
Hoare Logic in Lean
Declarations not yet indexedLean 4.22.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
FMCn_Lean
Repositório destinado às práticas de Lean4 da Monitoria de FMCn.
Declarations not yet indexedLean stable
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
crup
A Checker for RUP proofs written in Lean 4
Declarations not yet indexedLean 4.3.0
Pinned Reservoir package record · checked 2026-07-25
RupSat
Package metadataLean library
http-client
A Curl wrapper written in Lean 4 to be used as a http-client in lean 4 projects
Declarations not yet indexedLean 4.25.2
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
mathmatic_in_elementary_number_th
初等数论讲义的形式化证明 by lean4
Declarations not yet indexedLean 4.24.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean library
sgc
Lean 4 library characterizing the algebraic structure of metastability and consolidation in stochastic systems
Declarations not yet indexedLean 4.25.2
Pinned Reservoir package record · checked 2026-07-25
Lean package