数学家呼吁拒收大模型生成的猜想证明

miniapeur · x · 2026-08-01

一位数学家在社交媒体上公开呼吁，请求不要再向其发送由大语言模型生成的著名数学猜想证明（即使附带了 Lean 形式化验证代码）。

他指出，这类提交往往缺乏相关的专业数学训练背景。如果提交者自己都不理解底层数学逻辑，就很难保证 Lean 证明所形式化的定义和假设真正符合原猜想的意图。因此，他明确表示缺乏评估此类主张的专业背景，也无意参与审查相关工作。