Australian National University; Australian National University, Data61, CSIRO; Data61, CSIRO
Minchao Wu, Michael Norrish, Christian Walder, Amir Dezfouli
interactive theorem proving;reinforcement learning;HOL4
TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning