Tree-search library for neural theorem proving that connects to the Lean 4 REPL, alongside Rocq and Isabelle, and is evaluated on miniF2F-lean4 with DeepSeek-Prover-V2.
Abstract
Tree search algorithms enable systematic exploration of the proof space in neural theorem proving. Existing LLM tree search libraries primarily target natural language reasoning and do not provide native integration with formal verifiers, while theorem proving systems often rely on task-specific search implementations. We introduce TreeThink, an open-source Python library for modular, fully asynchronous tree search in neural theorem proving. It integrates established tree search methods with vLLM-based inference pipelines and diverse node evaluation techniques, ranging from lightweight heuristics to neural evaluators. We support Lean 4, Rocq, and Isabelle/HOL alongside natural language. It connects directly to each language's Read-Eval-Print Loop (REPL) server for real-time verification and proof state extraction. We evaluate TreeThink on miniF2F and MATH500, demonstrating cross-language formal proof search, natural language reasoning support, and up to 8.0$\times$ wall-clock speedup from asynchronous execution. Source code is released under the MIT license at https://github.com/GGLAB-KU/treethink , and the library is accessible as a downloadable package at https://pypi.org/project/treethink/ .
Problem
Existing LLM tree-search libraries target natural-language reasoning and lack integration with formal verifiers. Theorem-proving systems instead tend to use task-specific search code that is hard to reuse.
Approach
TreeThink is an open-source, fully asynchronous Python library. It modularizes search algorithms (best-first, beam, MCTS, rollout-free MCTS), vLLM-based policies, and eight node evaluators, ranging from heuristics to neural judges. A unified REPL client connects to Lean 4, Rocq, and Isabelle/HOL for real-time verification and proof-state extraction, with proof caching and natural-language support.
Figure 1: NTP tree search process. 1. Select: search method selects a node using a search algorithm. 2. Expand : the policy LLM generates child nodes. 3. Evaluate : evaluator strategy scores the generated nodes. W stands for the value assigned to a node. 4. Verify : external systems verify the correctness of the proof. Main operations in individual sections are in red while batched processes are i
Results
On miniF2F, tree search raised pass rates over pass@1 in all three languages, reaching 57.4% in Lean with RF-MCTS. Asynchronous execution gave up to 6.3x wall-clock speedup in the reported experiment; the abstract claims up to 8.0x. On MATH500, RF-MCTS reached 40.0%, versus 34.8% for maj@12.
