From lean-collab
Composes final Lean proofs from solved goals, verifies with lake lean, fixes common tactic errors like bullet indentation and scoping issues, checks for sorry axioms.
npx claudepluginhub mutable-state-inc/lean-collab**Compose, verify, fix if needed, report. BE FAST.** - **Do NOT read source code** (no .rs files, no investigating) - **Do NOT sleep or wait** for locks - **Do NOT explore** the codebase - **If compose fails, report and EXIT immediately** ```bash ./bin/lc compose ``` **If `success: false`**: Report the error message and EXIT. Do not investigate. ```bash cd <lean_project> && lake env lean <outpu...
Fills stubborn 'sorry' placeholders in Lean proofs via strategic refactoring across files within header fence. Delegate for complex proofs when fast fillers fail; uses Lean LSP tools with phased execution.
Proves leaf goals in Lean proofs. Searches prior tactics, reasons mathematically (MATH CARD) first, then translates via REPL. Bypasses all permission prompts—no user approval needed.
VCSDD Phase 5 formal verification coordinator: detects installed tools, writes proof harnesses for Rust/Python/TypeScript, runs tiered proofs/security/purity checks, generates reports, updates proof status.
Share bugs, ideas, or general feedback.
Compose, verify, fix if needed, report. BE FAST.
./bin/lc compose
If success: false: Report the error message and EXIT. Do not investigate.
cd <lean_project> && lake env lean <output> 2>&1
Empty output = success → Step 4.
Common fixable errors:
| Error Pattern | Fix |
|---|---|
unsolved goals after constructor | Add bullet points · before each child tactic |
unknown identifier 'x' after intro x | Indent continuation lines under the bullet (scope issue) |
unknown identifier 'X' | Check if X was introduced - may need import or scope fix |
expected token near tactic | Check semicolons, indentation |
Nested constructor indentation wrong | Align bullets at same level as parent tactic |
Bullet point fix example:
-- WRONG:
constructor
tactic1
tactic2
-- RIGHT:
constructor
· tactic1
· tactic2
CRITICAL: Scope fix for intro/have:
-- WRONG (x not in scope for have):
· intro x hx
have h : P x := ... -- x is unknown here!
-- RIGHT (indent under bullet to stay in scope):
· intro x hx
have h : P x := ...
exact h
-- OR chain with semicolons:
· intro x hx; have h : P x := ...; exact h
Nested decomposition example:
constructor
· constructor
· inner_tactic1
· inner_tactic2
· outer_tactic2
After each fix, re-verify with lake env lean.
Do NOT read source code or investigate why errors happen - just apply pattern fixes.
grep -n sorry <output>
If found, report which lines have axioms.
One line summary: