lean-pkg/lean-pkg
Developer tools이 페이지는 AI로 자동 번역되었습니다. 기술적인 세부 사항은 원문을 확인하세요. 원문 보기
lean-pkg: lifecycle registry and trust gate for Lean 4 verification packages (comparator/nanoda acceptance bar)
개요
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. 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 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 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.
README
원문 README의 일부입니다. 원문 보기.
lean-pkg
Lean checks the proofs. You check the statements. lean-pkg checks the receipts. 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.
New here? The Quickstart goes from pip install to a
verified page on your own machine, with no shared registry or cluster 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).
추천 도구
다른 키워드를 입력하거나 필터를 제거해 보세요.
설치
npx skillfish add lean-pkg/lean-pkg