Adversarially review Lean proofs

Multi-phase adversarial review of Lean code across 4 dimensions with mechanical fix drafting

Systematic code review covering redundancy, hygiene, faithfulness, and proof-quality with adversarial false-positive killing.

• · Lean file paths

• · findings (id, file, line, decl, dimension, severity, rule, claim, evidence, fix, mechanical, confidence)
• · dedup report
• · draft fixes

• · uv (Python runner)
• · rg (ripgrep)
• · lake (Lean)
• · review/rubric.md
• · finding-schema.json

Lean files present; review assets in place; uv + lake installed; worklist.py available

• · Reviewer emits >100 findings → dedup by (id, highest severity, latest phase)
• · Verifier refutes false positives via evidence check
• · Mechanical fix flag guides fixer safety

• · Findings tied to specific line numbers and declarations
• · Cross-family verifier (refutation-focused)
• · Mechanical fixes isolated and diff-friendly