When Does Structured Knowledge Help Neural Theorem Proving?
cs.AI, cs.LG, cs.LO
Submitted: 2026-09-28
Updated: 2026-09-28
Code: https://github.com/sarehnabi/mathagent
Project page: https://sarehnabi.github.io/mathagent
Sources
- Aristotle: IMO-level Automated Theorem Proving
- Remarks on the disproof of the unit distance conjecture
- ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics
- Scaling Self-Play with Self-Guidance
- Pseudo-Formalization for Automatic Proof Verification
- Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience
- Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving
- STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
- LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving
- Mathematical exploration and discovery at scale
- Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs
- LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks
- TheoremGraph: Bridging Formal and Informal Mathematics
- Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation
- Scaling Natural-Language Graph-Based Test Time Compute for Automated Theorem Proving
- The Network Structure of Mathlib
- Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving
- AlphaEvolve: A coding agent for scientific and algorithmic discovery
- Integer values of $\tan(\arctan 1+\arctan 2+\cdots+\arctan n)$ are rare
- TheoremBench: Evaluating LLMs on Theorem Proving in Formal Mathematics
Related papers
- MAVEN-T: Reinforced Heterogeneous Distillation for Real-Time Multi-Agent Trajectory Prediction
- Model Discovery Agent: LLM-assisted Bayesian experiment design for data-efficient discovery of mechanistic world models
- Agents' Last Exam
- The Clinician's Veto: Navigating Trust, Liability, and Uncertainty in Autonomous AI Prescribing
- MindHelper: Closed-Loop Embodied Mental-State Reasoning for Precision Intervention
- Incumbent Advantage: Brand Bias and Cognitive Manipulation Dynamics in LLM Recommendation Systems