TacticToe records tactic-level proof information from HOL4, learns which proof actions are promising in a new goal state, and searches over complete tactic sequences directly in higher-order logic rather than translating every problem to first-order logic.
Thibault Gauthier, Cezary Kaliszyk and Josef Urban introduced TacticToe in the LPAR-21 proceedings published on 4 May 2017. The system learned tactic and premise choices from previous HOL4 proofs and used modified A* search to explore tactic-level proof paths, re-proving 39% of 7,902 HOL4 theorems within five seconds in the reported evaluation. A later expanded study published in 2018 replaced the search with Monte Carlo tree search and reported stronger results on the HOL4 standard library.
TacticToe records tactic-level proof information from HOL4, learns which proof actions are promising in a new goal state, and searches over complete tactic sequences directly in higher-order logic rather than translating every problem to first-order logic. The 2017 system used a modified A*-style search with tactic prediction and small-scale hammering; the later expanded implementation developed the search machinery further and remains available in the HOL4 repository.
The work demonstrated that machine learning could guide proof-assistant-native tactic search rather than only premise filtering for an external automated prover. This combination of learned action prediction, search and kernel-checked proof construction became a recurring design pattern in later neural interactive theorem proving.
Significance rationale: TacticToe was an important early proof-assistant-native learning system that used recorded human HOL4 proofs to guide tactic-level proof search directly inside a mature interactive theorem prover. The initial LPAR-21 publication combined learned tactic and premise selection with modified A* search; an expanded 2018 study developed the same system further with Monte Carlo tree search. Together the work established a line later continued by reinforcement-learning systems such as TacticZero.
—
The LPAR-21 proceedings establish the initial public TacticToe system, its learned tactic-level proof search and the reported HOL4 evaluation. Machine checking refers to proof scripts accepted by HOL4 and does not imply independent reproduction of the reported success rate.
The expanded 2018 research record documents the later Monte Carlo tree-search version and stronger HOL4 standard-library evaluation without changing the identity of the underlying TacticToe milestone.
The maintained public HOL4 repository contains the TacticToe implementation, recording workflow, evaluation support and usage instructions. E3 denotes inspectable artifacts rather than independent verification of every experimental claim.
Corrected the canonical event date from 2018-04-02 to 2017-05-04 after locating the LPAR-21 proceedings publication of the initial TacticToe system, and revised the record to distinguish the 2017 A*-guided version from the expanded 2018 Monte Carlo tree-search study while preserving the stable Event ID.
