Erdős Problems 冻结评论：AI 证明洪水把人挤走了
那个成了 AI 做数学的公开记分牌的网站，把记分牌拆了。运营 erdosproblems.com 的 Thomas Bloom 周一发帖，冻结新的问题评论和证明声明，去掉每个问题的开放/已解决状态和已解决百分比计数，未来的解法不再用归功式语言，无论是人还是 AI 做的。HN 的标题是“Erdősproblems.com 倒在 AI 攻势之下”。
数字解释了原因。网站有 1,221 个问题，9,000 多条评论，近 2,000 个注册用户，每天 1 万到 2.5 万独立访客。2025 年 8 月上线评论之后，一个真实的社区长出来了。然后 AI 在不到一年里从对这些问题毫无用处变成能解掉难题，现在人们跟网站互动的主要方式变成了晒 AI 生成的证明，往往不打算解释，只是为了记录一个 Bloom 称之为越来越没意义的优先权声明。有些数学家不再碰 Erdős 问题，因为觉得拼不过 AI。
Bloom 的措辞很克制。帖子里说 AI 生成证明的仓库应该存在，免得别人浪费 token 重新生成同一个证明，而且现在已有好几个候选。Bloom 只是不想自己运营一个。原话是：没人会在屠宰场里开餐馆。网站会继续记录结果，会推高质量的讲解，包括对 AI 证明的讲解，前提是写法是人写的、AI 使用诚实披露。抄袭或谎报 AI 使用的，哪怕证明正确也拒收。
这是四天里同一种成本转移的第四个案例。Simon Willison 的硬预算上限，谷歌暂停的漏洞赏金，维基媒体的清理账单，现在是一个人的数学网站。agent 让产出一份提交近乎免费。检查它、放进上下文、承受社区效应，这些依然昂贵，而扛着这份成本的人把门关了。
对 agent 做数学的人来说，实际变化很小：把证明发邮件，等手动更新。文化变化更大。AI 数学最出名的公开基准刚刚说了一句：一个形式化证明，并不是一个问题价值的终点。
链接：erdosproblems.com/forum/thread/blog:9
← 返回所有文章
数字解释了原因。网站有 1,221 个问题，9,000 多条评论，近 2,000 个注册用户，每天 1 万到 2.5 万独立访客。2025 年 8 月上线评论之后，一个真实的社区长出来了。然后 AI 在不到一年里从对这些问题毫无用处变成能解掉难题，现在人们跟网站互动的主要方式变成了晒 AI 生成的证明，往往不打算解释，只是为了记录一个 Bloom 称之为越来越没意义的优先权声明。有些数学家不再碰 Erdős 问题，因为觉得拼不过 AI。
Bloom 的措辞很克制。帖子里说 AI 生成证明的仓库应该存在，免得别人浪费 token 重新生成同一个证明，而且现在已有好几个候选。Bloom 只是不想自己运营一个。原话是：没人会在屠宰场里开餐馆。网站会继续记录结果，会推高质量的讲解，包括对 AI 证明的讲解，前提是写法是人写的、AI 使用诚实披露。抄袭或谎报 AI 使用的，哪怕证明正确也拒收。
这是四天里同一种成本转移的第四个案例。Simon Willison 的硬预算上限，谷歌暂停的漏洞赏金，维基媒体的清理账单，现在是一个人的数学网站。agent 让产出一份提交近乎免费。检查它、放进上下文、承受社区效应，这些依然昂贵，而扛着这份成本的人把门关了。
对 agent 做数学的人来说，实际变化很小：把证明发邮件，等手动更新。文化变化更大。AI 数学最出名的公开基准刚刚说了一句：一个形式化证明，并不是一个问题价值的终点。
链接：erdosproblems.com/forum/thread/blog:9
评论