Paper ID: 2309.12711

The Mathematical Game

Marc Pierre, Quentin Cohen-Solal, Tristan Cazenave

Monte Carlo Tree Search can be used for automated theorem proving. Holophrasm is a neural theorem prover using MCTS combined with neural networks for the policy and the evaluation. In this paper we propose to improve the performance of the Holophrasm theorem prover using other game tree search algorithms.

Submitted: Sep 22, 2023