mlsanityData to 7 Oct 2026

When Does Structured Knowledge Help Neural Theorem Proving?

arXiv 2609.34460 ↗First posted 28 Sep 2026cs.AI cs.LG cs.LOcited by 0

Not on the map. Why?

Abstract (arXiv)

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 (analogies, generalizations, cross-domain bridges) remains implicit. We introduce MathAgent, which builds this layer as a knowledge graph, 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 context, knowledge-graph context, Mathlib retrieval, both) and five models: Qwen3-8B/32B, their Lean-specialized derivatives Goedel-Prover-V2-8B/32B, and Claude Sonnet 4.6, on miniF2F, plus PutnamBench and MathOlympiadBench for Sonnet. Three findings emerge. (i) Specialization dominates augmentation: Lean fine-tuning adds 33-38 percentage points of solve rate in every mode, and a specialized 8B model beats a 4× larger general one by 29-35 points, while no augmentation mode improves solve rate by more than 3 points. (ii) Augmentation 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 the augmentation modes solve different problems: an oracle selecting the best mode per problem solves 6% to 58% more than the unaugmented prover, a complementarity effect that strengthens on harder problems (32% more on PutnamBench). These results motivate adaptive strategies that select augmentation by model capability and problem. Code, data, and artifacts are available at https://github.com/sarehnabi/mathagent

Key facts. No citing papers in the map yet (data through 7 Oct 2026). Builds on 52 of its 71 references that are in the map. First posted on arXiv 28 Sep 2026.

Builds on

52 of 71 references.

References · 52

  1. 2025Qwen3 Technical Reportcited by 8,195
  2. 2023AutoGen: Enabling Next-Gen LLM Applications via Multi-Agent Conversationcited by 1,906
  3. 2023MetaGPT: Meta Programming for A Multi-Agent Collaborative Frameworkcited by 1,761
  4. 2022Solving Quantitative Reasoning Problems with Language Modelscited by 1,359
  5. 2022When Not to Trust Language Models: Investigating Effectiveness of Parametric and Non-Parametric Memoriescited by 1,103
  6. 2025AlphaEvolve: A coding agent for scientific and algorithmic discoverycited by 763
  7. 2023WizardMath: Empowering Mathematical Reasoning for Large Language Models via Reinforced Evol-Instructcited by 618
  8. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  9. 2023Llemma: An Open Language Model For Mathematicscited by 385
  10. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 380
  11. 2020Generative Language Modeling for Automated Theorem Provingcited by 379
  12. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
38 more
  1. 2025DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decompositioncited by 270
  2. 2022Autoformalization with Large Language Modelscited by 252
  3. 2022HyperTree Proof Search for Neural Theorem Provingcited by 192
  4. 2023Large Language Models for Generative Information Extraction: A Surveycited by 183
  5. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 180
  6. 2025Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learningcited by 173
  7. 2024PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competitioncited by 153
  8. 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correctioncited by 140
  9. 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 126
  10. 2023Revisiting Relation Extraction in the era of Large Language Modelscited by 100
  11. 2025Seed-Prover: Deep and Broad Reasoning for Automated Theorem Provingcited by 96
  12. 2016DeepMath - Deep Sequence Models for Premise Selectioncited by 80
  13. 2021NaturalProofs: Mathematical Theorem Proving in Natural Languagecited by 80
  14. 2023An In-Context Learning Agent for Formal Theorem-Provingcited by 78
  15. 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Provingcited by 77
  16. 2025Mathematical exploration and discovery at scalecited by 66
  17. 2025Hilbert: Recursively Building Formal Proofs with Informal Reasoningcited by 55
  18. 2024Lean Copilot: Large Language Models as Copilots for Theorem Proving in Leancited by 52
  19. 2023Magnushammer: A Transformer-Based Approach to Premise Selectioncited by 50
  20. 2022Generative Knowledge Graph Construction: A Reviewcited by 49
  21. 2023Lemur: Integrating Large Language Models in Automated Program Verificationcited by 49
  22. 2025Aristotle: IMO-level Automated Theorem Provingcited by 47
  23. 2017Premise Selection for Theorem Proving by Deep Graph Embeddingcited by 44
  24. 2025Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experiencecited by 36
  25. 2025Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Proverscited by 26
  26. 2025REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoningcited by 18
  27. 2026Advancing Mathematics Research with AI-Driven Formal Proof Searchcited by 18
  28. 2026LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworkscited by 11
  29. 2026Scaling Self-Play with Self-Guidancecited by 9
  30. 2025DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theoremscited by 8
  31. 2025HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMscited by 8
  32. 2026LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Provingcited by 7
  33. 2025AutoMathKG: The automated mathematical knowledge graph based on LLM and vector databasecited by 6
  34. 2026Formalizing Mathematics at Scalecited by 5
  35. 2026The Network Structure of Mathlibcited by 4
  36. 2026TheoremGraph: Bridging Formal and Informal Mathematicscited by 4
  37. 2026Pseudo-Formalization for Automatic Proof Verificationcited by 3
  38. 2026Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisationcited by 3

50 most cited of 52 All 52 (JSON)

Built on by

Not cited yet.