Design | Chapter 1 | 24 min read | Home
1. Design Thesis
Navigation, not prediction. The central design decision in Wayfinder is that proof search should be spatial navigation through structured mathematical space rather than sequential token prediction. This has a concrete architectural consequence: the neural network runs once per proof state to produce navigational coordinates, and all subsequent operations — premise retrieval, tactic resolution, search prioritization — are deterministic symbolic operations on a precomputed semantic network.
This design is directly adapted from ModelAtlas (Vinaik, 2025), which demonstrated that structured navigation over signed semantic coordinates outperforms both flat database queries and dense embedding retrieval for finding ML models on HuggingFace. We apply the same paradigm to mathematical entities: lemmas, tactics, and proof states are positioned in a structured coordinate system; retrieval is multiplicative bank alignment × IDF-weighted anchor relevance × seed similarity.
The thesis is falsifiable. If dense retrieval consistently outperforms structured navigation for premise selection (Phase 2.2 of the plan), the navigational paradigm is wrong for this domain. If tactic classification outperforms navigational coordinates (Phase 4.4 ablation), the ternary decoder design is wrong. Both negative results would be informative.
Sources: docs/WAYFINDER_DESIGN.md