lean-pkg/lean-pkg

Эта страница переведена автоматически. Технические детали смотрите в оригинале. Открыть оригинал

4 stars Качество 68 Тренд 25Apache-2.0

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).