  We propose an online training procedure for a transformer-based automated
theorem prover. Our approach leverages a new search algorithm, HyperTree Proof
Search (HTPS), inspired by the recent success of AlphaZero. Our model learns
from previous proof searches through online training, allowing it to generalize
to domains far from the training distribution. We report detailed ablations of
our pipeline's main components by studying performance on three environments of
increasing complexity. In particular, we show that with HTPS alone, a model
trained on annotated proofs manages to prove 65.4% of a held-out set of
Metamath theorems, significantly outperforming the previous state of the art of
56.5% by GPT-f. Online training on these unproved theorems increases accuracy
to 82.6%. With a similar computational budget, we improve the state of the art
on the Lean-based miniF2F-curriculum dataset from 31% to 42% proving accuracy.
