OpenProver: Agentic and Interactive Theorem Proving with Lean 4
OpenProver：使用Lean 4进行智能且交互式的定理证明
机构 * Charles University, Faculty of Mathematics and Physics（查尔斯大学数学与物理系）
专题命中 程序分析与验证 ：code generation(abstract)；repository(abstract)；分类 cs.AI
AI总结 介绍用于大语言模型驱动的自动化定理证明的开源系统OpenProver，它集成特定架构，完全开源，能自动验证证明，提供交互式界面，通过在ProofNet上评估展示自动验证在定量消融实验中的潜力。
Comments 7 pages, 2 figures. Accepted at the 19th Conference on Intelligent Computer Mathematics (CICM 2026)
