Experiment Plan | Chapter 2 | Prerequisites: Plan-Overview | 28 min read | Home

Phase 0: Proof Network Construction (Week 1-2)

Goal: Build the semantic network of mathematical entities from Mathlib, and establish the data pipeline. Code status: All scripts implemented (extract_proof_network.py, build_nav_training_data.py, anchor_gap_analysis.py). Awaiting execution on data.

0.1 Obtain LeanDojo Benchmark Data

What: Download LeanDojo's extracted Mathlib dataset — ~98,734 theorems with proof traces, intermediate goal states, and premise information.

How:

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

- [Plan-Overview](../plan-overview/)
- [Phase-1](../phase-1/)