mlsanityData to 7 Oct 2026

TacticToe: Learning to Prove with Tactics

arXiv 1804.00596 ↗First posted 2 Apr 2018cs.AI cs.LOcited by 43

Not on the map. Why?

Abstract (arXiv)

We implement a automated tactical prover TacticToe on top of the HOL4 interactive theorem prover. TacticToe learns from human proofs which mathematical technique is suitable in each proof situation. This knowledge is then used in a Monte Carlo tree search algorithm to explore promising tactic-level proof paths. On a single CPU, with a time limit of 60 seconds, TacticToe proves 66.4 percent of the 7164 theorems in HOL4's standard library, whereas E prover with auto-schedule solves 34.5 percent. The success rate rises to 69.0 percent by combining the results of TacticToe and E prover.

Key facts. Cited by 43 papers in the map (data through 7 Oct 2026). First posted on arXiv 2 Apr 2018.

Builds on

No reference list yet.

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2021: 8; 2022: 6; 2023: 5; 2024: 15; 2025: 2; 2026: 7.

43 papers.

Sort:

By area:

  1. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  2. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  3. 2022Autoformalization with Large Language Modelscited by 252
  4. 2022HyperTree Proof Search for Neural Theorem Provingcited by 192
  5. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  6. 2022A Survey of Deep Learning for Mathematical Reasoningcited by 124
  7. 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 118
  8. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 80
  9. 2024TheoremLlama: Transforming General-Purpose LLMs into Lean4 Expertscited by 58
  10. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  11. 2024Lean Copilot: Large Language Models as Copilots for Theorem Proving in Leancited by 52
  12. 2021LIME: Learning Inductive Bias for Primitives of Mathematical Reasoningcited by 46
31 more
  1. 2021TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learningcited by 37
  2. 2025Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physicscited by 27
  3. 2024LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN provercited by 25
  4. 2023Lyra: Orchestrating Dual Correction in Automated Theorem Provingcited by 24
  5. 2024Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchicallycited by 22
  6. 2024Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programmingcited by 19
  7. 2024Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4cited by 15
  8. 2024Rigor with Machine Learning from Field Theory to the Poincar'e Conjecturecited by 12
  9. 2021The Role of Entropy in Guiding a Connection Provercited by 8
  10. 2022The Isabelle ENIGMAcited by 8
  11. 2021Online Machine Learning Techniques for Coq: A Comparisoncited by 7
  12. 2024Learning Guided Automated Reasoning: A Brief Surveycited by 7
  13. 2023MizAR 60 for Mizar 50cited by 6
  14. 2021Learning Equational Theorem Provingcited by 5
  15. 2021Generating Symbolic Reasoning Problems with Transformer GANscited by 5
  16. 2023CoProver: A Recommender System for Proof Constructioncited by 5
  17. 2026Neural Theorem Proving for Verification Conditions: A Real-World Benchmarkcited by 4
  18. 2026Event-B Agent: Towards LLM Agent for Formal Model Synthesis and Repaircited by 3
  19. 2021Learning to solve geometric construction problems from imagescited by 2
  20. 2024BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Provingcited by 2
  21. 2024Application of AI to formal methods - an analysis of current trendscited by 2
  22. 2025ProofNet++: A Neuro-Symbolic System for Formal Proof Verification with Self-Correctioncited by 2
  23. 2026Why Agentic Theorem Prover Works: A Statistical Provability Theory of Mathematical Reasoning Modelscited by 1
  24. 2026Neuro-Symbolic Proof Generation for Scaling Systems Software Verificationcited by 1
  25. 2022Feynman on Artificial Intelligence and Machine Learning, with Updatescited by 0
  26. 2024Considerations on Approaches and Metrics in Automated Theorem Generation/Finding in Geometrycited by 0
  27. 2024Towards Automated Functional Equation Proving: A Benchmark Dataset and A Domain-Specific In-Context Agentcited by 0
  28. 2024Learning Rules Explaining Interactive Theorem Proving Tactic Predictioncited by 0
  29. 2026Exponential Sample Complexity Separation between Flat and Hierarchical Agentic Theorem Proverscited by 0
  30. 2026ProofSketcher: Hybrid LLM + Lightweight Proof Checker for Reliable Math/Logic Reasoningcited by 0
  31. 2026Learned Interventions in Lean 4 grindcited by 0