TreeThink: modular async tree search library for LLM theorem proving

Researchers introduce TreeThink, an open-source Python library designed for modular, fully asynchronous tree search in neural theorem proving. It integrates established search methods with vLLM-based inference pipelines and diverse node evaluation techniques.

• Supports Lean~4, Rocq, Isabelle/HOL, and natural language reasoning.
• Connects directly to each language's REPL server for real-time verification and proof state extraction.
• Demonstrates up to 6.3x wall-clock speedup from asynchronous execution on miniF2F and MATH500 benchmarks.

The library enables cross-language formal proof search and natural language reasoning support, with source code released under the MIT license.