Tactician is a tactic learner and prover for the Coq Proof Assistant. The system will help users make tactical proof decisions while they retain control over the general proof strategy. To this end, Tactician will learn from previously written tactic scripts, and either gives the user suggestions about the next tactic to be executed or altogether takes over the burden of proof synthesis. Tactician’s goal is to provide the user with a seamless, interactive, and intuitive experience together with strong, adaptive proof automation.
Yes, the system has first-class support for Opam, Coq’s package manager. When
you install dependencies, Tactician can automatically instrument those
developments and learn from them. When you work on your project, Tactician
will have background knowledge on all modules you Require.
On the flip side, using Tactician in your project does not mean you now have a hard
dependency on Tactician. When the system finds a proof, it presents you with
a caching witness that you can copy into your source file. As long as this witness
remains valid, you can compile your project without having the main Tactician code-base
installed. You only need 10 lines of helper tactics, which you can install
through the coq-tactician-dummy package, or simply copy them into your development.
We have not yet performed a large-scale test on students, but we believe that the system may indeed be used in this capacity. Installation is straightforward and the system functions on Linux, macOS and Windows. The automation is push-button style without needing any configuration, and when a proof cannot be found, Tactician can still suggest tactics that may be useful.
Yes! Tactician is an extensible platform that can incorporate multiple machine learning models and search procedures. If you want to contribute your ideas, you can either work on the Tactician code-base directly, or you can create a plugin for Tactician in a separate repository. We are always searching for people that want to develop new ideas, either independently or in collaboration with us. If you’d like more information, please reach out to us!
As of January 2024, several of Tactician’s models provide state-of-the-art proving performance. Evaluated over a wide range of Coq developments, the best models can prove up to 26% of theorems fully automatically. This outperforms all other provers we have made comparisons to. Performance between individual Coq packages fluctuates wildly. The best models as of 2024 are the built-in k-nearest neighbor model and Graph2Tac. The Graph2Tac paper contains an extensive analysis of the performance of several models.