Design | Chapter 5 | Prerequisites: 2-The-Proof-Network | 24 min read | Home
5. Navigational Training Data Format
Each training example maps a proof step to navigational labels:
{
"goal_state": "⊢ ∀ x : ℕ, 0 + x = x",
"theorem_id": "Nat.zero_add",
"step_index": 0,
"total_steps": 1,
"nav_labels": {
"structure": -1,
"automation": -1,
"decompose": -1
},
"anchor_labels": [
"nat-arithmetic", "equality", "universal-quantifier",
"omega-solvable", "one-liner"
],
"ground_truth": {
"tactic": "omega",
"premises": [],
"remaining_steps": 0,
"solvable": true
},
"bank_positions": {
"STRUCTURE": [0, 0],
"DOMAIN": [-1, 1],
"DEPTH": [-1, 2],
"AUTOMATION": [-1, 2],
"CONTEXT": [-1, 1],
"DECOMPOSITION": [-1, 1]
}
}
5.1 Tactic-to-Direction Mapping (6-Bank)
The v1 design navigated 3 banks (STRUCTURE, AUTOMATION, DECOMPOSE), giving only 27 direction vectors. Several distinct tactics collapsed to the same coordinates (e.g., intro and apply both at (0, +1, 0)). The expanded 6-bank mapping adds DOMAIN, DEPTH, and CONTEXT directions, giving 729 possible vectors and disambiguating nearly all common tactics.
| Tactic Category | STRUCT | AUTO | DECOMP | DOMAIN | DEPTH | CONTEXT | Representative Tactics |
| Decision procedures | -1 | -1 | -1 | -1 | -1 | 0 | omega, decide, norm_num |
| Simplification | -1 | -1 | 0 | 0 | -1 | 0 | simp, simp_all, ring, field_simp |
| Rewriting | 0 | 0 | 0 | 0 | 0 | 0 | rw, conv, unfold |
| Linear arithmetic | -1 | -1 | -1 | -1 | -1 | +1 | linarith, positivity (uses hyps) |
| Introduction | 0 | +1 | 0 | 0 | 0 | +1 | intro, rintro (creates hyps) |
| Elimination | +1 | +1 | +1 | 0 | +1 | +1 | cases, rcases, obtain |
| Induction | +1 | +1 | +1 | 0 | +1 | 0 | induction, induction' |
| Application | 0 | +1 | 0 | 0 | 0 | 0 | apply, exact, refine |
| Subgoal creation | 0 | +1 | +1 | 0 | +1 | +1 | have, suffices, calc |
| Assumption | -1 | -1 | -1 | 0 | -1 | -1 | assumption, exact?, trivial |
| Contradiction | +1 | +1 | 0 | 0 | 0 | +1 | contradiction, exfalso (uses hyps) |
| Automation with hints | -1 | 0 | 0 | 0 | 0 | 0 | aesop, tauto, push_neg |
| Type coercion | 0 | -1 | 0 | -1 | -1 | 0 | norm_cast, push_cast |
Key disambiguations from 6-bank expansion:
intro(CONTEXT=+1, creates hypotheses) vsapply(CONTEXT=0, consumes the goal)cases(CONTEXT=+1, adds hypotheses per case) vsinduction(CONTEXT=0, structural)linarith(CONTEXT=+1, uses hypotheses) vsomega(CONTEXT=0, self-contained)assumption(CONTEXT=-1, discharges from context) vs other closers
Bank semantics:
- STRUCTURE -1 = reduces structural complexity (decides, simplifies)
- STRUCTURE +1 = increases structural complexity (introduces cases, subgoals)
- AUTOMATION -1 = requires no human insight
- AUTOMATION +1 = requires choosing what to apply/introduce
- DECOMPOSE +1 = creates new subgoals
- DOMAIN -1 = concrete/computational domain (naturals, integers)
- DOMAIN +1 = abstract/structural domain (topology, categories)
- DEPTH -1 = shallow step (proof gets shorter)
- DEPTH +1 = deep step (proof branches or lengthens)
- CONTEXT -1 = reduces or ignores context (discharges, clears)
- CONTEXT +1 = enriches or uses context (introduces, applies hypotheses)
Graceful degradation: The system supports a navigable_banks config parameter. Setting navigable_banks: [STRUCTURE, AUTOMATION, DECOMPOSITION] reverts to 3-bank navigation if the full 6-bank version proves too hard to learn.
Sources: docs/WAYFINDER_DESIGN.md