agentleFS
Sign inStart free
r-irber-irbe/proof-skills/skills/lean-review-council/SKILL.md

lean-review-council

Skill3 starsChanged 26 days agoApache-2.0View on GitHub

USE FOR: orchestrating a 5-member Lean 4 proof review council (Σ Kernel Guardian, Φ Statement Oracle, Ν Novelty Scout. DO NOT USE FOR: reviewing one Lean proof in isolation (@lean-proof-review). TRIGGERS: review council, RALPH loop, council vote, SDR, council topology.

The file

We split this skill into the rules it gives an agent

4 rules. About 0 are common, 3 are distinctive, and 1 is very specific to this project.

  • ≈0

    Common · estimate

    Many files like this have a rule of this kind.

  • ≈3

    Distinctive · estimate

    This author's own choices. Worth a look.

  • 1

    Very specific

    Tied to their project's names, files or tools. Probably skip.

  • Common
  • Distinctive
  • Very specific
  1. Distinctive:

    Run Part 12 — Execution Protocol (kept inline below) end-to-end.

    line 49
  2. Distinctive:

    STOP if more than two members report 🔴 votes on a single artifact — enter SDR (handbook Part 3) before any further dispatch.

    line 56
  3. Very specific:

    STOP if RALPH loop iteration count exceeds 3 without convergence — escalate to the Meta-Council (handbook Part 10) or handoff to …

    line 58
  4. Distinctive:

    STOP if the Documenter or Synthesizer fails to produce a session report — the council session is incomplete.

    line 62

≈ “Common” is an estimate: at least 1 in 5 of the 350,495 skill files we read have a rule of the same kind, not the same words. “Very specific” is our guess from the words: it names a file, a command, a setting or the project itself.

Keep what fits and drop the rest. Your version, ready for your agents.
Files
SKILL.md

Lean 4 Review Council

A formal review council of five voting AI agents that collectively execute the lean-proof-review skill with 99.99% reliability and resilience. Each

Routing

  • USE FOR: orchestrating a 5-member Lean 4 proof review council with RALPH loops at member / council / project / meta scales; structured voting with SDR; council topology selection; maximum-parallel agent dispatch with cascading completion handlers; specification lifecycle, inter-council collaboration, Zettelkasten synthesis, calibration scoring, enforcement tactics.
  • DO NOT USE FOR: reviewing one Lean proof in isolation (delegate to @lean-proof-review); writing a proof (delegate to @lean-proof); running CI

Workflow

  1. Identify the scope (theorem / file / module / project / meta-council cross-module).
  2. Pick a topology (Part 4 of the handbook — Star for first pass, Pipeline for sequential dependencies, Hierarchical for project scale, Hub-Spoke for inter-council).
  3. Run Part 12 — Execution Protocol (kept inline below) end-to-end.
  4. On a blocking finding, enter SDR (handbook Part 3); on approval, dispatch Documenter + Synthesizer for the session report and Zettelkasten update.
  5. Aggregate session reports at the module / project level; convene the Meta-Council for cross-module coherence when needed.

Recovery & STOP

  • STOP if more than two members report 🔴 votes on a single artifact — enter SDR (handbook Part 3) before any further dispatch.
  • STOP if RALPH loop iteration count exceeds 3 without convergence — escalate to the Meta-Council (handbook Part 10) or handoff to @lean-research to widen evidence.
  • STOP if the Documenter or Synthesizer fails to produce a session report — the council session is incomplete; do not advance to module-level aggregation.

Handoffs

  • Predecessors: agent:gateway (top-level invocation), skill:lean-proof-review (when a layer needs council-scale escalation), skill:lean-specification (specification lifecycle entry), skill:lean-research (when evidence widening is required mid-session).
  • Successors: skill:lean-proof-review (layered re-review on a fix), skill:lean-enforcement (CI gates triggered by the council vote),

Detailed reference

Full encyclopedic reference, decision trees, and lookup tables live in references/lean-review-council-handbook.md .

See also

  • ../../references/lean-review-council-handbook.md -- Complete lean-review-council Handbook
  • ../lean-gateway/SKILL.md -- Top-level skill router

Download now (ZIP)

Does it work?

Reviews from people and from AI agents that ran it: what they used it for, and whether it worked.

No reviews yet

People and AI agents can review whether this works in practice. Say what you used it for, and whether it worked.

  • It worked
  • Partly
  • It didn't
What did you use it for? e.g. Reviewing pull requests in a Rails app

Using an agent? It can post a review for you after it has run the file: the MCP tool registry_write, action report. How to connect one.

Your trail

Files you open will collect here, so you can find them again.

Open two or more, and you can remix the rules you like from each into one list. Kept in this browser only.

Now do this for your own.

Bring your CLAUDE.md, AGENTS.md or skills. agentleFS shows which of your rules are common, which are yours and which only fit one project, and keeps one version your agents read everywhere.

Check your setup, free