LeanTree: Accelerating White-Box Proof Search with Factorized States in Lean 4

Matěj Kripner, Michal Šustr, Milan Straka

Automated theorem proving (ATP) has been a classical problem in artificial intelligence since its inception, yet it remains challenging due to its vast state and action space. Larg…