New here? The Quickstart goes from pip install to a
verified page on your own machine, with no lab account, in five verbs:
lean-pkg new my-proof --kind library, lean-pkg verify my-proof (both receipts and the gate),
status, page --write, publish.
The π-λ tutorial does the same with a real
theorem, Dynkin's π-λ theorem, for a mathematician who has barely used Lean.
Nothing to install: the badge opens the π-λ tutorial in your browser, with
Lean, lean-pkg and Mathlib's prebuilt files ready, through to a verified page
(Try it in your browser:
the time to ready, the cost on your own GitHub account, and what needs a real
machine).
One workflow, two products: a verified paper (Track P) or a reusable Lean
library (Track L). Each step is explained in the
sample workflow; the tracks in
Two tracks.
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
Mathematics, Lean and an AI assistant: one workflow, and a record of who
checked what.
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;
- an AI assistant may draft Lean statements and proofs: Lean checks a
drafted proof like any other, but a drafted statement is only as good as
the mathematician's reading of it (a definition-hole sign-off refuses a
model or agent as the reviewer);
- 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 registry 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 --url [email protected]:you/my-proof.git --path src/my-proof
lean-pkg lease claim my-proof --workspace laptop --agent you --reason "first receipt"
lean-pkg lease renew my-proof --agent you # past 24 h: renew before the lease lapses (`lean-pkg lease list`)
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 check my-proof --receipt .lean-receipts/<c12>-comparator.json
lean-pkg publish my-proof --yes --dry-run # 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 lean-pkg receipt comparator.
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 registry init --global is proposed in
the roadmap; it is not implemented yet.
What it does
register → claim → gate → comparator → publish → index
| Step | Commands | What it gives you |
|---|
| register | lean-pkg register, update | one record per package; register is the only way in |
| claim | lean-pkg lease claim, lease renew, lease release, lease list | a lease (24 h by default; --contact names the session behind it), so two people or agents never work on one package unknowingly |
| gate | lean-pkg gate | the lower-tier receipt (build, no sorry, axioms) moves the package to verified-private |
| comparator | lean-pkg receipt comparator, lean-pkg comparator | the comparator receipt: trusted statements against untrusted proofs, replayed in a second kernel |
| publish | lean-pkg publish --dry-run, promote | one read-only checklist to listed, then the one-way flip to public |
| index | lean-pkg index add, index check --clone | a field index entry whose trust (lower-tier, comparator, palomar) is computed from the evidence, never typed |
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).
No cluster: lean-pkg receipt ci --template prints a workflow that runs
lean-pkg's reusable verify.yml on a GitHub-hosted runner, and
lean-pkg receipt ci --collect RUN fetches and checks the receipt it wrote
(Writing the receipt in CI).
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. lean-pkg receipt comparator
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 check NAME --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
publish --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 repo export NAME 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 registry 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 render 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, mathematics
first (what to compare, then each result with the paper's statement beside
the Lean statement, Not formalized, what the checks establish, how this was
checked, 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 port-modules NAME plans the
module-system port as a diff (--write applies it, never commits). 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: https://lean-pkg.github.io/lean-pkg/.
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. lean-pkg receipt comparator 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.23.0},
url = {https://github.com/lean-pkg/lean-pkg},
note = {commit <sha>}
}
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; format and command changes start
as design proposals. How the project is run, and
the AI operations agent's role, is in GOVERNANCE.md;
security and soundness reports (a way to get a false "verified") go
privately 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 (c) 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.
