Goal 8 — Verified proof-path generation (gate G8)

[duckyquang]

Simplification + equational ATP, with a verifier gating every step.

Sub-goals

• 8.0 Search harness: best-first/beam over rewrites, verifier gate on every step (e-graph/SymPy/numeric tiers), budgets + full search telemetry
• 8.1 Value head trained on step-distance labels (from 6.1 traces) to guide search
• 8.2 Proof benchmark: held-out identity families, length-OOD (proofs longer than training traces), difficulty tiers
• 8.3 ATP comparison: guided-GNN vs uniform search vs transformer-proposer, all verifier-gated — success rate, nodes expanded, proof length, length-OOD
• 8.4 Simplification mode (goal discovery): search for minimal form with a cost function — reuse Goal 4/5 exact-cost machinery as the objective; compare against SymPy simplify as reference
• 8.5 Analysis + report; frontier-LLM reference run (LLM as step-proposer through the same verifier — reference ceiling, not controlled baseline)
• 8R Reserved repair pass

Gate G8

Guided search beats uniform search on nodes-expanded at equal success rate; zero invalid steps emitted (the verifier guarantee holds end-to-end).

Depends on Goals 6–7.