← lean-pkg documentation

Check intermediate results while the argument evolves, not only the finished paper.

A Lean companion does not have to wait until the manuscript is done. You can formalize a selected intermediate step while the argument is still changing, record exactly what was checked at a stable commit, and carry that evidence forward as the paper evolves. At the end you ship the manuscript, a reproducible companion, and an explicit record of what is and is not covered.

This page is a workflow guide with a small synthetic example. It describes capabilities, not measured results: auditable reuse and more focused review are what the workflow supports; a net speedup or a general reliability gain has not been measured.

Who does what

Layer Responsibility
Lean checks the encoded deduction: the formal statement and its proof
lean-pkg the package, claim and evidence lifecycle: registry, leases, claims, receipts bound to commits, gate, ledger, search
your manuscript workflow (external) writing the paper, keeping statements and formal counterparts aligned, reviewing statement correspondence and the arguments Lean does not cover

lean-pkg does not compare a paper’s prose with a Lean statement, and it does not review mathematics outside the formal statements. Those steps belong to your own review process, whatever tools it uses.

A certificate covers the exact formal statements it records, under their exact hypotheses. It does not certify the surrounding paper.

The layout

Keep the Lean package in its own directory and the working notes outside it (see Progress files live outside the package directory):

telescoping-paper/              the manuscript repository
  paper/telescoping.tex
  progress/                     progress log, wave notes
  lean/                         the package: registered local_path
    lakefile.toml  lean-toolchain  lake-manifest.json  claims.yaml
    coverage.yaml               the paper-to-Lean map (below)
    Telescoping/Basic.lean

1. Register the package and take the lease

lean-pkg register telescoping-companion --repo git@github.com:you/telescoping-paper.git \
  --path src/telescoping-paper/lean --owner-project telescoping-paper
lean-pkg lease claim telescoping-companion --workspace laptop --agent you

2. Pick an intermediate step and search before building

Choose a step the rest of the argument leans on, or one you are unsure of. In the example paper, the main estimate uses the partial sums of 1/((k+1)(k+2)). Search before writing anything:

lean-pkg search "telescoping partial sums" --package telescoping-companion

If the search reports incomplete: searched N of M sources, a zero is not a negative result; search again later or look by hand. For the full discover, pin, check and decide cycle, see Prior-art search: while the paper is being written.

3. State it exactly, with its hypotheses

Write the formal statement with every hypothesis the paper uses, and no more:

theorem Telescoping.sum_inv_mul_succ (n : ℕ) :
    ∑ k ∈ Finset.range n, (1 : ℚ) / ((k + 1) * (k + 2)) = 1 - 1 / (n + 1)

Never assume the result you want in order to get coverage: a hypothesis that restates the conclusion makes the certificate say nothing. When a formal attempt fails, say why before moving on. It may be a wrong formulation, a missing hypothesis, a library gap, or a problem with the build, and only the first two say something about the mathematics.

Declare the result in claims.yaml, and check the file before committing:

schema: claims/1
package: telescoping-companion
claims:
  - id: telescoping-companion/sum-inv-mul-succ
    decl: Telescoping.sum_inv_mul_succ
    kind: theorem
    summary: "For every n, the sum over k < n of 1/((k+1)(k+2)) equals 1 - 1/(n+1)."
    file: Telescoping/Basic.lean
    status: reusable
    keywords: [telescoping, partial-sums]
  - id: telescoping-companion/partial-fraction
    decl: Telescoping.inv_mul_succ_eq_sub
    kind: lemma
    summary: "1/((k+1)(k+2)) = 1/(k+1) - 1/(k+2), the step the main sum uses."
    file: Telescoping/Basic.lean
    status: internal

lean-pkg claims check --file claims.yaml

reusable claims are the ones a later gate requires; internal helpers are still part of the package and its evidence, but are not offered for reuse.

4. Freeze a checkpoint and record evidence

When the step is proved, commit the source and produce a receipt bound to that commit, for example from a capped local run (or receipt slurm on a cluster):

lean-pkg receipt systemd --unit tele-gate --commit "$(git rev-parse HEAD)" --log /tmp/tele/verify.log \
  --stdout /tmp/tele/unit.out --stderr /tmp/tele/unit.err --checker "verify.sh" --run -- bash verify.sh /tmp/tele/verify.log
lean-pkg claims sync telescoping-companion
lean-pkg gate telescoping-companion --check --receipt .lean-receipts/<commit12>-<job>.json
lean-pkg update telescoping-companion --status gate-pending --reason "receipt for <commit12> ready"
lean-pkg gate telescoping-companion --receipt .lean-receipts/<commit12>-<job>.json
lean-pkg claims ledger telescoping-companion

The receipt binds the package directory at one commit. The gate refuses, for example, a receipt whose verify log declares fewer sorry warnings or axioms than Lean itself printed, or a commit where the package has changed since.

5. Keep developing; reuse what did not change

The paper keeps changing. Each later checkpoint asks one question per claim: did its formal statement, its proof, or the way the paper uses it change?

A refusal is information. If gate refuses, read which binding it names before changing anything.

6. Keep a coverage map

Record how each numbered result of the paper relates to the companion in coverage.yaml (schema coverage/1) in the package directory: one row per paper result, with its correspondence class (same-assumptions, inputs-supplied with the named inputs, or outside) and the claim ids that formalize it. Do not keep a hand-written coverage table: lean-pkg coverage check NAME validates the file, and lean-pkg page NAME --write renders the map, the “Not formalized” list and the status into the companion’s README from it, the claims ledger and the receipts. A row is called verified only when the ledger closes its claims. See The verification page for the schema and an example.

Update the file at every checkpoint, and run lean-pkg page NAME --check: the map is what tells a reader where the certificate stops.

Anchoring to an arXiv version

A companion is released against one posted version of the paper, and a reader should be able to check that the TeX the claims were written against is that version’s source. lean-pkg formalization anchor does the comparison and records it:

# offline: the e-print you downloaded from https://arxiv.org/e-print/<id>v<N>
lean-pkg formalization anchor NAME --arxiv <id>v<N> --from-file <id>v<N>.tar.gz --compare-tex paper.tex
# or let lean-pkg download it (the only network access; HTTPS, 60 s timeout, 64 MiB cap)
lean-pkg formalization anchor NAME --arxiv <id>v<N> --fetch --compare-tex paper.tex

The version is required: an unversioned id is whatever arXiv serves today. The e-print is read in memory, never unpacked to disk. A gzip’d tar, a gzip’d single .tex and a plain tar are read; a PDF-only submission is refused (it has no source to anchor to; pin manuscript.version by hand). An archive with an absolute path, a .. component, a link or a device member, or more members or bytes than the caps allow, is refused whole.

The command prints the e-print’s SHA-256, its main .tex (the file with \documentclass; --main-tex PATH when several have one), how it relates to the manuscript coverage.yaml is bound to, and, with --compare-tex, whether your .tex is identical after normalising line endings, trailing whitespace and trailing blank lines, or the differing lines. Without --write nothing is written.

--write writes three files and commits none of them:

It refuses an anchor nothing ties to the ledger: --write needs coverage.yaml already bound to that version, a bound {repo, commit, sha256} whose SHA-256 is one of the e-print’s files, or --compare-tex showing the files identical. When they differ (a changed \bibliographystyle line, say), read the differences and pass --accept-diff "REASON"; the reason goes into the record. A second record for the same version with other e-print bytes is refused: posted versions do not change. The registry is never written; when its source_paper.arxiv differs, the command prints the lean-pkg update NAME --source-paper-arxiv <id>v<N> to run.

Moving to a later version (v2 after v1) is a re-anchor: the old record stays, the files are re-pointed, and the command prints the claims-ledger step, lean-pkg claims rebase NAME --from-tex OLD.tex --to-tex NEW.tex, so theorem numbers and labels follow the new text.

Moving to a new manuscript version

Claims written against a private draft carry its numbering. When the posted version differs, do not re-key the rows by hand:

lean-pkg claims rebase my-paper-lean --from-tex draft.tex --to-tex posted.tex \
  --to-aux posted.aux --from-aux draft.aux --to-version arXiv:IDvN --out-dir rebase-posted

Statements whose text is unchanged (up to comments, colour, whitespace and the other listed normalizations) are carried with their numbers, pages and lines re-keyed from the new .aux; reworded, deleted and moved statements are listed in rebase-posted/rebase-report.md with both excerpts, and their rows are left as they were. No status changes, and no finding is marked fixed: read each listed row against the new text, edit the proposals, then commit them. The old TeX must be the file coverage.yaml is bound to (its SHA-256), so the comparison is against what the claims were written for. See Move to a new manuscript version.

7. Finish

At submission the deliverable is:

Publishing the companion follows the usual path: scan for private strings, the comparator tier, and promote.

When the comparison covers more than the paper’s main results, add a headline configuration (comparator.headline.json, Palomar’s six keys only) listing just the main results: formalization.yaml then advertises those in status.main_results and palomar prepare names it for the Palomar entry, while the receipt and the gate keep binding the full comparison. Every headline name must be covered by the gate-bound comparator receipt (same Challenge and Solution modules), or the render is refused.

Credits

lean-pkg page NAME --write writes both credits below into the README’s Acknowledgments (the Easley sentence only with a backing Slurm receipt), and --check fails when the lean-pkg credit is missing or an Easley sentence has no backing (The verification page). By hand: give the companion’s README an ## Acknowledgments (or ## Tools) section that names the tool used to develop and verify it, with the repository link and the concept DOI (which always resolves to the latest release):

Developed and verified with [lean-pkg](https://github.com/lean-pkg/lean-pkg) ([doi:10.5281/zenodo.23272098](https://doi.org/10.5281/zenodo.23272098)).

To name the exact version, add it with its version DOI, taken from lean-pkg’s CITATION.cff (identifiers) or the README’s Citation section for the version that produced the receipts (lean-pkg --version). The compute acknowledgment below goes in the same section.

Acknowledge the compute

When the receipts show the gates ran on the Auburn University Easley Cluster (a receipt slurm receipt in .lean-receipts/ whose job ran on that cluster), put the official sentence, with the cluster name linked, in the companion’s README:

This work was completed in part with resources provided by the [Auburn University Easley Cluster](https://hpc.auburn.edu/hpc/docs/hpcdocs/build/html/easley/intro.html).

Keep the wording verbatim (“in part” unless Easley was the only compute used). A companion whose receipts came from other hosts carries no such sentence: the acknowledgment is a statement about where the evidence was produced. Other clusters have their own required wording: describe yours in a site profile and lean-pkg page renders and checks it the same way.

Consolidate several checkpoint packages into one

A long project can leave several verified-private packages behind, one per round or checkpoint, each with its own gate. Publishing one companion then means consolidating them into a new package. There is no single command for this: repo export moves one existing record to one new repository, while consolidation creates a new record from several inputs. The recipe below uses only existing commands. It assumes the inputs share one Lean toolchain and one Mathlib revision; align the pins first if they do not, since that is a change to every input.

When the Lean code lives inside the paper’s own repository rather than in registered packages, lean-pkg-extract plan plans the public tree instead: every file classified (private material default-denied), traced to a blob of one source commit, with its module and claim maps (P1: plan only; write comes next).

The rules. The old packages, their repositories and their histories stay as they are. The new package gets a new name, because an old name already denotes its own round. Its evidence is new: no old receipt is copied or reused, because a receipt binds one commit of one repository and the consolidated commit descends from none of them. Old receipts and commits appear in the new repository only as provenance.

Assemble the tree without renaming anything

Build the new tree in a new repository and commit the result as one consolidation commit that relocates code and changes nothing else:

Renames, merged helpers and cleanups come later as separate commits, each reviewed and gated on its own. A reviewer can then check the consolidation commit mechanically against the hash map, and the later commits as ordinary diffs.

Record the source and claim hash map

Commit a hash map in the new package directory, in the consolidation commit itself, so that the first receipt binds it. lean-pkg does not read this file; it is your record, and a reviewer re-checks it. One possible shape, provenance/consolidation.yaml:

inputs:
  - package: example-round-1            # the old registry name
    repo_commit: 0123456789abcdef0123456789abcdef01234567
    gate_receipt: .lean-receipts/0123456789ab-job123.json   # path in the OLD repository; provenance only
    comparator_receipt: .lean-receipts/0123456789ab-comparator.json
files:
  - from: {package: example-round-1, path: Example/Round1/Basic.lean,
           sha256: 9f2c...}
    to: {path: Example/Round1/Basic.lean, sha256: 9f2c...}
    change: none                        # or: imports-only
claims:
  - from: example-round-1/main-bound
    to: example-companion/main-bound

Take each from hash from the old commit, not from a working copy (git -C OLD show COMMIT:PATH | sha256sum), and each to hash from the committed new tree (git show HEAD:PATH | sha256sum). Every relocated file and every old claim gets a row; a claim dropped on purpose gets a row that says so. For an imports-only row, the diff between the two blobs with the import lines removed must be empty. If the new package is meant to become public, check that the old names and paths the map cites may be public: lean-pkg public-safety NAME --strict scans the map like any other file.

Carry the license of adopted files

Files adopted from another project (vendored, then ported) keep their upstream license. A port can pass the hash map and the import check while leaving that license behind. Copy the upstream license byte for byte from the commit you took the files from into a scoped file, for example LICENSES/LicenseRef-Upstream-MIT.txt, and list the files it covers (a REUSE.toml annotation or a provenance list); do not copy it to the root as a license for the whole package. lean-pkg-extract plan warns when this is missing; see Licenses of adopted files.

Audit the collisions before the first gate

Several inputs that each passed their own gate can still clash once they share one environment. Check before the first verify run:

Register, gate and run the comparator on the new commit

lean-pkg register example-companion --like example-round-1 \
  --repo git@github.com:you/example-companion.git --path src/example-companion
lean-pkg lease claim example-companion --workspace laptop --agent you
lean-pkg claims sync example-companion

register --like copies the sibling’s repository URL, owner project, upstream target and automation note, and reports whether the toolchain and Mathlib pins match; --repo names the new repository instead of the copied one. The new package shares root namespaces with the old ones, so audit reports duplicate-namespace; record why with lean-pkg update NAME --namespace-note TEXT (the finding becomes info once every package sharing the namespace carries a note).

Then produce a fresh lower-tier receipt and a fresh comparator receipt at the consolidation commit (or a later commit), exactly as for any package: step 4 above and Produce the comparator receipt. The old packages need no change. If you want their records to point forward, lean-pkg update NAME --append-note TEXT --agent A adds a note event to an old record without touching its repository or its evidence.

Two environment pitfalls

What this does not claim