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.