In this project, I provide a complete, human-readable description for every one of Mathlib4's 9,150 modules — the mathematics library of the Lean 4 proof assistant — stating what each module contains, who uses it, and, wherever the names alone would leave it ambiguous, how it differs from its similarly named neighbors. Coverage is total rather than representative: every directory and every file, described against one fixed, fully specified reference snapshot, released as an independent, open-source resource for the Lean and Mathlib community — not an official product of either. Every entry in this glossary, without exception, is checked against the actual Mathlib4 source at the reference snapshot (Lean 4.29.1, Mathlib4 commit 1ad783f9bf, 2026-05-09): of 9,150 entries, 9,107 carry Complete status and 43 carry Benchmark Theorem status; zero are Pending, and zero are Needs Review. Ismail's Glossary covers the full Mathlib4 hierarchy — 1,129 directories and 8,021 files across six depth levels, spanning all 32 of Mathlib's top-level mathematical domains, from algebra and analysis to category theory and measure theory. Each entry carries six structured fields (path, name, type, parent path, depth, description), so the same data serves a human reader and a retrieval pipeline equally well.The Glossary JSON. The complete dataset, all 9,150 entries, in machine-readable form for any AI platform or retrieval pipeline.The RAG JSON. A flat, embedding-ready export with each entry pre-merged into a single field, for retrieval-augmented-generation systems that want a drop-in data source.The Claude Skill. A self-contained bundle that installs the glossary as an active, queryable reference inside Claude, so Mathlib navigation answers are grounded in current data rather than a language model's frozen training-time memory.The Master Spreadsheet. The live, community-editable source of truth, with a static snapshot published alongside it for anyone who needs a fixed, citable copy.The Interactive Website. A searchable glossary tree plus a dedicated visual Atlas of all 32 top-level domains, built for orientation rather than lookup, alongside a Lean 4 syntax reference and a getting-started guide. To this project's knowledge, no existing Mathlib tool — declaration search engine, in-editor tactic, or auto-generated documentation — provides complete, structural, plain-language coverage of the library at this depth; each presupposes that the user already knows, at least approximately, what they are looking for. All data is provided in full transparency and community contribution is actively encouraged: the complete glossary, every deliverable described above, and the moderated contribution workflow are at github.com/M-Ismail-ZA/IsmailsGlossary. For any feedback, corrections, or collaboration, please contact me via the email address listed on the paper.
Muhammed Ismail (Sat,) studied this question.