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

arXiv: https://arxiv.org/abs/2008.00120 · HTML: https://mlsanity.com/paper/2008.00120/

## Key facts

- Cited by 24 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 31 Jul 2020.

## Built on by (most cited first, 24 of 24)

- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean](https://mlsanity.com/paper/2404.12534/) (2024)
- [Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics](https://mlsanity.com/paper/2510.12787/) (2025)
- [Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification](https://mlsanity.com/paper/2412.14063/) (2024)
- [Graph2Tac: Online Representation Learning of Formal Math Concepts](https://mlsanity.com/paper/2401.02949/) (2024)
- [CoqPilot, a plugin for LLM-based generation of proofs](https://mlsanity.com/paper/2410.19605/) (2024)
- [A Contemporary Survey of Large Language Model Assisted Program Analysis](https://mlsanity.com/paper/2502.18474/) (2025)
- [Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verification](https://mlsanity.com/paper/2410.19940/) (2024)
- [The Isabelle ENIGMA](https://mlsanity.com/paper/2205.01981/) (2022)
- [Online Machine Learning Techniques for Coq: A Comparison](https://mlsanity.com/paper/2104.05207/) (2021)
- [Learning Guided Automated Reasoning: A Brief Survey](https://mlsanity.com/paper/2403.04017/) (2024)
- [Specify What? Enhancing Neural Specification Synthesis by Symbolic Methods](https://mlsanity.com/paper/2406.15540/) (2024)
- [Agentic Verification of Software Systems](https://mlsanity.com/paper/2511.17330/) (2025)
- [RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generation](https://mlsanity.com/paper/2505.22846/) (2025)
- [QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning](https://mlsanity.com/paper/2408.09237/) (2024)
- [A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants](https://mlsanity.com/paper/2508.18587/) (2025)
- [Event-B Agent: Towards LLM Agent for Formal Model Synthesis and Repair](https://mlsanity.com/paper/2605.17475/) (2026)
- [The Tactician's Web of Large-Scale Formal Knowledge](https://mlsanity.com/paper/2401.02950/) (2024)
- [Automating Formal Verification with Reinforcement Learning and Recursive Inference](https://mlsanity.com/paper/2605.30914/) (2026)
- [Harnessing Code Agents for Automatic Software Verification](https://mlsanity.com/paper/2607.06341/) (2026)
- [Towards Automated Functional Equation Proving: A Benchmark Dataset and A Domain-Specific In-Context Agent](https://mlsanity.com/paper/2407.14521/) (2024)
- [Learning Rules Explaining Interactive Theorem Proving Tactic Prediction](https://mlsanity.com/paper/2411.01188/) (2024)
- [Can Open-Weight LLMs Produce Kernel-Verified Coq Proofs? A Pilot Study](https://mlsanity.com/paper/2608.05420/) (2026)
- [PROVE-RT: Generating Mechanized Theorem Prover Scripts for Real-Time Systems using LLMs](https://mlsanity.com/paper/2608.12762/) (2026)

## 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.