lean-pkg/lean-pkg

lean-pkg

Prove it. Then prove you proved it. A registry and trust gate for Lean 4 formalization packages: know which packages exist, who holds each one, and what evidence binds it to a verified commit, before anything becomes public.

---

Why lean-pkg

A green build is a claim. A receipt is evidence.

A Lean project that builds with zero sorry is not yet a verified theorem. The statement may have drifted from the paper’s claim, the check ran in the same kernel that elaborated the proof, and “CI was green” is a status word nobody can re-derive. lean-pkg requires two receipts before a package can go public: a build-and-axioms receipt bound to one commit, and a comparator receipt in which trusted statements are checked against untrusted proofs and replayed in an independent kernel. At promotion time it re-derives both from bytes.

Research loop: discover, formalize, verify

Research mathematics is rarely linear. A symbolic computation may suggest a formula; Lean may expose a missing hypothesis; the manuscript changes; the formalization changes with it. lean-pkg is designed to keep the verification state attached to exact commits while that loop remains private.

The trust boundary is deliberately asymmetric:

• Python, SymPy, Sage, Mathematica, numerical experiments, or hand calculations may discover a candidate claim;
• Lean states and proves the mathematical claim;
• lean-pkg records which exact source and evidence were actually verified.

A computational discovery is therefore provenance, not proof. If the final Lean theorem no longer depends on trusting the computation that suggested it, the certificate rests on the Lean proof, not on the exploratory tool.

As formal libraries mature, a result that was initially conditional can be re-certified with fewer external dependencies. The roadmap treats that progression as certificate lineage rather than overwriting history.

Develop privately. Discover freely. Verify explicitly. Publish reproducibly.

Develop papers with a Lean companion

The companion does not have to start after the manuscript is finished. Check selected intermediate results while the argument evolves, keep each checkpoint bound to an exact commit, reuse unchanged results, and keep a map of which statements in the paper are formal, conditional or not formalized. A certificate covers its exact formal statements, not the surrounding paper. Walkthrough: Develop a paper with its Lean companion.

Who is this for

• A research group formalizing its own papers: run the private lifecycle (register, claim, gate, promote), mostly through agents, with a human reading each dry run.
• A mathematician asking “is this already verified in Lean?”: read the field index, with hypotheses and paper correspondence, keyed to Palomar ids.
• An LLM agent proving something: fetch llms.txt and the index first; import instead of re-deriving.
• A contributor: send code to the tool, or an index entry for a result you verified.

Not Palomar, not Mathlib

Public verified results are registered in Palomar, which archives them and assigns stable ids. Every package depends on Mathlib. Public packages are indexed by Reservoir, automatically (no registration step), which checks that they build but not what they prove; search it before building anything new. lean-pkg covers what those leave out: the months before a result is public, and a field-curated index after. A package that passes its comparator tier is already in the shape Palomar accepts. The full comparison is in Motivation and the FAQ.

In sixty seconds

Install the CLI once, then use one shared private registry to coordinate many independent Lean/Git research repositories.

~/.lean-pkg/registry/          # recommended shared coordination repo
  .git/
  lean-packages.yaml
  lean-package-events.jsonl

~/src/
  paper-a/                     # its own Git repo and Lean project
  paper-b/                     # another independent Git repo
  paper-c/

Today, bootstrap the shared registry explicitly:

pipx install git+https://github.com/lean-pkg/lean-pkg.git

mkdir -p ~/.lean-pkg/registry
git -C ~/.lean-pkg/registry init
lean-pkg --registry ~/.lean-pkg/registry/lean-packages.yaml init
git -C ~/.lean-pkg/registry add lean-packages.yaml lean-package-events.jsonl
git -C ~/.lean-pkg/registry commit -m "registry: initialize lean-pkg"

# ~/.lean-pkg/registry is the default registry location: no LEAN_PKG_REGISTRY needed

# placeholders: replace you/my-proof with your repository and src/my-proof with
# the path of your checkout under $HOME (here ~/src/my-proof)
lean-pkg register my-proof --repo [email protected]:you/my-proof.git --path src/my-proof
lean-pkg claim my-proof --workspace laptop --agent you --reason "first receipt"
lean-pkg renew my-proof --agent you            # past 24 h: renew before the lease lapses (`lean-pkg leases`)
cd ~/src/my-proof && lake exe cache get    # your checkout: the --path above, under $HOME
# on your own machine, allow this host; without it the run refuses by design
COMPARATOR_RECEIPT_ALLOWED_HOSTS="$(hostname)" comparator-receipt
lean-pkg comparator my-proof --check --receipt .lean-receipts/-comparator.json
lean-pkg promote my-proof                      # dry run: the checklist says what is missing

No Lean project yet? Getting started, step 1 makes a minimal Challenge/Solution project with a complete comparator.json, ready for comparator-receipt.

my-proof is the package name given to register: every later command that takes NAME (claim, comparator, next, promote, …) takes that name, never a path. --path is relative to $HOME; if the checkout is somewhere else, lean-pkg update my-proof --path DIR --reason "checkout moved" records the real one.

The registry repository is the cross-project coordination history; each research repository keeps its own mathematics and committed .lean-receipts/ evidence. Keep the shared registry private unless you intentionally want to expose pre-publication project names, paths, notes, and status history.

A future one-command bootstrap such as lean-pkg init --global is proposed in the roadmap; it is not implemented yet.

What it does

register → claim → gate → comparator → publish → index

Not sure what comes next for a package? lean-pkg next NAME prints the single recommended command and why; agents get the same answer with --json.

Checking a learner’s exercise, not a package? lean-exercise check --challenge Challenge.lean --solution Solution.lean judges each sorry’d theorem with lake comparator in its sandbox; no registry involved (Checking Lean exercises). On a machine without the sandbox, --no-sandbox checks your own work only: the result is labelled self-check-only, never a grade.

Receipts from a cluster or a capped local unit: lean-pkg receipt slurm and receipt systemd turn a finished job into a lower-tier receipt, and --compress-log seals a very large log as deterministic gzip. The Slurm template (receipt slurm --template) builds the package with an empty, job-local Lake cache; SRC_MODE=clone gives the job a real .git at the commit, and DEPS_TAR restores prebuilt dependencies while the package itself still builds fresh; receipt slurm --preflight-deps checks before submission that the tarball holds every module the audit files import (Receipts and trust).

Writing the comparator configuration: lean-pkg comparator config --from-claims NAME --claims-file claims.yaml scaffolds entries from a working-copy claims file, and --challenge-from-type pre-fills statements with typed numerals, such as (3 / 2 : ℝ), so they elaborate back to the original. comparator-receipt checks early that every configured module is a Lake target and that no dependency is a symlink its sandbox cannot see, and lean-pkg comparator NAME --check --receipt R --repo DIR pre-checks a receipt made in a worktree (The comparator tier).

Something went wrong? lean-pkg report --command "..." drafts a bug report in this repository’s issue format with every private path and address redacted; --yes files it.

Safety nets, before anything is public:

• lean-pkg public-safety NAME scans the tree and the whole git history (blobs, commit messages, author and committer identities, tags, branch names) for private strings, the whole repository when the package is a subdirectory of it; promote refuses while blocking hits remain, and promote --yes fetches origin’s branches, tags and pull-request heads first. Before freezing a public candidate made from private history, add the project’s own terms (citation keys, working titles) to .lean-pkg-private-patterns; the built-in patterns cannot know them (Before freezing a public candidate).
• lean-pkg release NAME --fresh-repo DIR (or --adopt-repo DIR) gives a package incubated beside a paper a fresh public history; see Publishing a package incubated beside private work. Several checkpoint packages that become one public companion follow the consolidation recipe.
• lean-pkg comparator host-check says whether this machine can produce comparator receipts at all, before a long run.
• lean-pkg audit reports expired leases, receipt drift and GitHub visibility mismatches.

Two files live in each package repository. claims.yaml (schema claims/1) names the results someone might reuse; lean-pkg claims sync, claims list and claims check cache and validate them, and lean-pkg search searches them with the index and public sources (Prior-art search): --loogle-query sends Loogle a pattern of its own, --require-complete exits 1 when the search is incomplete (a source skipped, failed or capped), and --cache-dir keeps one search’s cache apart (Requiring a complete search). formalization.yaml is the mathlib-initiative self-report Palomar reads; lean-pkg formalization NAME renders it from the registry and the receipts (formalization.yaml). For a public companion, lean-pkg page NAME --write renders the README’s verification section (status, paper-to-Lean map, Not formalized, trust boundary, reproduce, evidence, citation, license, credits) from coverage.yaml, the claims ledger and the committed receipts, and lean-pkg page NAME --check fails when it is stale; lean-pkg coverage check NAME validates coverage.yaml (The verification page).

After the flip:

• Reservoir: lean-pkg reservoir check NAME checks the listing criteria before you wait for Reservoir to list the package.
• Palomar: lean-pkg palomar check NAME lists every gap to Palomar’s mechanical rules (a module header in every .lean file, the toolchain floor, the comparator configuration keys, formalization.yaml, the licence), read-only; run it before the gated waves, since fixing a gap changes build inputs and forces a re-gate. lean-pkg palomar prepare NAME then builds the submission bundle locally; nothing is sent.
• Zenodo: archive each GitHub release for a DOI and record it with lean-pkg record NAME doi-minted; lean-pkg itself is archived under 10.5281/zenodo.23272098.

Learn the workflow

From the terminal, lean-pkg help lists the commands and the help topics: lean-pkg help exit-codes, help environment and help formatting cover exit codes, environment variables and --json output (How to).

Documentation site: .

For collaborators

Joining someone else’s package? Accept the GitHub invitations, log in with gh auth login, clone this repository, and run bash scripts/bootstrap-collaborator.sh OWNER/PACKAGE: it checks the machine and your access, installs lean-pkg, clones the package and sets up your own committed registry. Then follow Add the comparator tier to an existing package step by step. Trying the tool cold, from the documentation alone? Record what happened with the stranger test template.

Requirements

Python 3.11+ and PyYAML. git for anything that reads a repository; gh, authenticated, for promote and audit. comparator-receipt needs Linux, elan, go, cargo, jq and bwrap (bubblewrap, the toolchain mechanism’s sandbox); lean-pkg comparator host-check says whether this machine can produce comparator receipts, and with which mechanism. With the toolchain mechanism (Lean v4.35.0-rc2 or later, what Palomar runs) a first run takes seconds once the Mathlib cache is in place. The legacy mechanism’s first run builds the comparator tools once (about 25 minutes); later runs take seconds. lean-exercise check needs Linux, bwrap able to create an unprivileged user namespace, and Lean v4.35.0-rc2 or later (Host).

AI assistance

Built with AI assistance: the implementation, tests, and documentation were written with Anthropic’s Claude, directed and reviewed by the maintainer, who is responsible for every merged change. The secretary-bird logo and the mascot illustration were generated with AI image tools by the maintainer. Contributions must disclose AI assistance; see CONTRIBUTING.md.

Citation

Releases are archived on Zenodo: the concept DOI 10.5281/zenodo.23272098 resolves to the latest release, and CITATION.cff lists it with the version DOIs. To cite a state between releases, cite the repository at a commit:

@software{lean_pkg,
  author  = {Chen, Le},
  title   = {lean-pkg: a registry and trust gate for Lean 4 formalization packages},
  year    = {2026},
  version = {0.7.54},
  url     = {https://github.com/lean-pkg/lean-pkg},
  note    = {commit }
}

Releases are listed in CHANGELOG.md; the process is in RELEASING.md. Proposed future directions are in ROADMAP.md. Design choices are recorded in docs/decisions; security reports go by SECURITY.md.

Acknowledgments

This work was completed in part with resources provided by the Auburn University Easley Cluster. The lower-tier receipts (lake build, sorry scan and axiom audit) and comparator receipts (statement comparison and kernel replay) that exercised lean-pkg during development were produced by Slurm jobs on Easley, alongside runs on lab workstations.

License

Copyright © 2026 Le Chen and Auburn University. Licensed under Apache-2.0; see LICENSE and NOTICE. Contributions are accepted under the same license; see CONTRIBUTING.md.