Shared evidence about Mathlib's probability theory

Lean checks every proof, but not whether a definition, or the statement of a theorem, says what was meant. That takes someone reading it. This demo collects such readings of Mathlib's probability theory (reviews, reported problems, questions and proposed tests), shows them beside the code, and shares them with the libraries built on Mathlib. It is made with the open tools of LeanTrustBuilders.

Three views of Mathlib's probability theory

Where the evidence is kept

Each review, problem, question or test is a record: a line of JSON in a git repository, the library's evidence store. The records about Mathlib's probability theory are in the Mathlib probability store. A record names its declaration by a hash of what the declaration means. So a page can tell whether a review still applies to the current code or was made on an earlier version, and the record applies in every library that uses the declaration.

Shared with the libraries built on Mathlib

Two libraries built on Mathlib have stores too: the Tau Ceti store and the LeanMachineLearning store. The three stores import each other. A review of a Mathlib definition filed in any of them shows on every page where the definition is used, marked with the store it comes from.

• Only what applies is shown. The Tau Ceti store's records about Tau Ceti's own declarations, for example, are not in the views of Mathlib's probability theory.
• Each store keeps its rules. Only a record's own store, or its author, can withdraw it or mark a problem fixed.
• The reader decides whether it counts. A switch in the reader's policy says whether reviews from imported stores count towards a claim's coverage.
• Nothing is copied. Each build reads the stores it imports afresh, at a commit it shows (below), and does not follow their own imports. The rules are S3's imported records.

Add a record

Anyone with a GitHub account can review a declaration, report a problem, ask a question or propose a test, with a store's issue forms (the Mathlib probability store's, for Mathlib's probability theory), or the buttons in each view. A bot turns the issue into a record, and the views are rebuilt. Records are never anonymous: each names the GitHub account it came from, and an AI agent's are labelled as such.

How it is made

Each piece is open, in its own repository of LeanTrustBuilders, and they fit together through three specifications, so that any of them can be replaced by another tool that follows them.

1. Mathlib, read by Lean. The extractor (trust-extract) reads the compiled library at one commit into a dataset: every declaration, with hashes of what it means, the graphs of what each one rests on, and facets such as docstrings, statements taken apart and where each is written. It can also have Lean's kernel check each declaration against only what the graph says it rests on. Mathlib Explorer, a site for reading Mathlib, extracts a dataset for each Mathlib release and keeps it as a release of its repository; this demo uses those. The Mathlib catalogue, a Lean package that states the domains and characterizations of Mathlib's definitions from outside Mathlib, has a dataset of its own, merged into Mathlib's.
2. The specifications. specs: S1 names a declaration as it was (its name at a commit, and hashes of its meaning), S2 is the dataset, and S3 the evidence records and stores, with the rubric a review says what it checked against.
3. The evidence. A store is the directory evidence/ of a repository: the Mathlib probability store is mathlib-probability-evidence's. evidence-store turns the issues opened with a store's forms into records, keyed by the declaration's hashes in the dataset, checks every change to the store, and fetches the stores it imports. evidence-core reads the records against the dataset: whether each still applies to the current code, what changed underneath it, whether a claim is covered under a reader's policy, and what to review next.
4. The front ends. referee-site builds the Referee site and the claim's page, and the index that trust's front end (trust-web) reads. Each library's views are built in the repository of its store, from its dataset, its store and the stores it imports: those of Mathlib's probability theory by mathlib-probability-evidence's Pages workflow, after every new record; Tau Ceti's by reviewed-by-pilot; and LeanMachineLearning's by its own CI, in LeanMachineLearning/LML.

The design behind the suite is in LeanTrustBuilders/design.

The records

Every record of the Mathlib probability store, and the records of the Tau Ceti and LeanMachineLearning stores about Mathlib's declarations.