LeanBridge Blueprint

 LeanBridge Blueprint🔗

Compiled2026-06-18T13:26:52ZProject60527ecblueprint: strip leftover leanblueprint commands (\leanok etc.) from converted knowlsLeanleanprover/lean4:v4.31.0VersoBlueprintv4.31.0@c0b8f77b714f

The plan is to formalize definitions from the L-functions and modular forms database (LMFDB) in mathlib, as well as creating tactics to import relevant data from the LMFDB. This blueprint catalogues the relevant LMFDB definitions, organised into number fields, elliptic curves, and modular forms, with a background chapter for supporting notions. It is migrated from the project's original LaTeX (leanblueprint) document; each definition links back to its LMFDB knowl.

Contents

  1. 1. Background
  2. 2. Number fields
  3. 3. Elliptic curves
  4. 4. Modular forms
  5. Dependency Graph
  6. Blueprint Summary