作者称 AI 辅助证明经数百次 agent 交叉验证无误，将开源 100GB 验证文件

DimitrisPapail · x · 2026-09-15

Dimitris Papail 回应质疑，称其一项数学证明是「计算机辅助证明」：数学归约部分以初等证明形式呈现，其数值前提是显式的有限不等式，可独立检验，他将把这些内容打包成约 100GB 的文件公开供人验证。

他表示，到目前为止从未见过 sol/astra 模型声称证明正确却被证伪的案例；该证明已通过三个模型合计数百次 agent 调用交叉验证。他补充说，并非否定 Lean 等形式化工具的价值，也不是反对把证明形式化，只是认为社区已逐渐接受 LLM 验证数学证明的可靠性。