研究人员推出了 TreeThink，这是一个开源 Python 库，专为神经网络定理证明中的模块化、完全异步树搜索而设计。它将成熟的搜索方法与基于 vLLM 的推理管道以及多样化的节点评估技术相结合。
- 支持 Lean~4、Rocq、Isabelle/HOL 和自然语言推理。
- 直接连接到每种语言的 REPL 服务器，以实现实时验证和证明状态提取。
- 在 miniF2F 和 MATH500 基准测试中，通过异步执行实现了高达 6.3 倍的墙钟时间加速。
该库支持跨语言形式化证明搜索和自然语言推理支持，源代码以 MIT 许可证发布。