← lean-pkg documentation

What a lean-pkg page lets you believe, what it asks you to take on trust, and how to check it yourself.

This page is for a referee or reader who meets a Lean verification page made with lean-pkg and wants to know how much it is worth. It is written from the code: each check is named by the module and function that enforces it (cli is src/lean_pkg/cli.py, and so on), so it can be read. Where lean-pkg relies on honesty rather than on a check, it says so.

The short version: lean-pkg checks that its evidence files agree with one another and with one git commit. It does not re-run Lean when it validates a receipt. A receipt is an unsigned record of a run, not a proof. The proof is the Lean source at the bound commit, and the only way to remove trust in the person who ran the checks is to run them again, which the last section shows.

What each artifact certifies

Artifact Certifies (checked by lean-pkg) Does not certify Trusted
Lower-tier gate receipt (.lean-receipts/<c12>-<job>.json) binds one commit X; its lean_toolchain equals lean-toolchain committed at X and its mathlib_rev the Mathlib rev in lake-manifest.json at X; sorry_count is 0; axioms is a subset of the allowed set (default propext, Quot.sound, Classical.choice); with the additive claim_axioms key, the axioms of every claim in claims.yaml at X (none missing, none on sorryAx, the rest allowed); HEAD is X or an admitted descendant (cli.validate_receipt); its redacted verify log <c12>-<job>-verify.redacted.log (or .gz) is present and hashes to report_sha256 (cli.report_log_check): a receipt whose log is missing or unreadable is refused by gate, gate --check and every consumer of a recorded receipt (the claims ledger and so promote, next, comparator, palomar prepare, index add and index check) that the build actually ran: the counts are copied from a log the executor wrote; anything about statements the executor (person, script, host) that ran lake build and #print axioms and wrote the log
Slurm receipt (receipt slurm) at writing time only: sacct showed the job COMPLETED with exit 0:0 (receipt.check_job); the job’s stdout seal matches the log byte for byte and lake-manifest.json was unchanged during the job (receipt.check_stdout); stderr was empty; the log shows a finished build and no module restored from Lake’s cache anything after writing: gate never runs sacct again, and a reader cannot, since accounting is private to the cluster. job_id: slurm-<J> is a string; nothing outside the cluster ties it to a real job the person who ran receipt slurm, the cluster’s accounting, and the account that ran the job
systemd receipt (receipt systemd --run) the unit’s recorded terminal state, exit 0, no restart, resource caps, and a clean checkout at X before and after the run (receipt_systemd.check_unit); the host appears only as a hashed label that the host is any particular machine the person and the host that ran it
Comparator receipt (lean-pkg receipt comparator, schema comparator-receipt/2) lists exactly the comparator*.json configurations tracked at X; each configuration’s bytes and fields equal the receipt’s; each log hashes to log_sha256 and contains the full line Your solution is okay!; permitted axioms within the allowed set; tool pins well-formed; both tiers bind the same commit (cli.validate_comparator, cli.comparator_pass). When the runner wrote it, lake comparator checked, for every theorem_names entry, that the Solution proves exactly the Challenge statement with only the permitted axioms, and replayed the proof in Lean’s kernel and in independent kernels (NanoDa and con-ron for the toolchain mechanism; nanoda for legacy). A Slurm claim (job_id J, host_policy Slurm job J ...) counts only with its slurm_sacct seal: lean-pkg receipt comparator --seal-sacct found J COMPLETED with exit 0:0 in a window containing the run, under the sealing account and on the receipt’s node where known, and the sealed record committed beside the receipt still hashes and parses to that (receipt.sacct_seal_problem) validation re-reads hashes and the PASS line; it does not re-run the comparator (promote says so: “not re-run”). That the Challenge says what the paper says. Theorems not listed in a configuration. The body of a definition hole (definition_names). An unsealed Slurm claim: it is only the SLURM_JOB_ID the shell had the comparator and the kernels; the person who wrote the Challenge; the runner of lean-pkg receipt comparator
Olean manifest (olean_manifest in the comparator receipt) the runner refused the run if the package’s compiled modules under .lake/build/lib changed between the build stage and the end of the comparison (comparator_receipt.check_oleans) no validator reads it after the run; it is a statement by the runner about its own run the runner
Definition-hole sign-off (lean-pkg-signoff.json) a non-empty reviewer name that is not a model or agent token, a date, and config_sha256 equal to the configuration’s bytes at X, covering every hole (holes.check_definition_holes, holes.check_reviewer) that the reviewer exists, read the bodies, or judged them correctly: “This is a declaration, not a verification” the named human reviewer
coverage.yaml rows, and the rule R11 the file is strict coverage/1; each claim a row names is in claims.yaml at HEAD with its file committed; every theorem the recorded comparator receipt compared is the declaration of a claim some row names (R11, coverage.scope_problems); a compute job is backed by a committed receipt with job_id: slurm-<J>, or by a comparator receipt whose Slurm claim carries a valid sacct seal (coverage.compute_backing, coverage.slurm_job_of) the class (same-assumptions, inputs-supplied, outside), the summary and the notes are the authors’ words; that a row’s Lean statement matches the paper’s result the authors
Verification page (lean-pkg page) every number and status word is rendered from the data above; the word verified appears only when the claims ledger at the promote stage closes the row, and a row says its statement was compared only when a passing comparator configuration at the gate-bound commit judged every claim it names (page._row_compared); the Lean statement shown is read from the source at the gate-bound commit (the Challenge module when the comparator compared it), or the file is linked when it cannot be read reliably (page._lean_statement, lean_scan.statement); page --check fails when the README block differs from a fresh render (page.render_all, page.readme_problems) the page renders the receipts; it does not validate them again (that is gate, comparator and index check) and does not run Lean. Its first line tells the reader which statements to compare by eye (page.TRUST_LINE), and What the checks establish says what no tool checks. The paper statement (paper.statement in coverage.yaml) is the authors’ transcription, not checked against the manuscript lean-pkg’s renderer, and the registry record it reads (status, recorded receipts)
Index entry (index/<name>/entry.yaml) index check --clone clones the repository, checks out the pin and runs the same validators as gate and comparator on the receipts as first committed in the pin or an evidence-only descendant; the index copies equal those bytes; trust is recomputed and must equal the stated one; comparator trust needs every headline judged (index.check_entry, index.derive, index.compute_trust) as for the receipts it carries; Palomar and Reservoir lookups are skipped, not failed, when the network is unreachable; the DOI is checked for form only the receipts’ authors; the git host; Palomar’s API
Palomar (index trust palomar, record palomar-registered) an entry is graded palomar when it lists a Palomar id; index check fetches the entry and refuses one registered for another commit or repository (index.network_checks) lean-pkg runs Palomar’s checks only as a prediction (palomar check, “predictive, non-authoritative”); with no network the id is not verified; compute_trust grades palomar before looking at the other tiers Palomar’s verifier and registry
Publication hold (update --withdraw-publication) while it is set, promote and the promote checklist of publish refuse (cli.promote_checklist), and next recommends nothing to publish it does not unpublish anything: a repository once public may have been cloned or forked the owner who set it; the registry file

The trust chain

A page made with lean-pkg is only as good as each of these. Each is named with what it is trusted for.

  1. The Lean kernel. Lean’s own kernel accepted the proofs during the build. For the comparator tier, the proofs were also replayed in a second, independently written kernel (NanoDa, and con-ron for the toolchain mechanism; the pinned nanoda for legacy), so a bug in one kernel alone does not pass.
  2. The comparator (lake comparator from the project’s own toolchain, or the pinned leanprover/comparator for legacy). Trusted to compare the exported Challenge and Solution statements correctly and to enforce the permitted axioms. lean-pkg vendors the driver scripts (scripts/verify-comparator.sh, scripts/comparator-check.sh) with their local changes listed in their headers.
  3. The toolchain pin. lean-toolchain at the bound commit names the Lean release; every validator compares the receipt against it (cli.check_toolchain_at). The toolchain itself is downloaded by elan and trusted as released, kernel included.
  4. The toolchain advisories. Lean releases occasionally ship with a kernel or runtime soundness bug that a later point release fixes. lean-pkg ships a dated list of them, toolchain-advisories.yaml, each entry citing the Lean release notes and the lean4 issue or pull request. gate, gate --check, receipt check and palomar check print a WARN line (and list toolchain_advisories in --json) when the toolchain is on it, and the page says so under How this was checked (never a reason for page --check to call a page stale). A warning, never a refusal: the proofs may well be sound, and the comparator tier’s independent kernels catch several of these bugs. The list is trusted to be complete only as far as its maintainers have read upstream; a toolchain not on it is not thereby certified.
  5. The Mathlib pin. lake-manifest.json at the bound commit pins Mathlib to a commit. Mathlib’s own proofs are checked by the same kernels when the package is built against it; its definitions are trusted to mean what their names say, which is the same trust every Mathlib user extends.
  6. The person running the gate. The lower-tier receipt is written from a log the executor’s script produced. lean-pkg checks the log’s internal consistency and binding, not that Lean produced it. A Challenge statement is chosen by a person, and its fidelity to the paper is a human judgement. With the claim_axioms key, the axioms of every claim come from core Lean’s collectAxioms run on the built environment after the build, not only from the #print axioms text of the theorems someone printed; the lines are in the same sealed log, so they rest on the same executor.
  7. The host. The receipts were produced on some machine. A compromised host can produce any log. The systemd and comparator receipts name the host (as a hashed label or a chosen public label), which identifies it but does not vouch for it.
  8. Git history. Commits are identified by SHA-1 object names, and every binding (receipt to commit, descendant rules, config and log bytes) is judged on git objects, never on the working tree. lean-pkg does not check commit signatures.
  9. The git host and Zenodo. The public repository host keeps the commits available; index add refuses a pin no public branch contains. A Zenodo DOI names an archived release and the commit it was cut from; lean-pkg records the DOI and that commit and checks their form, but does not download the archive and compare it.

Positioning against Lean’s own checks

Lean v4.35.0 (2026-10-12) ships lake check, which replays a build’s export through Lean’s kernel and refuses non-standard axioms, and lake comparator; with --paranoid both also run the independent kernels the toolchain now bundles. Those are items 1 and 2 of the chain above, and lean-pkg does not compete with them: its toolchain comparator mechanism already runs lake comparator. What a check run does not do is say which commit, toolchain and Mathlib pin it judged, who ran it and where, whether its Challenge is the result the paper claims, or how a referee re-checks it later. Those are lean-pkg’s receipts, coverage rows, page and receipt check. lean-pkg will consume lake check as a receipt producer once its result can be bound to a commit (v4.35.0 documents no machine-readable report), and will then drop what it duplicates. The FAQ entry What does lean-pkg add now that Lean has lake check --paranoid? separates what has shipped from what the Lean FRO has announced.

Threats

Covered

Not covered: lean-pkg relies on honesty here

Re-verify a page yourself

Do not take a receipt’s word for it: run the checks again.

You need only the public repository, a Linux machine, the Lean toolchain the package pins (elan installs it), bwrap for the comparator, and lean-pkg (pipx install git+https://github.com/lean-pkg/lean-pkg.git). No lean-pkg registry and no lab account. These steps were run end to end on a small package with no Mathlib; with Mathlib add lake exe cache get before each build.

1. Clone and find the bound commit. The page’s Reproduce section prints it as git checkout <X> # the commit the build check binds (pages written before 0.11: # the commit the gate receipt binds).

git clone https://github.com/OWNER/REPO && cd REPO
X=<the 40-hex commit from the page>
git merge-base --is-ancestor "$X" HEAD && echo "HEAD descends from X"
git diff --no-renames --name-status "$X" HEAD     # what changed after the gate

Everything listed must be evidence (.lean-receipts/) or, for a package that opted in to the docs-only rule, files the build does not read (the README, coverage.yaml, notes). A .lean file, a lakefile, lake-manifest.json or lean-toolchain in that list means the page describes an older source than HEAD.

2. Check the pins.

git show "$X":lean-toolchain
git show "$X":lake-manifest.json | python3 -c 'import json,sys; print([(p["name"], p.get("rev")) for p in json.load(sys.stdin)["packages"]])'

They must equal lean_toolchain and mathlib_rev in the receipts, and the toolchain and Mathlib lines of the page.

3. Check the receipt hashes. The page’s Evidence table gives the SHA-256 of each committed receipt:

sha256sum .lean-receipts/*.json

Then let lean-pkg’s own validators check the receipts, with no registry, no network and no Lean run:

lean-pkg receipt check --repo . --commit "$X"
lean-pkg receipt check --repo . --commit "$X" --json      # every check with its verdict

It runs gate’s and comparator’s validators on a private clone of the checkout, at X and at HEAD (--at REF for a tag or another ref), and prints one line per check, PASS, FAIL or SKIP (not applicable, with the reason), then the verdict. receipt check: PASS NAME at <X> (tier comparator; ...) means: the lower-tier and comparator receipts bind X, HEAD is X or an evidence-only descendant of it (only .lean-receipts/ changed, and formalization.yaml in its derived keys only, the same exemption gate applies; the result prints exemption applied: ... when it was needed), the toolchain and Mathlib pins agree with lean-toolchain and lake-manifest.json at X, every configuration, log and redacted log hashes to what the receipts say and each log has its PASS line, the comparator configurations at X name every reusable theorem claim (by the naming rule, or by the claim’s explicit judged_as, checked against the configurations), coverage.yaml accounts for every compared theorem (R11), and the page block states exactly what the receipts record. The table of checks is in Checking a published package’s receipts. Exit 0 only when no check fails.

A tag on the evidence commit itself passes without any option, even though that commit refreshed formalization.yaml. A package that committed its README, coverage.yaml or notes after the evidence (a docs-only descendant) fails the binding check: the author’s opt-in to the docs-only rule is in their registry, which you cannot read. Look at step 1’s list yourself; if every path there is a file the build does not read, re-run with --docs-descendants, and the result says that you accepted that rule.

Steps 1 to 3 establish that the evidence is consistent. They do not establish that a run happened. Steps 4 and 5 do.

4. Rebuild and print the axioms at X, in a fresh clone (no .lake/):

git checkout --detach "$X"
lake build
lake lean Verify/Axioms.lean        # or the package's own #print axioms file

The build must finish with no declaration uses 'sorry' warning, and every #print axioms line must report a subset of the axioms the page lists.

5. Re-run the comparator at X, in the same clean clone:

COMPARATOR_RECEIPT_ALLOW_HOST=1 comparator-receipt --project .

COMPARATOR_RECEIPT_ALLOW_HOST=1 is the explicit authorization for a run outside a Slurm job; it is recorded in your receipt’s host_policy. Add COMPARATOR_RECEIPT_NO_MATHLIB=1 for a package without Mathlib. The run prints one acceptance line per kernel and Your solution is okay! for every configuration, and writes .lean-receipts/<c12>-comparator.json in your clone. Compare it with the published one: the same commit, mechanism, lean_toolchain and tools, and for each configuration the same path, sha256 and theorem_names. Then read Challenge.lean (or the configured challenge module) against the paper: that last step is the one no tool does.

What a third party cannot reproduce