OpenProver：基于 Lean 4 的代理式交互式定理证明系统

本文提出 OpenProver，一个开源的由大语言模型驱动的自动定理证明系统，集成了 Lean 4 形式化验证。该系统采用受 Aletheia 启发的“规划者 - 工作者 - 验证者”架构：规划者维护紧凑白板与无限中间发现仓库，并将数学任务分解为并行工作者。OpenProver 支持通过形式化验证进行可复现评估，并提供交互式终端接口以实现人机协同证明搜索。作者在 ProofNet 数据集上进行了定量消融实验，展示了其在数学推理方面的潜力。