在这篇系统论文中，我们介绍了 OpenProver，这是一个开源的、基于 LLM 驱动的自动定理证明（ATP）系统，集成了 Lean 4 形式验证。
OpenProver 采用了 Planner-Worker-Verifier 架构，灵感来源于最近的 ATP 代理系统，如 Aletheia。
Planner 代理维护一个紧凑的白板草稿和一个无限的中间发现库，并将数学工作分解为并行的 Worker。
OpenProver 完全开源，通过自动形式验证生成的证明，提供可重复的评估，并为人类引导的证明搜索提供交互式终端接口。
在交互模式下，OpenProver 允许人类操作员监控和引导证明搜索过程，这得益于人机协同在交互式代码生成中的应用。
为了展示自动形式验证所带来的定量消融实验潜力，我们在 ProofNet 上评估了 OpenProver，并与一个简单的基线进行了比较。
OpenProver 可在 GitHub 上公开获取。
博主点评： OpenProver 的设计展示了 LLM 在定理证明中的应用潜力，通过集成 Lean 4 的形式验证，提供了一个强大的工具来增强人机协作。这种新颖的架构为定理证明领域带来了新的思路，值得进一步探索和发展。