Generated from folio-assistant-sci/skills/content/folio-paper-adapter/proof-editor.md — do not edit here.
✎ Edit this page’s source

Proof Editor (Coordinator)

Overview

proof-editor is the top-level orchestrator for proof quality. It does not do original analysis — it dispatches to specialist skills, synthesizes their reports, and produces a single prioritized action plan for the author.

Specialists it coordinates:

Specialist	Contribution
`proof-gap-audit`	Intra- and inter-proof gaps (existence, uniqueness, bridges)
`lean-proof-review`	Lean correctness, style, axiom soundness
`lean-completeness-audit`	LaTeX→Lean coverage (what’s stated but not formalized)
`proof-simplifier`	Overlong/brittle Lean proofs, tactic cleanup
`proof-conciseness`	Tighten narrative (human) proofs — cut verbosity without cutting reasoning
`proof-exposition-review`	Retrospective integration — does this proof use content added since it was written?
`proof-narrative-lean-equivalence`	Does the Lean sibling prove the same thing the narrative claims?
`proof-triage`	`sorry` inventory and priority ordering
`remark-audit`	Dangling remarks whose formalization is owed
`content-block-review`	Structural integrity of the block graph
`category-theory`	Diagrammatic / universal-property checks

When to Use This Skill

Author asks: “review my proofs”, “audit this chapter”, “what needs fixing before merge”, “help me finish this proof”
Before opening a PR that touches proof blocks
Post-merge sweep after a large formalization effort
When a reviewer flags multiple concerns and the author wants a consolidated response plan
Not for a single narrow task (e.g. “fix this sorry”) — use the specialist directly

Principle: suggestions, not edits

The editor coordinates — it does not apply changes. Every recommendation goes back to the author with:

A clear description of the gap / issue
The proposed fix (diff, new block, new lemma, etc.)
The specialist skill responsible for implementing it
Dependency ordering (what must be done first)

The author then decides which suggestions to accept and invokes the relevant specialist (or asks the editor to dispatch).

Workflow

Phase 1 — Scope & intake

Determine the scope and check the user’s role:

What is the target? (block | chapter | paper | branch-diff)
What is the user's role? (reader | collaborator | owner)
Which specialists are allowed for that role?
Is there prior review data in proof-objects.json or from the
   agent-review pipeline? (avoid re-running expensive analyses)

Phase 2 — Dispatch specialists in parallel

Launch specialist agents in parallel (single message, multiple Agent tool calls). Each agent runs its own skill on the scoped target.

Default dispatch fan-out:

Target scope	Agents launched
Single proof block	`proof-gap-audit`, `lean-proof-review`, `proof-narrative-lean-equivalence`
Chapter	above + `lean-completeness-audit`, `proof-simplifier`, `proof-conciseness`, `remark-audit`
Paper / branch-diff	above + `proof-triage`, `proof-exposition-review`, `lean-witness-audit`, `content-block-review`

Notes:

proof-narrative-lean-equivalence runs at every tier — it is the only skill that catches Class A “stub weakening” (theorem foo : True := trivial while the narrative claims something substantial).
proof-conciseness operates on .md proof bodies; chapter scope is the natural dispatch point for paper-wide tone consistency.
proof-exposition-review and lean-witness-audit are paper-scope retrospective audits; they are cheap to run on a branch diff because they self-scope to changed blocks.

Ask each agent to produce its report in the standard format with severity levels and concrete remediation suggestions.

Phase 3 — Synthesize

Merge specialist reports into a single finding set:

Deduplicate: the same issue flagged by two skills counts once. Example: a sorry without -- Ref: is flagged by both proof-triage and lean-proof-review — keep the more specific.
Cluster: group findings by affected block so the author can address each block in one pass.
Order by dependency: if fixing block $A$ invalidates a fix to block $B$ downstream, schedule $A$ first.
Rank by severity:
- critical: proof invalid as written, circular dep, conjectural propagation violation
- major: missing lemma, uniqueness/existence gap, broken chain
- minor: style, verbosity, hand-wave that’s defensible
Attach ownership: which specialist skill should the author invoke to apply the fix?

Phase 4 — Produce action plan

Deliver a single markdown document with the structure shown under Output format. Include:

Executive summary (counts, blockers)
Per-block findings in dependency order
Concrete suggested edits (diffs, new lemma statements, etc.)
Dispatch table: which skill to invoke for each fix
Links to affected files (GitHub blob URLs on the current branch, per AGENTS.md)

Phase 5 — Handoff

Present the plan to the author. Offer a numbered list of next actions so the author can reply with “1” or “1,3,5”. Do not begin applying fixes without explicit approval.

If the author says “apply all” or “go ahead”:

Dispatch each fix to its owner skill, in dependency order
After each batch, re-run the relevant specialists to confirm the gap is closed
Produce a delivery summary per .claude/skills/local/delivery-summary.md

Output format

## Proof Editor Report: <scope>

### Executive Summary
- Blocks reviewed: N
- Critical findings: N (blockers)
- Major findings: N
- Minor findings: N
- Estimated fix order: <dependency-ordered list of block labels>

### Findings (in dependency order)

#### 1. `prop:harmonic-decomp` — 2 critical, 1 major
**GitHub**: <repo-url>/blob/<branch>/content/.../harmonic-decomp.md

- [critical, proof-gap-audit] Existence of harmonic representative
  asserted but not constructed. Proof says "choose $h \in \ker \Delta$"
  with no argument for non-emptiness.
  - **Fix**: add lemma `lem:harmonic-nonempty` showing
    `ker Δ ≠ ∅` via spectral decomposition, or cite [author2004].
  - **Owner skill**: `formalizer` (+ `lean-generation` for the stub)

- [critical, lean-proof-review] `sorry` at line 83 missing `-- Ref:`.
  - **Fix**: add `-- Ref: [author2004] https://doi.org/...` or replace
    with a proof.
  - **Owner skill**: `proof-triage`

- [major, proof-simplifier] 40-line proof uses `simp only` with 12
  lemmas; `aesop` closes the goal.
  - **Fix**: replace with `aesop` + comment noting the specific
    lemmas for readers.
  - **Owner skill**: `proof-simplifier`

#### 2. `thm:lifting-exists` — 1 major
...

### Dispatch Table

| Fix # | Block | Owner skill | Blocked by |
|-------|-------|------------|-----------|
| 1.1 | prop:harmonic-decomp | formalizer | — |
| 1.2 | prop:harmonic-decomp | proof-triage | 1.1 |
| 1.3 | prop:harmonic-decomp | proof-simplifier | 1.2 |
| 2.1 | thm:lifting-exists | formalizer | 1.1 |

### Next Actions (pick a number)
1. Apply all critical fixes in order (dispatches 1.1, 1.2, 2.1)
2. Apply all fixes (critical + major + minor)
3. Apply only fix 1.1 (the blocking existence gap)
4. Show me the suggested diff for fix 1.3 before deciding
5. Skip the report — I'll handle it manually

Coordination rules

Role gating: route findings only to skills the user’s role can invoke. A reader gets a report but cannot dispatch collaborator-only fixers.
Idempotence: running the editor twice on an unchanged branch should produce the same report. Cache specialist outputs via proof-objects.json review entries when possible.
No silent edits: the editor never writes to .ts, .md, or .lean files. Dispatch skills do that, under author approval.
Honest confidence: if a specialist reports low confidence (< 0.7), surface that to the author — don’t smooth it over.
Link every finding to a GitHub blob URL, per turn-reporting §”Asking for review means linking the artefact”. Default to .md for block citations; include .lean sibling when the finding is Lean-specific.
Downstream-consumer sync. When a finding touches a proposition consumed by a derived chain (e.g. an algorithm or appendix block whose uses[] cites the proposition), include in the action plan a check that the consuming block still cites the (possibly-modified) proposition correctly. If the proof edit changes the proposition statement or its name, every consumer’s uses[] and any Correctness conditions section must update in the same PR.

Integration

Invoked by: editor skill (top-level router) when the user asks for proof review / audit at chapter or paper scope
Dispatches: all skills listed under Overview
Produces: single action plan; no file edits
Follows up: delivery-summary after approved fixes are applied