agentsclimarketplace
Sign in

Lean proof review

Skill r-irbe/proof-skills/skills/lean-proof-review

USE FOR: reviewing one Lean 4 proof / file for correctness, soundness, statement faithfulness, non-triviality, and proof quality; running the 4-layer verification checklist (formal soundness → statement → non-triviality → quality); flagging common Lean pitfalls; recommending tactic alternatives from the Mathlib + Aesop + Duper + Canonical stack. DO NOT USE FOR: writing a new proof (use @lean-proof); multi-agent council deliberation (use @lean-review-council); running CI scripts (use @lean-enforcement); scoring the whole project (use @lean-quality-engine). TRIGGERS: proof review, audit proof, verify Lean, 4-layer checklist, lean-pitfalls, proof quality.From its SKILL.md

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

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.

SKILL.md

5.6 KB, ~1.2k tokens by cl100k_base, as published. Nobody here has run it

lean-proof-review

⚠️ MANDATORY (hot-tier): layers L1 (soundness) and L2 (statement) are hard gates — a failure at either MUST block sign-off, regardless of L3/L4. Skipping Persist = incomplete.

Routing

  • USE FOR: auditing a single Lean 4 proof or file across the 4-layer checklist (L1 soundness, L2 statement, L3 non-triviality, L4 quality); cross-checking that imported tactics from the project automation stack are used correctly; spotting common pitfalls (vacuous truth, unused hypothesis, broken simp set, scope drift).
  • DO NOT USE FOR: authoring the proof (delegate to @lean-proof); convening a multi-agent review (delegate to @lean-review-council); running the CI scripts (delegate to @lean-enforcement).
  • TRIGGERS: proof review, audit proof, verify Lean, 4-layer checklist, lean-pitfalls, proof quality.

Behavioural rules (G-*)

  • G-1 (MUST): The reviewer MUST run the four layers in order (L1 → L2 → L3 → L4); a failure at L1 or L2 MUST halt the review. [Trace: AC-01]
  • G-2 (MUST): The reviewer MUST verify the theorem statement matches the source spec / paper / requirement before judging the proof. [Trace: AC-02]
  • G-3 (MUST NOT): The reviewer MUST NOT silently rewrite the proof; suggested rewrites MUST be flagged as suggestions for the author. [Trace: AC-03]
  • G-4 (SHOULD): The reviewer SHOULD recommend the higher-quality tactic when a lower-priority one was used unnecessarily (see REFERENCE.md "Proof Search Priority"). [Trace: AC-04]
  • G-5 (MUST): A non-trivial theorem with a one-tactic decide / aesop / grind close MUST be flagged for L3 (non-triviality) review. [Trace: AC-05]
  • G-6 (SHOULD NOT): The reviewer SHOULD NOT mark a proof "approved" without confirming lake build is green on the containing file. [Trace: AC-06]
  • G-7 (MUST): Every flagged finding MUST cite the layer, the line(s), and the rule from REFERENCE.md or GUARDRAILS.md. [Trace: AC-07]
  • G-8 (MUST): On any guard failure the skill MUST escalate per §Recovery & STOP. [Trace: AC-08]

Workflow

  1. Discover [discover] — read the target file, locate the theorem(s), find the source spec and any prior review record.
  2. L1 soundness [validate] — confirm no sorry, no admit, no sorryAx; defer to @lean-enforcement for axiom audit if needed.
  3. L2 statement [validate] — diff the theorem statement against the spec / paper; halt if it has drifted.
  4. L3 non-triviality [validate] — confirm the hypothesis is non-vacuous; spot pattern-match for hidden trivialities.
  5. L4 quality [validate] — apply the proof-search priority table; flag tactic mis-selection, unused hypothesis, fragile rewrite chains; suggest improvements but do NOT apply them.
  6. Persist [persist] (MANDATORY) — write the review record (per-layer status, findings, suggestions) to the repository's review log, link it from the theorem, update sign-off state. Skipping Persist = incomplete.

Recovery & STOP

  • L1 fails (sorry / admit / sorryAx) → STOP, do NOT proceed to L2-L4; escalate to author.
  • L2 fails (statement drift) → STOP, escalate to spec owner before any proof judgement.
  • lake build red on containing file → STOP, ask author to fix build first.
  • Confidence < 90 % on a tactic suggestion → mark as advisory, do NOT block.
  • Scope drift (edits to non-proof files) → immediate STOP, re-anchor.

Handoffs

  • Predecessors / successors: see FM handoffs (grammar from ADR-0080).
  • Source spec: specs/lean/proof-review/requirements.md — every G-rule traces to an AC there.
  • Related ADRs: ADR-0076, ADR-0080.
  • Reference: see REFERENCE.md for the full project automation stack, proof-search priority table, reusable Tactics lemma library, common Lean pitfalls, and the 4-layer verification checklist (original v1 content, preserved verbatim).
  • Mathlib-specific review: see ../../references/upstream/mathlib4-review.md for the Mathlib PR review delta (attributes/API, simp squeezing, normal forms, transparency, file size, canonical naming/style URLs). The former mathlib-review SKILL has been demoted to a REDIRECT stub pointing at this reference (W4 Wave 1 / move A2).

Common failure modes

AI agents commonly: rewrite the proof inline instead of suggesting changes; approve at L4 without confirming L1/L2 passed; miss vacuous-truth L3 failures behind a clean aesop close; cite a pitfall without quoting line numbers or the source rule. Full registry: GUARDRAILS.md §Agent failure taxonomy.

What ships with it: 2 files

26.3 KB alongside SKILL.md

tests/

Keep looking

Skills are one crate of 325,949. 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.