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.

翻译：蒙特卡洛树搜索可用于自动定理证明。Holophrasm是一种神经定理证明器，它将蒙特卡洛树搜索与用于策略和评估的神经网络相结合。本文提出利用其他博弈树搜索算法来提升Holophrasm定理证明器的性能。