Herman Geuvers

Tactic Learning and Proving for the Coq Proof Assistant

2020 · EPiC series in computing

We present a system that utilizes machine learning for tactic proof search in the Coq Proof Assistant. In a similar vein as the TacticToe project for HOL4, our system predicts appropriate tactics and finds proofs …