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.
For more information, see Tactician's website and the main coq-tactician repository
