一道题都没解网站先关了评论区十月六日埃尔德什问题网站宣布冻结问题评论与证明声明。这个决定没有涉及任何数学内容却比一次证明更有冲击力。它把一个被长期回避的问题摆上台面当机器能批量产出正确证明公开知识库该怎么活。网站的名字叫 erdosproblems.com由数学家托马斯·布鲁姆在二零二三年五月上线。它的初衷是整理保罗·埃尔德什留下的猜想让人类读者方便查阅和思考。上线时它只有两百多道题规模像一本个人笔记。两年后它收录一千二百二十一道题评论区累计九千多条。注册用户接近两千人每天访问量在一万到两万五千之间。这个体量已经超过绝大多数专业讨论区。转折点出现在二零二五年八月网站加上了评论功能。最初几个月非常热闹人们分享思路、纠正错误、补充引用。很多论文和合作从这些评论里长出来。但这种热度没有持续。一部分衰减是自然的好想法总会被说完。更大的一部分来自人工智能的冲击。如今最主流的公开互动是贴一份人工智能生成的证明然后不做任何解释。布鲁姆的判断很直白这些人是在抢占一个越来越没有意义的优先权。他不想经营一个专门做这件事的网站。于是有了这次冻结。冻结令的四条改动公告里的改动一共四条每一条都在切断一种激励。第一条是冻结问题评论与证明声明。综合讨论区和博客文章仍然开放评论。问题评论和证明声明可能在未来恢复但时间未定。在此期间更新建议改为通过邮件提交由他手动整理。第二条是隐藏所有题目的状态。网站不再显示未解、已解这类标签。所有题目用同一种中性颜色展示。已解数量和解出百分比也不再出现。第三条是停止使用归属语言。网站仍会记录相关结果和定理。但不再用某人证明了某结论这类措辞。布鲁姆给了一个示例句式。过去写某人证明了某不等式现在写已知某不等式并附上解释的链接。第四条是把重心转向高质量解释文章。网站鼓励人们投稿自己对证明的讲解。不论证明是旧的还是新的是人的还是机器的。只有被判定为高质量的才会被收录。他还在探索线上研讨班等新形式。一千二百二十一道题与九千条评论的账本理解这次改动需要看一组数字。网站目前收录一千二百二十一道题。评论总数超过九千条。注册用户接近两千。日独立访客在一万到两万五千之间。一名用户在公告下给出了更细的统计。全站当时共有二百九十一条证明声明。其中一百五十五条没有任何评论。十四条只有提交者自己的评论。一百一十二条至少收到过一条他人评论。有六十一道题挂着多份证明声明。一百五十五条零评论的声明里七十七条提交于九月之前。十月一日之后的十四条声明里七条没有评论。这组数字说明大多数证明声明从未进入讨论。它们只是被贴上去然后停在那里。布鲁姆说他收到的评论里绝大多数都是在宣告人工智能生成的证明。让审核只放行真实讨论等于拒掉几乎所有提交。这种审核策略不可持续。所以他没有选择加审核而是选择关门。反对者的三条反驳公告发布当天评论区就出现了集中的反对意见。第一条反驳针对隐藏状态。反对者认为唯一效果是让数学进展变得更不可见。它只增加读者自己判断历史的工作量。而且对劝退追名逐利者几乎没有作用。因为很多评论本来就发生在已解的题目上。状态变更本身也一直很少发生。第二条反驳针对冻结评论。有人担心提交会转向更冷清的仓库。那里的证明不会被看见想法也不会被引用。结果只是让进展的流动变慢。一位用户提到自己的两段合作直接源于站内评论。这类合作在冻结之后几乎不可能再发生。第三条反驳指向一个内在矛盾。如果抢先贴出的证明不值得承认那它就不该可怕到需要封禁。支持者则给出了另一种解释。他们认为把解释的负担交还给提交者本身就是一种筛选。也有人指出证明声明区其实早已被单独隔开。真正的问题不在分区而在没人愿意读那些长文档。一位用户承认自己曾经也是被批评的那种追逐者。优先权为什么会贬值要理解这场冲突得先理解证明声明在争什么。传统上数学里的优先权是一种稀缺资源。谁先证明谁获得署名、引用和职业回报。这个激励驱动了大量公开讨论。但当生成一份正确证明的成本降到接近于零优先权的价格就崩了。谁先提交不再取决于谁想得更深而取决于谁的算力先排上队。布鲁姆把这称为一种游戏化的追名逐利。他还指出一个更微妙的后果。这些声明给人一种错觉好像一道题的价值在证明出现时就结束了。他认为这不对无论证明来自人还是机器。一道题的答案会产生更多问题而不是终结讨论。这也解释了为什么他选择隐藏状态。已解与未解这个二分本身就是一种误导。很多题目的判断带有主观性什么算解决并不总是清楚。只浏览未解题的人会错过大量有意思的数学。与其让人盯着状态刷不如让人按主题去找问题。这正是他把重心转向解释文章的原因。解释是少数无法被低成本批量生产的东西。形式化验证站在哪一边公告里有一条容易被忽略的技术细节。布鲁姆说他会优先链接经过验证的 Lean 形式化。Lean 是一种交互式定理证明器能把证明写成机器可检验的代码。形式化让证明的正确性不再依赖读者的信任。他还指定了一个登记处名叫 Palomar。把形式化登记到 Palomar其他人可以看到它能编译通过。也能看到形式化的陈述是否与题目原意一致。这一条把人工智能证明放到了一个可验证的位置上。他明确表示会尽快链接正确的 Lean 形式化。而对于解释不清、又没有形式化支撑的证明他不太可能更新网站。这个区分很关键。形式化解决的是正确性不解决理解。一份能编译的证明仍然可能没人看得懂。所以他把解释和形式化并列而不是二选一。这也回应了另一类批评。有用户担心冻结会挤压学术圈之外的人。布鲁姆的回答是他会链接来自任何来源的正确形式化和高质量写作。但他要求如实披露人工智能的使用。有抄袭或隐瞒证据的提交即使正确也可能被拒。一个最小可用的证明声明仓库如果这类仓库注定要存在它至少需要三个基本能力。第一是按规范化后的陈述去重。第二是记录形式化验证的状态。第三是保留人类可读的解释链接。下面这段 Python 用标准库实现了这三件事。它读取一份 JSONL 提交日志按陈述指纹去重并输出统计。import hashlib, json, re, sys, unicodedata SPACES re.compile(r\s) GREEK {\u03b1: alpha, \u03b2: beta, \u03b3: gamma, \u2264: , \u2265: , \u2260: !} def normalize(statement): s unicodedata.normalize(NFKC, statement) for k, v in GREEK.items(): s s.replace(k, v) s SPACES.sub( , s).strip().lower() return s def fingerprint(statement): raw normalize(statement).encode(utf-8) return hashlib.sha256(raw).hexdigest()[:16] def load(path): with open(path, r, encodingutf-8) as f: for line in f: line line.strip() if line: yield json.loads(line) def dedupe(records): best {} for rec in records: key fingerprint(rec[statement]) cur best.get(key) keep rec.get(formalized) and not (cur or {}).get(formalized) if cur is None or keep: best[key] rec return list(best.values()) def report(records): total len(records) formal sum(1 for r in records if r.get(formalized)) with_exp sum(1 for r in records if r.get(exposition)) silent 1 - with_exp / total if total else 0.0 return { statements: total, formalized: formal, with_exposition: with_exp, silent_ratio: round(silent, 3), } if __name__ __main__: print(json.dumps(report(dedupe(load(sys.argv[1]))), indent2))这段脚本不做任何网络请求也不依赖第三方库。它的核心是 normalize 函数把数学陈述压成稳定的指纹。去重的粒度放在陈述层而不是证明层。因为同一个陈述可以有无数份不同的机器证明。仓库真正需要收敛的是陈述不是证明文本。formalized 字段用来标记是否登记过形式化验证。exposition 字段存的是人类可读解释的链接。统计输出里最值得看的是无解释声明的占比。这个比例越高仓库就越接近一个只进不出的黑洞。同类站点正在往哪里走布鲁姆说这类仓库应该存在但他不想亲自经营。他列出的候选路径实际上已经在被不同平台试探。下表把几种典型形态放在一起对比。平台准入方式稀缺资源对机器产出的态度arXiv事后审核与分类可信度接受但设门槛Zenodo完全开放注意力无条件接收Palomar形式化登记机器可检验性只收可编译证明erdosproblems.com冻结声明与评论人的参与暂停接收arXiv 走的是事后审核路线。它一度被大量低质量投稿冲击最终靠分类和门槛维持秩序。Zenodo 走的是完全开放路线任何文件都能拿到永久标识。代价是发现性极差除非被搜索工具命中。Palomar 只做形式化登记范围窄但判据硬。erdosproblems.com 原本是讨论区现在主动收缩成档案。这四种形态的分工其实对应四种不同的稀缺资源。arXiv 稀缺的是可信度Zenodo 稀缺的是注意力。Palomar 稀缺的是机器可检验性而讨论区稀缺的是人。当机器的产出能力远超人类的阅读能力最稀缺的一定是人。这也解释了为什么冻结评论是一种防御而不是一次升级。网站没有变得更强大只是把闸门关小了一点。冻结之后读者还剩什么冻结之后网站并没有变成一座空房子。已有的九千多条评论会作为档案保留下来。题目仍然可以按主题和标签浏览。综合讨论区和博客文章的评论区依然开放。更新建议改走邮件由布鲁姆手动整理。解释性文章的投稿通道也被明确鼓励。失去的是两样东西。一是新的问题评论二是可见的题目状态。对偶尔来查资料的读者影响其实有限。他们本来也不会去读几十份未经整理的长文档。真正受影响的是常驻讨论的那批人。他们失去了一个低成本交换想法的场所。一位用户说自己每天早上习惯性刷新证明声明。现在这个动作没有了目标。另一件容易被忽略的事是标签系统的保留。布鲁姆确认标签继续可用并欢迎反馈问题。这说明网站并没有放弃组织只是放弃了计分。三条判断标准如果把这件事抽象一层可以得到三条判断标准。第一条是验证成本。当一个领域能低成本验证产出时产出一定会泛滥。数学恰好具备这个性质证明可以被机器检查。第二条是激励可见性。只要排名、状态和署名可见就会有人为它们优化。把指标藏起来优化的动机也会随之减弱。第三条是人类阅读容量。这条几乎不会增长它是所有知识库的真正瓶颈。三条标准放在一起结论就很清楚。当验证成本下降、激励高度可见、阅读容量不变时知识库必然失衡。治理手段无非是动其中一条。提高验证成本会牺牲开放性。隐藏激励会牺牲进展的可见度。增加阅读容量短期几乎做不到。布鲁姆选择了前两条的组合。他没有解决矛盾只是把矛盾移出了自己的院子。这未必是最优解但至少是一次诚实的权衡。而这份诚实正是这场讨论最值得留下的东西。这不只是数学的问题把视线拉远这件事的模式在其他领域已经反复出现。任何公开的、结构化的、易于批量作答的知识库都会遇到同样的压力。问答社区、代码仓库、文献索引一个接一个地面对过。它们的应对方式大致只有三种。第一种是提高门槛比如要求形式化或复现。第二种是改变激励比如取消可见的排名与状态。第三种是主动收缩只保留最窄的核心功能。布鲁姆这次同时用了后两种。他的选择之所以值得讨论是因为它放弃了增长。大多数平台面对同样的压力会选择扩容量而不是关闸门。他给出的理由带有很强的个人色彩。他引用了一篇关于人类数学家是否还有必要的文章。文章提出的准则是人类应该帮助人类繁荣。他把这条准则改写成网站版本。网站应该帮助埃尔德什问题的爱好者群体繁荣。繁荣的定义不是产出更多证明而是保持有人愿意思考和理解。这个定义直接决定了四条改动的方向。公告结尾写了一段很不一样的文字。他描述埃尔德什是一个极其爱社交的人。他一生在数学家之间旅行敲门时说我的大脑是开放的。他不是那种把自己关起来多年攻一道题的人。布鲁姆借此表达了对一种未来的担忧。那种未来里人只负责提出问题然后看着屏幕等答案。每份证明被丢进仓库只有机器会读它。他认为埃尔德什会觉得这种未来很糟。所以公告的最后一句是一句请求。不要放弃作为人类活动的数学。找一个对你真正有意义的问题找到同样感兴趣的人然后聊它。