When Does Structured Knowledge Help Neural Theorem Proving?

arXiv:2609.34460v1 Announce Type: new Abstract: 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 syn