研究人员开发了KAPPA，一个开源软件系统，旨在自动检查统计理论论文中的证明。KAPPA利用语言模型代理（特别是由Claude Code驱动的代理）将LaTeX证明翻译成Lean 4证明助手及其Mathlib库。然后，该系统会验证每个结果，并给出四种判决之一：已验证、有条件验证、已记录问题或未完成。KAPPA被应用于几篇统计论文，成功识别出已发表的错误以及一些经人工确认的其他问题。 AI
影响 自动化对数学证明的严格验证，可能提高科学文献的可靠性。
排序理由 该集群描述了一个用于验证学术论文中数学证明的新软件工具，属于研究范畴。
在 Hugging Face Daily Papers 阅读 →
AI 生成摘要 · Google Gemini · 来自 2 个来源。 我们如何撰写摘要 →
完整方法见我们的编辑标准。
arXiv:2610.35596v1 Announce Type: cross Abstract: Papers in statistical theory rest on long proofs that few readers check line by line. We present KAPPA (Kit of Agents for Proof-checking Papers with a proof Assistant), open-source software that organizes language model agents, ru…
Papers in statistical theory rest on long proofs that few readers check line by line. We present KAPPA (Kit of Agents for Proof-checking Papers with a proof Assistant), open-source software that organizes language model agents, run by Claude Code, to translate the proofs of a LaT…