Origin
docs/ROADMAP.md Research Goals (v2.0.0+ — 2027+) section corresponds to the echidnabot ROADMAP.adoc:169 line:
Cross-referenced in echidna's docs/ROADMAP.md under the long-tail research track (after Stages 5-8 complete).
Scope
Generate proof sketches (informal partial proofs) from a goal statement, which a human or further automation completes:
- Sketch generator trained on the corpus accumulated under Wave-3 (
training_data/, 553 MB, 66 674 proofs)
- Output formats: natural-language Isar-style sketches for IPAs; tactic skeletons for SMT-backed assistants
- Evaluation harness: sketch quality measured by completion rate against held-out theorems
- Integration: optional dispatcher mode that emits a sketch when no backend solves outright
Aspirational scope — this is Research v2.0.0+, no PR-count estimate (long-tail enumeration flags it as aspirational rather than scoped).
Dependencies
- S2 (training on the fixed corpus) must land first; the sketch generator is downstream of trained weights at
models/neural/
- GNN integration (v2.1, shipped) provides the embedding substrate
- All Stage 5-8 production-hardening must land first (the platform must be stable enough to host a research feature)
- No upstream blocker
Why filed
To make the Research v2.0.0+ commitment trackable. Today the line lives only as a single bullet in echidnabot/ROADMAP.adoc:169 with no echidna-side tracker; filing here gives the owner a place to attach design notes, ADRs, and PRs when the time comes. Explicitly aspirational so the issue can sit open for years without being a stale-issue signal.
Origin
docs/ROADMAP.mdResearch Goals (v2.0.0+ — 2027+) section corresponds to the echidnabot ROADMAP.adoc:169 line:Cross-referenced in echidna's
docs/ROADMAP.mdunder the long-tail research track (after Stages 5-8 complete).Scope
Generate proof sketches (informal partial proofs) from a goal statement, which a human or further automation completes:
training_data/, 553 MB, 66 674 proofs)Aspirational scope — this is Research v2.0.0+, no PR-count estimate (long-tail enumeration flags it as aspirational rather than scoped).
Dependencies
models/neural/Why filed
To make the Research v2.0.0+ commitment trackable. Today the line lives only as a single bullet in echidnabot/ROADMAP.adoc:169 with no echidna-side tracker; filing here gives the owner a place to attach design notes, ADRs, and PRs when the time comes. Explicitly aspirational so the issue can sit open for years without being a stale-issue signal.