OpenProver发布：基于LLM的交互式定理证明系统，集成Lean 4验证

近日，arXiv平台发布了一项名为OpenProver的开源系统研究，该系统专注于大语言模型驱动的自动定理证明，并集成了Lean 4形式化验证功能。OpenProver采用了受近期ATP智能体系统启发的“规划器-工作者-验证器”三层架构：规划器负责维护紧凑的白板草稿和无限容量的中间结果仓库，并将数学工作分解为并行执行的工作者任务。

该系统完全开源，通过自动形式化验证生成证明，确保评估的可复现性，并提供了交互式终端界面，允许用户在证明搜索过程中进行监控与引导。这种设计借鉴了交互式代码生成中已验证的人机协同模式，增强了系统的实用性与灵活性。

为展示自动形式化验证支持下的量化消融实验潜力，研究团队在ProofNet数据集上对OpenProver进行了评估，并与简单基线模型进行了对比。目前，OpenProver已在GitHub平台公开，供社区研究使用。