数学家为何不信任 AI 生成的 Lean 代码

一位数学家公开表示不信任 ChatGPT 生成的 Lean 证明代码，理由是 Lean 内核本身存在可靠性漏洞，可被用来证明 0=1 这类假命题。ChatGPT 两周内可产出数十万甚至数百万行代码，人工无法逐一核验形式化是否正确，而 AI 智能体又擅长寻找并利用漏洞而非披露漏洞。他还批评 OpenAI 在未与专家合作的情况下发布大量质量欠佳的预印本。