OpenProver：与Lean 4交互的智能体定理证明

本系统论文提出OpenProver：一个带集成Lean 4形式验证的、LLM驱动的自动定理证明（ATP）开源系统。OpenProver集成了受Aletheia等近期ATP智能体系统启发的规划者—工作者—验证者架构：规划者智能体维护紧凑的白板草稿与无界的中间发现仓库，把数学工作分解给并行工作者。OpenProver完全开源，经生成证明的自动形式验证提供可复现评估，并提供交互式终端界面支持人类引导的证明搜索。交互模式下，操作者可监控并引导证明搜索过程——动机来自交互式代码生成中已确立的人机协同。为展示自动形式验证所 enables 的定量消融实验潜力，我们在ProofNet上评估OpenProver并与简单基线比较。OpenProver公开于https://github.com/kripner/OpenProver。