mlsanityData to 7 Oct 2026

The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq

arXiv 2008.00120 ↗First posted 31 Jul 2020cs.AI cs.LOcited by 23

Not on the map. Why?

Abstract (arXiv)

We present Tactician, a tactic learner and prover for the Coq Proof Assistant. Tactician helps users make tactical proof decisions while they retain control over the general proof strategy. To this end, Tactician learns from previously written tactic scripts and gives users either suggestions about the next tactic to be executed or altogether takes over the burden of proof synthesis. Tactician's goal is to provide users with a seamless, interactive, and intuitive experience together with robust and adaptive proof automation. In this paper, we give an overview of Tactician from the user's point of view, regarding both day-to-day usage and issues of package dependency management while learning in the large. Finally, we give a peek into Tactician's implementation as a Coq plugin and machine learning platform.

Key facts. Cited by 23 papers in the map (data through 7 Oct 2026). First posted on arXiv 31 Jul 2020.

Builds on

No reference list yet.

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2021: 2; 2022: 1; 2023: 0; 2024: 11; 2025: 5; 2026: 4.

23 papers.

Sort:

By area:

  1. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  2. 2024Lean Copilot: Large Language Models as Copilots for Theorem Proving in Leancited by 52
  3. 2025Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physicscited by 27
  4. 2024Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verificationcited by 25
  5. 2024Graph2Tac: Online Representation Learning of Formal Math Conceptscited by 15
  6. 2024CoqPilot, a plugin for LLM-based generation of proofscited by 10
  7. 2025A Contemporary Survey of Large Language Model Assisted Program Analysiscited by 10
  8. 2022The Isabelle ENIGMAcited by 8
  9. 2024Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verificationcited by 8
  10. 2021Online Machine Learning Techniques for Coq: A Comparisoncited by 7
  11. 2024Learning Guided Automated Reasoning: A Brief Surveycited by 7
  12. 2024Specify What? Enhancing Neural Specification Synthesis by Symbolic Methodscited by 6
11 more
  1. 2025Agentic Verification of Software Systemscited by 5
  2. 2024QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learningcited by 3
  3. 2025RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generationcited by 3
  4. 2025A Case Study on the Effectiveness of LLMs in Verification with Proof Assistantscited by 3
  5. 2026Event-B Agent: Towards LLM Agent for Formal Model Synthesis and Repaircited by 3
  6. 2024The Tactician's Web of Large-Scale Formal Knowledgecited by 1
  7. 2026Harnessing Code Agents for Automatic Software Verificationcited by 1
  8. 2024Towards Automated Functional Equation Proving: A Benchmark Dataset and A Domain-Specific In-Context Agentcited by 0
  9. 2024Learning Rules Explaining Interactive Theorem Proving Tactic Predictioncited by 0
  10. 2026Can Open-Weight LLMs Produce Kernel-Verified Coq Proofs? A Pilot Studycited by 0
  11. 2026PROVE-RT: Generating Mechanized Theorem Prover Scripts for Real-Time Systems using LLMscited by 0