When Does Structured Knowledge Help Neural Theorem Proving?

Sareh Nabi, Roland Vogl, Marzieh Nabi

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…