When Does Structured Knowledge Help Neural Theorem Proving?

Does structured mathematical knowledge help LLMs prove theorems in Lean 4? If so, for which models, and does the answer vary by problem? Formal libraries such as Mathlib encode 285,000+ verified theorems with syntactic dependencies, but the semantic layer mathematicians rely on for discovery, such as analogies, generalizations, and cross-domain bridges, remains implicit. We introduce MathAgent, a system that builds this missing layer as a knowledge graph called MathKG, and uses it to augment LLM theorem provers. MathKG connects 364 Mathlib theorems and definitions by 9,434 typed semantic edges, inferred via LLM-based relation extraction anchored to verified Mathlib declarations. We run a controlled ablation across four augmentation modes (no external context, knowledge-graph context, Mathlib library retrieval, and both combined) and five models: the general-purpose Qwen3-8B/32B, their Lean-specialized derivatives Goedel-Prover-V2-8B/32B, and the proprietary Claude Sonnet 4.6. We evaluate on miniF2F, adding PutnamBench and MathOlympiadBench for the proprietary model. Three findings emerge. (i) Specialization dominates augmentation by an order of magnitude: Lean fine-tuning adds 33–38 percentage points of solve rate in every augmentation mode, and a specialized 8B model even beats a $4\times$ larger general one by 29–35 points in every mode; by contrast, no single augmentation mode improves solve rate by more than 3 points, so external knowledge does not substitute for competence in the weights. (ii) Augmentation's aggregate effect is capability-conditioned: knowledge-graph context helps small models but hurts large ones, with the specialized model gaining more relative to its general base at every scale. (iii) Yet across every model the augmentation modes solve different problems, so an oracle that selects the best augmentation mode per problem solves 6% to 58% more problems than the unaugmented prover (least for the proprietary model, most for a weak general one), revealing a complementarity effect that strengthens on harder problems. Together these results motivate adaptive strategies that select augmentation by model capability and problem. Code, data, and artifacts will be released upon publication.