数学家David Bessis说,他这辈子最好的定理,从没写成论文。灵感来得那天他正准备一场退休前的最后演讲,证明太顺,他临场把幻灯片最后一页改成一句非正式的备注,连定理的名字都没敢正式命名。第二好的成果更离谱——一篇旧预印本里的定理,他压根没投稿,却已经被后来的论文引用了数十次。
Bessis后来离开学界创业做机器学习,现在跳出来写文章,标题直接叫"定理经济的崩溃"。他的意思是:数学界几十年靠"发表定理、抢占归属权"分配声望和职位的游戏,正在被AI从根上动摇。
定理不值钱,语言才值钱
Bessis自己拆穿了这套游戏的虚伪之处。他说那篇被引用数十次的预印本,真正有价值的不是定理本身,而是里面两条定义——用它们搭出的一套"语言",后来被写进了一本七百页的专著里,填补了整个领域的空白。
证明定理这一步,他说反而是最容易的部分:"一旦定义对了,剩下的几乎是自动往下走。"难的是凭直觉判断"这里应该有个什么样的定理",以及为它造出合适的表达方式。
这不是他一个人的怪癖。Bill Thurston,1982年菲尔兹奖得主,早在三十年前就写过类似的话:
数学的产品是清晰与理解,而非定理本身。
这句话现在成了Bessis文章的题眼,但它本身并不新——Thurston在经典论文《论证明与进步》里就系统讲过,数学的进步不等于已发表的证明,提出问题、构建概念、培养直觉这些工作同样重要,却几乎从不被计入功劳簿。
荣誉法则:好用,但只奖励一半
这套"证明并发表"的记功法则(Bessis戏称"定理经济")之所以能撑几十年,是因为它确实有效:它减少了人情和任人唯亲,给一个处理永恒真理的学科提供了一把看似客观的尺子。
代价是,做定义、写讲义、帮别人理解已有结果的人,天然吃亏。G. H. Hardy在他那本著名的数学自传里写得很直白:造东西的人对讲解东西的人的鄙视,是最深、也最"正当"的鄙视。这话现在读起来刺耳,但它精确描述了这套体系奖励谁、忽视谁。
AI先动手的是哪一半
问题来了:AI, 尤其是配合Lean、Mathlib这类形式化证明库的工具,现在正在做什么?答案是——它擅长的恰恰是验证:检查一步推导有没有逻辑漏洞、在现有证明库里搜可用的引理、帮着修补证明中的小缺口。这一块社区反应是乐观但审慎:认可它省时间,但也警惕"跑分式进步"和看着像证明、实则是幻觉的输出。
它不擅长的,恰恰是Bessis自己引以为豪的那一半:凭直觉判断"这里该有个什么概念",然后把它造出来、写成能让别人接着用的语言。
- 结论.AI先自动化的是最容易计件的那一环,恰恰不是Bessis自己认为最难、最值钱的那一环。
- 风险.如果学界把"AI辅助证出更多定理"误当成真进步,评价体系可能奖励错方向。
文章断在了它该说的地方
有意思的是,Bessis这篇文章从头到尾都在讲自己的往事和Thurston的旧话,真正该展开的部分——AI具体是怎么把定理经济逼向崩溃的——他还没写到就停笔了。这不是我故意留白,是他原文本身就在触到靶心之前戛然而止。
这个"缺口"本身就是个信号:连提出这个论断的人,自己都还没把论证补完。数学界对AI的态度也一样悬着——Lean社区认它有用,但没人敢说验证成本降下来之后,归属和评价该怎么重新分配。
如果定理经济真的要塌,塌的会是那把用来数定理数量的旧尺子。而Bessis自己当年放弃发表、专心造语言的选择,反倒像是提前给出了答案:下一个被记住的,大概率不是证明最多定理的人,而是造出让别人都想用的那套语言的人。