The v0.1.0 signature-bearing API reference covers all 31 supported modules and 601 supported declarations. Its complete dependency-aware tree is served at the stable versioned route below.

Getting started Entropy, mutual information, and KL Markov chains and data processing Formalizing a research paper LeanInfoTheory and mathlib v0.1.0 API reference Source-derived declaration inventory Module guide Theorem highlights Development Prior art Blueprint Module dependency map Roadmap Documentation provenance License and citation

The signature-bearing reference documents the frozen release API. The current source-derived inventory is supplementary: it includes non-private declarations from non-stable examples and reference anchors as well as the supported library. Use the module guide for import choices and theorem highlights for a curated mathematical map. The versioned API reference is rebuilt from the exact release commit, while the unversioned project pages report the current project state. Current supported coverage is recorded in docs/current-public-api.json. The source index labels its development links explicitly; maintenance staging pins those links to the exact site commit before publication. Current file-linked API docs are inspected locally and cannot be copied into the frozen route.