发表机构
Charles University, Faculty of Mathematics and Physics（查尔斯大学数学与物理系）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
介绍用于大语言模型驱动的自动化定理证明的开源系统OpenProver，它集成特定架构，完全开源，能自动验证证明，提供交互式界面，通过在ProofNet上评估展示自动验证在定量消融实验中的潜力。
AI 中文摘要
在本系统论文中，我们展示了OpenProver，这是一个用于由大语言模型驱动的自动化定理证明（ATP）并集成了Lean 4形式验证的开源系统。OpenProver集成了受近期ATP智能系统（如Aletheia）启发的规划器-工作器-验证器架构。规划器代理维护一个紧凑的白板便签本和一个无界的中间结果存储库，并将数学工作分解给并行的工作器。OpenProver完全开源，通过对生成证明的自动形式验证提供可重复评估，并提供用于人工引导证明搜索的交互式终端界面。在交互式模式下，受交互式代码生成中已确立的人机协同作用的启发，OpenProver允许人工操作员监控和引导证明搜索过程。为展示自动形式验证实现定量消融实验（quantitative ablation experiments）的潜力，我们在ProofNet上评估OpenProver并将其与一个简单基线进行比较。OpenProver可通过此https URL公开获取。
英文摘要
In this system paper, we present OpenProver, an open-source system for LLM-driven automated theorem proving (ATP) with integrated Lean 4 formal verification. OpenProver integrates a Planner-Worker-Verifier architecture inspired by recent ATP agentic systems such as Aletheia. A Planner agent maintains a compact Whiteboard scratchpad and an unbounded Repository of intermediate findings, and decomposes mathematical work into parallel Workers. OpenProver is fully open-source, offers reproducible evaluation through automatic formal verification of generated proofs, and provides an interactive terminal interface for human-guided proof search. In interactive mode, OpenProver allows the human operator to monitor and steer the proof search process, motivated by the established human-AI synergy in interactive code generation. To showcase the potential for quantitative ablation experiments enabled by automatic formal verification, we evaluate OpenProver on ProofNet and compare it with a simple baseline. OpenProver is publicly available at https://github.com/kripner/OpenProver.
Comments7 pages, 2 figures. Accepted at the 19th Conference on Intelligent Computer Mathematics (CICM 2026)
