开源AI助研系统，用Lean 4自动证明数学定理并支持人机协作。
OpenProver: Agentic and Interactive Theorem Proving with Lean 4
- 采用规划-执行-验证架构，分解任务并并行求解。
- 在ProofNet上表现优于基线，可自动生成可验证的正式证明。
- 支持交互式界面，适合数学研究与形式化验证学习者。
本文介绍OpenProver，一个基于Lean 4的开源大模型驱动自动化定理证明系统。该系统采用受Aletheia启发的规划-执行-验证架构：规划器维护一个简洁的白板和无限存储中间成果的仓库，并将数学任务分解为并行执行的工作者。OpenProver完全开源，通过自动形式化验证实现可复现评估，并提供交互式终端界面，支持人类干预与引导证明过程。其设计灵感来自人机协同编程中的成功经验。为展示自动形式化验证带来的量化消融实验潜力，我们在ProofNet数据集上对OpenProver进行了评估，并与简单基线方法进行对比。系统代码已公开于https://github.com/kripner/OpenProver。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。