ASPBE Lean Blueprint

1.1. Reader map🔗

Map of the ASPBE Lean library and its two synchronized reader surfaces

There are three useful ways into the formal library:

  1. New to Lean: read this Overview, then Foundations, Routes, and Case Studies. Each curated card explains the mathematical role before showing the checked declaration.

  2. Looking for a result: use the Library Explorer to search every explicit public declaration and filter by catalog, declaration kind, or experimental status.

  3. Auditing a claim: open its Blueprint declaration panel, read the exact hypotheses and conclusion, then follow the repository source link. The Lean signature, not the reader cue, determines what has been certified.

The terms used on this site have narrow meanings. A declaration is a named Lean definition, type, theorem, or lemma. A structure is a record: proposition-valued fields are requirements until a concrete value supplies proofs. A theorem or lemma on the default import surface has a compiled proof. A diagnostic or experimental obligation must not be reported as a certified result.