Experiment Plan | Chapter 4 | Prerequisites: Phase-1 | 28 min read | Home

Phase 2: Navigation Training (Week 3-5)

Goal: Train the navigational components and validate that the proof network enables meaningful retrieval. Code status: Training script (train_navigator.py), eval scripts (eval_retrieval.py, eval_spreading.py), and config (wayfinder.yaml) all implemented. Awaiting Phase 0-1 data.

2.0 Literature Review: Lean4 Proof Search Algorithms

What: Survey existing work on proof search termination, progress estimation, and potential functions in interactive theorem provers. The Mutation Theory connections (trajectory monotonicity, Lyapunov convergence) may have tighter domain-specific analogs in the ITP literature.

Already completed: Initial survey in docs/Wayfinder_External_Research.md covers 8 major systems. Key findings already incorporated:

  • AlphaProof uses remaining-tactic-count as value target (adopted for critic head)
  • HTPS: soft critic targets >> hard binary (adopted)
  • LeanProgress: proof history gives 13-point improvement (adopted)
  • BFS-Prover: best-first search competitive with MCTS when policy is strong
  • No system uses knowledge graph navigation for proof search (validates novelty)
  • LeanHammer hybrid achieves 37.3% (hammer integration adopted)

Remaining areas to investigate:

  • Well-founded recursion and termination metrics in Lean 4 itself
  • Proof complexity measures (proof tree depth, cut-rank, quantifier depth) as alternative Lyapunov function candidates — raw step count may not be the best training target for the progress head
  • QEDCartographer's reward-free RL for state values — compare to our Lyapunov approach
  • Crouse et al.'s GNN-based proof length prediction in first-order logic
  • Formal connection between proof complexity and teaching dimension (T5.17)

Output: Annotated bibliography in docs/RELATED_PROOF_SEARCH.md. Focus on: (1) better progress head training targets, (2) formal convergence criteria, (3) any existing structured retrieval approaches we may have missed.

Time: 2-3 days concurrent with Phase 1/2 implementation.

2.1 Navigational Direction Training

What: Train the ProofNavigator to predict correct navigational directions from goal state embeddings.

How:




---
*Sources: `docs/WAYFINDER_PLAN.md`*
## See Also

- [Phase-1](../phase-1/)
- [Phase-3](../phase-3/)