KAPPA: 利用 Lean 4 和语言模型智能体检查统计学论文证明

开源软件 KAPPA 利用 Claude Code 运行语言模型智能体，将 LaTeX 统计论文的证明翻译至 Lean 4 并逐一验证，对每个结果给出四种判定。 系统让独立智能体编写与审查代码，比对原文，确保证明步骤跟随之前的证据可重跑，无需语言模型即可复现判定。 盲测发现三篇已发表论文中被公开修正前的版本里的错误，验证了工具在发现证明谬误上的有效性与可靠性。