Cascade Hunter

Search academic literature, build dependency graphs of mathematical results, and hunt for high-impact errors that cascade through downstream work.

End-to-End Pipeline
INPUT Search Config (JSON) search verify MODULE 1 — SEARCH 1a Queries 1b Search ×6 1c Score & Select 1d LaTeX 1e Extract 1f Dep Map Dependency Graph MODULE 2 — VERIFICATION Key Select Proof Recovery Skeleton → Critical Path → Verify N parallel verifiers per critical step dismiss counter audit FP Impact → REPORT.md dependency graph feeds verification
Data source
LLM / agent call
Deterministic
Audit gate
Input / output

Module 1 — Search

Generates queries from a topic config, searches 6 academic APIs in parallel, scores papers by theoretical density and domain fit, downloads LaTeX, extracts formal results, and builds a dependency graph.

Module 2 — Verification

Decomposes proofs into skeleton steps, identifies load-bearing steps via BFS from main theorems, runs N parallel verifiers per step, then filters false positives through 3 gates before tracing impact downstream.

Infrastructure

GPT + Claude dual provider. CLI or API mode. Per-phase checkpointing with resume. Full I/O logging per LLM call.

Module 2: Verification
PHASE 2a Key Result Selection LLM selects top results per paper; globally re-ranked by priority PHASE 2b Proof Recovery extract proof from LaTeX; fallback: LLM locates it in source SKELETON DECOMPOSITION PHASE 2c Skeleton Extraction decompose proof into 4–10 atomic steps each: claim + technique + dependencies + LaTeX excerpt S1 S2 S3 ★ S4 S5 ★ ★ = load-bearing 2c2 Coherence Verification if steps are all true, does the chain prove the theorem? 2c3 Source Cross-Validation verify the extracted proof actually belongs to this theorem misattributed? → filter out PHASE 2d — CRITICAL PATH algorithmic (no LLM) M critical on path off path BFS from main theorems along hard edges; select load-bearing + external-invocation steps PHASE 2e — FOCUSED STEP VERIFICATION each critical step verified independently by N parallel LLM calls Verifier 1 ✓ Verifier 2 ✗ Verifier 3 ✗ consensus: ≥ 2 agree → flag FALSE-POSITIVE REDUCTION — 3 gates in series Gate 1: Dismissal LLM tries to defend the proof fatal structural cosmetic artifact × Gate 2: Counterexample try to construct specific values that break the step's claim found + verified → upgrade to fatal Gate 3: Audit re-read raw LaTeX source confirm / resolve / uncertain many flagged fatal + structural only confirmed errors PHASE 2f — Impact Propagation trace each error through dependency graph to main theorems classify: catastrophic / repairable / contained ! Thm 3.1 Cor 3.2 Thm 4.1 3 more...
REPORT.md hierarchical error report organized by impact to main theorems
FATAL STRUCTURAL COSMETIC

Skeleton Decomposition

Each proof is decomposed into 4–10 atomic steps. Each step records its claim, technique, dependencies on prior steps, and external results invoked. Two quality checks verify coherence and source attribution.

Critical Path

Algorithmic BFS from main theorems through hard dependency edges. Only load-bearing and external-invocation steps are verified—focusing effort where errors would cascade farthest.

3-Gate FP Reduction

Dismissal tries to defend the proof; counterexample tries to break the step claim with specific values; audit re-reads raw LaTeX. Errors surviving all three gates are classified as fatal/structural/cosmetic.