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.
Tactician is a tool for refactoring tactic proof scripts for the HOL Light theorem prover. Its core operations are packaging up a series of tactic steps into a compact proof with tactical connectives, and the reverse operation of unravelling compact proofs into interactive steps. This can be useful for novices learning from legacy proof scripts, as well as for experienced users maintaining their proofs. In this paper, we give an overview of Tactician's core capabilities and provide insight into how it is implemented.