The Mathematical Game

This analysis evaluates the performance of various game tree search algorithms applied to automated theorem proving within the Metamath formal language environment. The primary objective is to enhance the Holophrasm theorem prover by replacing its native Monte Carlo Tree Search (MCTS) mechanism with alternative search strategies, including Minimax, Predictor Upper Confidence Bound applied to Trees (PUCT), Product Propagation (PP), and Proof Number Search (PNS). The study focuses on the first 200 theorems provided by the Holophrasm interface to benchmark these algorithms against the baseline.

Key findings indicate that while traditional Minimax highlights the necessity of progressive widening to manage the branching factor of proof trees, more selective algorithms like PUCT and Product Propagation demonstrate superior efficiency. Product Propagation, in particular, proves effective under strict time constraints. The research concludes that combining Product Propagation with a modified PUCT bandit function yields the most robust results, successfully breaking the 141-theorem performance ceiling observed across other methods. Specifically, this hybrid approach achieved 144 solved theorems under higher computational limits.

The methodology relies on comparative performance testing, measuring the number of theorems solved against varying parameters such as maximum passes and time limits. The study underscores that while neural networks provide essential guidance for node evaluation and proposition selection, the underlying search algorithm remains a critical determinant of success. The findings suggest that hybridizing search strategies offers a more scalable path for neural theorem proving, with future research intended to validate these improvements across the full Metamath dataset.