LeanTree: Accelerating White-Box Proof Search with Factorized States in Lean 4
Matěj Kripner, Michal Šustr, Milan Straka
cs.LG
Jul 19, 2025 · v1
TL;DR
LeanTree is a Lean 4 tool factorizing proof states into independent branches, plus a dataset for white-box proof search.
Abstract
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. Large language models (LLMs) have recently emerged as a promising heuristic for ATP, but they lack correctness guarantees and thus require interaction with a proof verifier. Such interactions typically follow one of two approaches: black-box interaction, which does not utilize intermediate proof states, or white-box approaches, which allow for incremental proof construction and examination of intermediate states. While black-box approaches have directly benefited from recent LLM advances, white-box methods have comparatively lagged behind. In this paper, we address this gap by introducing LeanTree, which consists of (i) a tool built in the Lean 4 language that factorizes complex proof states into simpler, independent branches, and (ii) a dataset of these factorized intermediate states. Our white-box tooling offers several advantages over black-box approaches: it simplifies evaluation, reduces necessary context, generates richer training data, enables parallel search across multiple states, supports efficient reuse of states, and provides feedback in case of errors. Our preliminary results hint that white-box approaches outperform black-box alternatives in some settings.
Problem
White-box automated theorem proving methods in Lean 4, which leverage intermediate proof states for incremental construction, have lagged behind black-box approaches that directly benefited from recent LLM advances.
Approach
LeanTree introduces a tool built in Lean 4 that factorizes complex proof states into simpler, independent branches (an AND-OR proof tree), along with a dataset of these factorized intermediate states. The factorization simplifies evaluation, reduces necessary context, generates richer training data, enables parallel search across multiple states, supports efficient state reuse, and provides error feedback. They train Llemma-7B on the extracted dataset.
Results
Preliminary results on MiniF2F using linear rollouts with Llemma-7B indicate that white-box approaches outperform black-box alternatives in some settings. The factorization enables advantages like transposition detection (analogous to board games) and parallel proof search across independent subgoals.
