陶哲轩担忧 AI 批量生成数学证明的可靠性

菲尔兹奖得主陶哲轩联署 25 位同行发起宣言，呼吁停止与 OpenAI 合作，以抵制 AI 数学证明。 背景是 OpenAI 曾批量发布 722 篇模型生成手稿，但同期 Lean 证明器暴露出多个健全性漏洞。 核心担忧在于数学界可能失去对 AI 证明进行独立可信判断与解释的能力。