mlsanityData to 7 Oct 2026

Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers

arXiv 2205.10893 ↗First posted 22 May 2022cs.AIcited by 97

Not on the map. Why?

Cited by 22 in LLM reasoning, but placed by its own abstract, which didn’t fit.

Abstract (arXiv)

In theorem proving, the task of selecting useful premises from a large library to unlock the proof of a given conjecture is crucially important. This presents a challenge for all theorem provers, especially the ones based on language models, due to their relative inability to reason over huge volumes of premises in text form. This paper introduces Thor, a framework integrating language models and automated theorem provers to overcome this difficulty. In Thor, a class of methods called hammers that leverage the power of automated theorem provers are used for premise selection, while all other tasks are designated to language models. Thor increases a language model's success rate on the PISA dataset from 39% to 57%, while solving 8.2% of problems neither language models nor automated theorem provers are able to solve on their own. Furthermore, with a significantly smaller computational budget, Thor can achieve a success rate on the MiniF2F dataset that is on par with the best existing methods. Thor can be instantiated for the majority of popular interactive theorem provers via a straightforward protocol we provide.

Key facts. Cited by 97 papers in the map (data through 7 Oct 2026). Builds on 14 of its 49 references that are in the map. First posted on arXiv 22 May 2022.

Builds on

14 of 49 references.

References · 14

  1. 2017Attention Is All You Needcited by 59,932
  2. 2021RoFormer: Enhanced Transformer with Rotary Position Embeddingcited by 4,581
  3. 2020The Pile: An 800GB Dataset of Diverse Text for Language Modelingcited by 2,346
  4. 2017Mastering Chess and Shogi by Self-Play with a General Reinforcement Learning Algorithmcited by 723
  5. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 380
  6. 2020Generative Language Modeling for Automated Theorem Provingcited by 379
  7. 2022Formal Mathematics Statement Curriculum Learningcited by 141
  8. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  9. 2016DeepMath - Deep Sequence Models for Premise Selectioncited by 80
  10. 2022Structured, flexible, and robust: benchmarking and improving large language models towards more human-like behavior in out-of-distribution reasoning taskscited by 56
  11. 2017Premise Selection for Theorem Proving by Deep Graph Embeddingcited by 44
  12. 2017HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Provingcited by 26
2 more
  1. 2013HOL(y)Hammer: Online ATP Service for HOL Lightcited by 8
  2. 2015Premise Selection and External Provers for HOL4cited by 7

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2022: 5; 2023: 23; 2024: 30; 2025: 26; 2026: 13.

97 papers.

Sort:

By area:

  1. 2023A Survey of Large Language Modelscited by 2,537
  2. 2022Solving Quantitative Reasoning Problems with Language Modelscited by 1,359
  3. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  4. 2023Llemma: An Open Language Model For Mathematicscited by 385
  5. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  6. 2022Autoformalization with Large Language Modelscited by 252
  7. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 225
  8. 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 189
  9. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 180
  10. 2023Progressive-Hint Prompting Improves Reasoning in Large Language Modelscited by 147
  11. 2023Focused Transformer: Contrastive Training for Context Scalingcited by 133
  12. 2022A Survey of Deep Learning for Mathematical Reasoningcited by 124
38 more
  1. 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 118
  2. 2024Lean Workbook: A large-scale Lean problem set formalized from natural language math problemscited by 115
  3. 2022Teaching Algorithmic Reasoning via In-context Learningcited by 111
  4. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 108
  5. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 80
  6. 2023An In-Context Learning Agent for Formal Theorem-Provingcited by 78
  7. 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Provingcited by 77
  8. 2024TheoremLlama: Transforming General-Purpose LLMs into Lean4 Expertscited by 58
  9. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  10. 2023FIMO: A Challenge Formal Dataset for Automated Theorem Provingcited by 54
  11. 2024Lean Copilot: Large Language Models as Copilots for Theorem Proving in Leancited by 52
  12. 2023Magnushammer: A Transformer-Based Approach to Premise Selectioncited by 50
  13. 2025Aristotle: IMO-level Automated Theorem Provingcited by 47
  14. 2024AutoVerus: Automated Proof Generation for Rust Codecited by 46
  15. 2023Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Provingcited by 37
  16. 2024miniCTX: Neural Theorem Proving with (Long-)Contextscited by 35
  17. 2025Solving Formal Math Problems by Decomposition and Iterative Reflectioncited by 35
  18. 2024LeanAgent: Lifelong Learning for Formal Theorem Provingcited by 34
  19. 2023FormalGeo: An Extensible Formalized Framework for Olympiad Geometric Problem Solvingcited by 26
  20. 2024Proving Theorems Recursivelycited by 25
  21. 2024Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verificationcited by 25
  22. 2023Lyra: Orchestrating Dual Correction in Automated Theorem Provingcited by 24
  23. 2023TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Modelscited by 24
  24. 2023Mathematical Language Models: A Surveycited by 24
  25. 2024FunBO: Discovering Acquisition Functions for Bayesian Optimization with FunSearchcited by 22
  26. 2024FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Provingcited by 22
  27. 2024Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchicallycited by 22
  28. 2024Proof Automation with Large Language Modelscited by 20
  29. 2024Consistent Autoformalization for Constructing Mathematical Librariescited by 20
  30. 2024Graph2Tac: Online Representation Learning of Formal Math Conceptscited by 15
  31. 2024Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4cited by 15
  32. 2023Adapting Large Language Models for Education: Foundational Capabilities, Potentials, and Challengescited by 13
  33. 2025A Survey on Mathematical Reasoning and Optimization with Large Language Modelscited by 12
  34. 2024SubgoalXL: Subgoal-based Expert Learning for Theorem Provingcited by 11
  35. 2024Data for Mathematical Copilots: Better Ways of Presenting Proofs for Machine Learningcited by 11
  36. 2023AI for Mathematics: A Cognitive Science Perspectivecited by 10
  37. 2025Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Taskscited by 9
  38. 2024Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verificationcited by 8

50 most cited of 97 All 97 (JSON)