mlsanityData to 7 Oct 2026

HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving

arXiv 2412.20735 ↗First posted 30 Dec 2024cs.AI cs.CLcited by 32

On the map: LLM reasoning → Mathematical reasoning

also in 1 more
Abstract (arXiv)

We introduce HunyuanProver, an language model finetuned from the Hunyuan 7B for interactive automatic theorem proving with LEAN4. To alleviate the data sparsity issue, we design a scalable framework to iterative synthesize data with low cost. Besides, guided tree search algorithms are designed to enable effective ``system 2 thinking`` of the prover. HunyuanProver achieves state-of-the-art (SOTA) performances on major benchmarks. Specifically, it achieves a pass of 68.4% on the miniF2F-test compared to 65.9%, the current SOTA results. It proves 4 IMO statements (imo_1960_p2, imo_1962_p2}, imo_1964_p2 and imo_1983_p6) in miniF2F-test. To benefit the community, we will open-source a dataset of 30k synthesized instances, where each instance contains the original question in natural language, the converted statement by autoformalization, and the proof by HunyuanProver.

Key facts. Cited by 32 papers in the map (data through 7 Oct 2026). Placed in Mathematical reasoning, one of 17 directions in LLM reasoning. Builds on 15 of its 19 references that are in the map. First posted on arXiv 30 Dec 2024.

Builds on

15 of 19 references.

Closest ancestors · 2

Same direction, newest first

  1. 2024Lean-STaR: Learning to Interleave Thinking and Proving14 Jul
  2. 2023WizardMath: Empowering Mathematical Reasoning for Large Language Models via Reinforced Evol-Instruct18 Aug

Other references · 13

  1. 2024GPT-4o System Cardcited by 4,467
  2. 2023Math-Shepherd: Verify and Reinforce LLMs Step-by-step without Human Annotationscited by 895
  3. 2023MetaMath: Bootstrap Your Own Mathematical Questions for Large Language Modelscited by 724
  4. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  5. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 380
  6. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 225
  7. 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 189
  8. 2024Toward Self-Improvement of LLMs via Imagination, Searching, and Criticizingcited by 123
  9. 2024Lean Workbook: A large-scale Lean problem set formalized from natural language math problemscited by 115
  10. 2024Q*: Improving Multi-step Reasoning for LLMs with Deliberative Planningcited by 95
  11. 2023Multilingual Mathematical Autoformalizationcited by 38
  12. 2024LiteSearch: Efficacious Tree Search for LLMcited by 30
1 more
  1. 2024Proving Olympiad Algebraic Inequalities without Human Demonstrationscited by 20

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2025: 23; 2026: 9.

32 papers.

Sort:

By area:

  1. 2025Towards Reasoning Era: A Survey of Long Chain-of-Thought for Reasoning Large Language Modelscited by 381
  2. 2025DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decompositioncited by 270
  3. 2025Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learningcited by 173
  4. 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correctioncited by 140
  5. 2025BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Provingcited by 82
  6. 2025Aristotle: IMO-level Automated Theorem Provingcited by 47
  7. 2025Solving Formal Math Problems by Decomposition and Iterative Reflectioncited by 35
  8. 2025Prover Agent: An Agent-Based Framework for Formal Mathematical Proofscited by 28
  9. 2025Leanabell-Prover: Posttraining Scaling in Formal Reasoningcited by 27
  10. 2025Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Proverscited by 26
  11. 2025ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Datacited by 23
  12. 2025FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levelscited by 23
20 more
  1. 2025Solving Inequality Proofs with Large Language Modelscited by 21
  2. 2025REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoningcited by 18
  3. 2025Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Modelscited by 17
  4. 2026A Minimal Agent for Automated Theorem Provingcited by 13
  5. 2026AI co-mathematician: Accelerating mathematicians with agentic AIcited by 13
  6. 2025One Example Shown, Many Concepts Known! Counterexample-Driven Conceptual Reasoning in Mathematical LLMscited by 12
  7. 2026AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithmscited by 11
  8. 2025MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curationcited by 10
  9. 2025FormaRL: Enhancing Autoformalization with no Labeled Datacited by 9
  10. 2025Ineq-Comp: Benchmarking Human-Intuitive Compositional Reasoning in Automated Theorem Proving on Inequalitiescited by 8
  11. 2025Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Provingcited by 7
  12. 2026Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinementcited by 7
  13. 2026LongCat-Flash-Prover: Advancing Native Formal Reasoning via Agentic Tool-Integrated Reinforcement Learningcited by 6
  14. 2025ProofCompass: Enhancing Specialized Provers with LLM Guidancecited by 3
  15. 2025Translating Informal Proofs into Formal Proofs Using a Chain of Statescited by 3
  16. 2025EconProver: Towards More Economical Test-Time Scaling for Automated Theorem Provingcited by 1
  17. 2026TheoremBench: Evaluating LLMs on Theorem Proving in Formal Mathematicscited by 1
  18. 2026MA-ProofBench: A Two-Tiered Evaluation of LLMs for Theorem Proving in Mathematical Analysiscited by 1
  19. 2026Rethinking Supervision Granularity: Segment-Level Learning for LLM-Based Theorem Provingcited by 0
  20. 2026TreeThink: A Modular Tree Search Library for Mathematical Reasoning with LLMscited by 0

Similar, not cited

Close in wording, no citation either way

  1. 2025LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation
  2. 2026Direct Optimization of Generators for Search in Automated Theorem Proving
  3. 2025A Combinatorial Identities Benchmark for Theorem Proving via Automated Theorem Generation
  4. 2024MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data
  5. 2025LogicTree: Structured Proof Exploration for Coherent and Rigorous Logical Reasoning with Large Language Models
  6. 2025Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs
  7. 2025MINIF2F-DAFNY: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification
  8. 2025Scaling Natural-Language Graph-Based Test Time Compute for Automated Theorem Proving