HyperTree Proof Search 把 AlphaZero-style online learning 带入神经定理证明，并从失败搜索中持续学习

Meta AI 等提出 HyperTree Proof Search（HTPS），一种受 AlphaZero 启发的 neural theorem-proving search algorithm，并配套 online training：模型从此前 proof search 的成败中继续学习。论文报告在 held-out Metamath theorems 上，HTPS 从 65.4% 提升到 online-training 后的 82.6%；在 Lean-based miniF2F-curriculum 上将当时 state of the art 从 31% 提高到 42%。