# HyperTree Proof Search for Neural Theorem Proving (@ arXiv 2022)

### Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, AurÃ©lien Rodriguez, TimothÃ©e Lacroix

This paper proposes a new tree search algorithm for neural theorem proving: HyperTree Proof Search (HTPS).
It's a HyperTree because metavariables from different branches might be linked, which frequently
happens when one applies a theorem that splits the current goal into multiple related sub-goals.
They rely on the observation that, in practice, this hyper-tree is highly unbalanced, and it's thus
viable to descend simultaneously on all open sub-goals. HTPS is thus an adaptation of Monte Carlo Tree Search
for the sub-goal structure that arises in top-down interactive theorem proving.

The paper is experimentally impressive, especially for evaluating in 3 theorem proving environments
(Lean, Metamath, and their own Equations environment). I'm really curious to see if the source code
will be released. The models, however, I have less hope to use - they're quite large and they seem to require
a ton of distributed compute to run RL.