agentsclimarketplace

Lean package research

Skill r-irbe/proof-skills/skills/lean-package-research

APM-installable agent skills for Lean 4 and Mathlib4 — proof tactics, math domains, review and research workflows, generic tooling.

Install
npx -y skills add r-irbe/proof-skills --skill lean-package-research

Assembled from the repository path, not quoted from the project. Check it against their README if it does not work.

One thing to look at

  • 2 stars2 stars. Stars are a popularity signal and not a quality one, but at this level it is likely that nobody has read this closely except its author, and you would be relying on your own review.

What its author says it does

Copied from the file, not written here

USE FOR: Lean 4 package and toolchain research — evaluating Reservoir/GitHub packages, Mathlib/cslib pin changes, Lake dependency health, package adoption classes, update sequencing, and external theorem-substrate candidates. Use this whenever the user asks whether to add, update, fork, pin, vendor, or reject a Lean package, even if they phrase it as "can we use this repo?" or "does mathlib have this now?". DO NOT USE FOR: ordinary theorem lookup without a package decision (use @lean-research); package-file mutation or `lake update` execution (use @lean-enforcement plus a project-specific edit claim); proof writing (use @lean-proof); general project QA (use @lean-quality-engine). TRIGGERS: Lean package, Reservoir, GitHub Lean repo, Lake dependency, lake-manifest, lean-toolchain, mathlib update, cslib update, package adoption, package pin, dependency health, external theorem substrate.

SKILL.md

5.3 KB, as published. Nobody here has run it

lean-package-research

Package research is separate from theorem lookup because dependency decisions change reproducibility, build time, trust surface, and future maintenance. This skill turns a candidate package or pin change into an adoption recommendation with evidence, sequencing, and validation.

Routing

  • USE FOR: Lean 4 package and toolchain research — evaluating Reservoir/GitHub packages, Mathlib/cslib pin changes, Lake dependency health, package adoption classes, update sequencing, and external theorem-substrate candidates.
  • DO NOT USE FOR: ordinary theorem lookup without a package decision (use @lean-research); package-file mutation or lake update execution (delegate validation to @lean-enforcement under an edit claim); proof writing (use @lean-proof); general project QA (use @lean-quality-engine).
  • TRIGGERS: Lean package, Reservoir, GitHub Lean repo, Lake dependency, lake-manifest, lean-toolchain, mathlib update, cslib update, package adoption, package pin, dependency health, external theorem substrate.

Workflow

  1. Scope the package question [discover] — identify whether the caller wants theorem borrowing, dependency adoption, pin update, fork/vendor choice, or negative-result evidence. If the request only needs symbol lookup, hand off to @lean-research.
  2. Run the discovery ladder [discover] — use ../../references/discovery-ladder.md for Reservoir, GitHub, current-pin package source, theorem-search services, and literature checks. Record negative results rather than relying on memory.
  3. Assess dependency health [validate] — inspect Lake metadata, toolchain compatibility, maintenance status, archive/staleness, license visibility, transitive dependencies, binary fetches, and whether the package is already represented by Mathlib/cslib.
  4. Classify adoption [validate] — use ADOPT-NOW, ADOPT-LATER, RESEARCH-MORE, DO-NOT-ADOPT-NOW, or DO-NOT-ADOPT. Package adoption and theorem borrowing may receive different classes.
  5. Plan sequencing [execute] — list exact files that would change, commands that must run, rollback/preflight steps, and which validation owner should run them. Do not mutate package files from this skill.
  6. Persist handoff [persist] — return a compact package card with evidence, confidence, adoption class, validation commands, blockers, and HITL questions.

Package card format

## Package research card: <package or pin>

- Question:
- Candidate:
- Current project pins/toolchain:
- Sources checked:
- Theorem/substrate value:
- Dependency health:
- Adoption class:
- Confidence:
- Required validation:
- Write targets if later authorized:
- Rollback:
- HITL needed:

Recovery & STOP

  • STOP if the package would require editing lean-toolchain, lakefile.lean, or lake-manifest.json without an explicit edit claim and human authorization.
  • STOP if the adoption class is ADOPT-NOW but confidence is below the local belief floor, validation is unknown, or the dependency graph is dirty.
  • STOP if a package is archived, stale, or has unclear transitive dependencies and the caller asks for immediate adoption; return RESEARCH-MORE or DO-NOT-ADOPT-NOW with evidence.
  • STOP if a theorem-search hit cannot be re-verified at source; downgrade symbol borrow confidence and hand off to @lean-research.

Handoffs

  • Predecessors: @lean-research for symbol/literature leads, @lean-integration-protocol for project integration boundaries, agent:gateway for package-focused user requests.
  • Successors: @lean-research for deeper theorem lookup, @lean-enforcement for validation commands, @lean-quality-engine for milestone/package-health scoring.
  • References: discovery ladder (../../references/discovery-ladder.md) and eval prompts (../../references/discovery-ladder-evals.md).

Keep looking

Skills are one crate of 328,083. Ordering is by how many stacks a row turns up in, so the top of any crate is what has actually been picked rather than what has the most stars.