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.