Lean LMFDB Bridge Project

This repository contains a Verso blueprint for formalizing definitions within the L-functions and modular forms database. You can view the rendered blueprint at cbirkbeck.github.io/LeanBridge.

The process for updating the contents of this blueprint is different than most other blueprints, because it is built to improve the integration between Mathlib and the LMFDB. While there is some framing content manually written in content.tex, most of the blueprint is generated from the LMFDB's knowl database using the update script, whose output convert_knowls.py turns into the chapters of the Verso blueprint.

Thus most of the work in updating this blueprint takes the following form:

1. Adding definitions and theorems to mathlib

2. Linking definitions in LMFDB knowls to mathlib using the DEFINES macro, and linking theorems using the cite command. Editing and creating knowls requires an account on the LMFDB; contact David Roe or Andrew Sutherland on Zulip (either LMFDB or Lean) if you want to get involved.

3. Once definitions have been added to mathlib and linked in the corresponding knowl, refresh the knowl folder and the Verso chapters (see Updating the blueprint) and make a PR to this repository.

Linking to Mathlib

The overview above describes the workflow; this section collects the practical details for its key step — matching an LMFDB definition or theorem to the right Mathlib declaration and recording the link.

Finding the Mathlib declaration

Before defining anything yourself, check whether Mathlib already has it:

• Loogle — search by name fragment, type pattern, or conclusion (e.g. NumberField.discr, ClassGroup _).
• LeanSearch — natural-language search (e.g. "discriminant of a number field").
• Mathlib docs — the full API, with a search box.
• In the editor — hover over a name for its type and docstring, and use exact? / apply? to let Lean find a matching lemma.

For example, for a number field K:

LMFDB concept	Mathlib declaration
Degree over ℚ	Module.finrank ℚ K
Discriminant	NumberField.discr K
Ring of integers	NumberField.RingOfIntegers K (𝓞 K)
Class group / number	ClassGroup (𝓞 K) / NumberField.classNumber K
Unit rank / regulator	NumberField.Units.rank K / NumberField.Units.regulator K
Galois	IsGalois ℚ K

If it genuinely isn't in Mathlib yet, it must first be added to Mathlib.

Recording the link

Link the declaration from the corresponding LMFDB knowl: use the DEFINES macro for definitions and the cite command for theorems (see the LMFDB knowl guidelines for the exact syntax). Editing or creating knowls requires an LMFDB account — contact David Roe or Andrew Sutherland on Zulip (LMFDB or Lean) to get involved. Finally, refresh the blueprint (see Updating the blueprint) and open a PR.

Local setup

1. Install Lean by following the Lean installation guide, and clone this repository.

2. Download Mathlib's and Tau Ceti's compiled files, then build:

   lake exe cache get
   export LAKE_CONFIG=$PWD/scripts/tauceti-cache.toml
   lake cache get --service tauceti-public --repo TauCetiProject/TauCeti --package TauCeti --mappings-only
   lake build

   lake build builds LeanBridge.lean, a curated import of the library. To build every hand-written module, as CI does, run ./scripts/build-modules.sh; it leaves out the generated level-one certificates, the lookup demo (which queries the LMFDB over the network) and one experiment. With LAKE_CONFIG set to scripts/tauceti-cache.toml, the build fetches the Tau Ceti modules that LeanBridge imports from Tau Ceti's public cache instead of compiling them.

Updating the blueprint

The update script downloads the knowls from a public mirror of the LMFDB database, so it needs Python with NetworkX and psycopg2:

pip install networkx psycopg2-binary
cd blueprint/src
python update_knowls.py
cd ../..
python blueprint-verso/scripts/convert_knowls.py

update_knowls.py rewrites the knowl folder, definitions.txt, edges.txt and the auto_*.tex chapter lists. convert_knowls.py turns these into the chapters in blueprint-verso/LeanBridgeBlueprint/Chapters.

Each chapter entry links its Lean declarations with (lean := ...): the Mathlib declarations that the knowl records with DEFINES(..., mathlib=...), followed by the declarations listed for it in blueprint/src/lean_links.json: Tau Ceti and LeanBridge ones, which knowls cannot link, and Mathlib ones for knowls that do not record them yet. That file maps each knowl to {declaration: module}; the converter imports the modules into the generated Prelude.lean. For this the blueprint project depends on LeanBridge, so it uses the same toolchain. To check that the site builds, run lake exe cache get and then ./scripts/ci-pages.sh in blueprint-verso/; the site is written to blueprint-verso/_out/site/html-multi/.

Repository layout

• LeanBridge.lean: the root import of the library. Its header lists the Tau Ceti declarations that LeanBridge uses for LMFDB elliptic-curve knowls instead of its own copies.
• LeanBridge/ForMathlib: formalisations of the blueprint's LMFDB knowls on top of Mathlib and Tau Ceti, laid out as Mathlib's own directories. Each declaration's docstring names its knowl, and blueprint/src/lean_links.json links the knowls to them.
• LeanBridge/LMFDB: LMFDB-specific material: certificates for LMFDB number fields and level-one newforms, and tactics that query the LMFDB.
• LeanBridge/IdealArithmetic: vendored from CertifyingInvariantsNF: certified rings of integers, discriminants, class groups and Galois groups of number fields.
• LeanBridge/Lookup: the lookup tactic, which searches the LMFDB for a counterexample to the goal.
• LeanBridge/Spec: specifications, with sorry, of objects not yet defined: modular curves, Shimura curves and Hilbert modular surfaces.
• blueprint/src: the knowls as LaTeX, the update script, its definitions.txt and edges.txt, and lean_links.json.
• blueprint-verso: the Verso blueprint project, which depends on LeanBridge for its links to Lean declarations.
• scripts: build-modules.sh, tauceti-cache.toml (Tau Ceti's public build cache, for LAKE_CONFIG), and the Sage scripts that generate the level-one certificates.
• widget: the JavaScript of the LMFDB search widget.
• home_page: the Jekyll home page of the old LaTeX blueprint site, no longer deployed.
• .github/workflows: build.yml builds the Lean library with scripts/build-modules.sh; blueprint.yml builds the Verso blueprint and deploys it to GitHub Pages; create-release.yml tags a release when lean-toolchain changes on main; update.yml updates the dependencies when run by hand.