The Mathematical Game
This work addresses the challenge of automated theorem proving for researchers in AI and formal methods, but appears incremental as it builds on an existing method without indicating major breakthroughs.
The paper tackled the problem of improving automated theorem proving by enhancing the Holophrasm neural theorem prover, which uses Monte Carlo Tree Search (MCTS) with neural networks, through the integration of other game tree search algorithms, but no concrete performance numbers or results were provided in the abstract.
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.