mlsanityData to 7 Oct 2026

DeepMath - Deep Sequence Models for Premise Selection

arXiv 1606.04442 ↗First posted 14 Jun 2016cs.AI cs.LG cs.LOcited by 80

Not on the map. Why?

Abstract (arXiv)

We study the effectiveness of neural sequence models for premise selection in automated theorem proving, one of the main bottlenecks in the formalization of mathematics. We propose a two stage approach for this task that yields good results for the premise selection task on the Mizar corpus while avoiding the hand-engineered features of existing state-of-the-art models. To our knowledge, this is the first time deep learning has been applied to theorem proving on a large scale.

Key facts. Cited by 80 papers in the map (data through 7 Oct 2026). First posted on arXiv 14 Jun 2016.

Builds on

No reference list yet.

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2021: 11; 2022: 10; 2023: 12; 2024: 17; 2025: 19; 2026: 11.

80 papers.

Sort:

By area:

  1. 2022Solving Quantitative Reasoning Problems with Language Modelscited by 1,359
  2. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  3. 2022Autoformalization with Large Language Modelscited by 252
  4. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 180
  5. 2022Formal Mathematics Statement Curriculum Learningcited by 141
  6. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  7. 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 126
  8. 2022A Survey of Deep Learning for Mathematical Reasoningcited by 124
  9. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 108
  10. 2022Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Proverscited by 97
  11. 2021NaturalProofs: Mathematical Theorem Proving in Natural Languagecited by 80
  12. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 80
38 more
  1. 2024Premise Order Matters in Reasoning with Large Language Modelscited by 71
  2. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  3. 2024Lean Copilot: Large Language Models as Copilots for Theorem Proving in Leancited by 52
  4. 2023Magnushammer: A Transformer-Based Approach to Premise Selectioncited by 50
  5. 2024Learning Formal Mathematics From Intrinsic Motivationcited by 45
  6. 2024miniCTX: Neural Theorem Proving with (Long-)Contextscited by 35
  7. 2025Solving Formal Math Problems by Decomposition and Iterative Reflectioncited by 35
  8. 2024LeanAgent: Lifelong Learning for Formal Theorem Provingcited by 34
  9. 2025Prover Agent: An Agent-Based Framework for Formal Mathematical Proofscited by 28
  10. 2025Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physicscited by 27
  11. 2023Mathematical Language Models: A Surveycited by 24
  12. 2024Proof Automation with Large Language Modelscited by 20
  13. 2021Contrastive Reinforcement Learning of Symbolic Reasoning Domainscited by 17
  14. 2021Neural Termination Analysiscited by 16
  15. 2021Learning to Guide a Saturation-Based Theorem Provercited by 15
  16. 2022Peano: Learning Formal Mathematical Reasoningcited by 15
  17. 2025A Survey on Mathematical Reasoning and Optimization with Large Language Modelscited by 12
  18. 2024Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Provingcited by 11
  19. 2021Vampire With a Brain Is a Good ITP Hammercited by 10
  20. 2023Machine-Learned Premise Selection for Leancited by 10
  21. 2025MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curationcited by 10
  22. 2021Learning Symbolic Rules for Reasoning in Quasi-Natural Languagecited by 9
  23. 2022A Survey in Mathematical Language Processingcited by 9
  24. 2023Abstract Visual Reasoning: An Algebraic Approach for Solving Raven's Progressive Matricescited by 9
  25. 2021The Role of Entropy in Guiding a Connection Provercited by 8
  26. 2022The Isabelle ENIGMAcited by 8
  27. 2024Learning Guided Automated Reasoning: A Brief Surveycited by 7
  28. 2025Lean Finder: Semantic Search for Mathlib That Understands User Intentscited by 7
  29. 2024ATG: Benchmarking Automated Theorem Generation for Generative Language Modelscited by 6
  30. 2021Generating Symbolic Reasoning Problems with Transformer GANscited by 5
  31. 2023CoProver: A Recommender System for Proof Constructioncited by 5
  32. 2025Agentic Verification of Software Systemscited by 5
  33. 2021A Study of Continuous Vector Representationsfor Theorem Provingcited by 4
  34. 2025Neural Theorem Proving: Generating and Structuring Proofs for Formal Verificationcited by 4
  35. 2023Lemmas: Generation, Selection, Applicationcited by 3
  36. 2023Reinforcement Learning and Data-Generation for Syntax-Guided Synthesiscited by 3
  37. 2025RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generationcited by 3
  38. 2025A Case Study on the Effectiveness of LLMs in Verification with Proof Assistantscited by 3

50 most cited of 80 All 80 (JSON)