77岁的老爷子不躲了：丘成桐组队1000个数学家，要给AI补上"不会证明"的短板

赛博复古像素风 | 互联网老炮遛弯记 | 凹凸圈工作室出品

这礼拜AI圈的新闻，十有八九是"又融了多少钱""又出了什么新模型"。今天我挑一条不一样的——一条77岁老爷子组队的消息。

先把事实摆上，全部对着京报网、新京报这些多源报道核过：

10月11日，清华大学成立「丘成桐数学与人工智能实验室联盟」。牵头人丘成桐，联合8家机构：清华求真书院、丘成桐数学科学中心、北京雁栖湖应用数学研究院、中科院晨兴数学中心、上海数学与交叉学科研究院、东南大学丘成桐中心、河套数学与交叉学科研究院、香港中文大学致真交叉数学科学院。团队规模超1000名科学家。

成立仪式上，老爷子说了句提气的话："在浪潮中冲浪，而不是躲起来。"

一、老爷子为什么偏偏这时候出手

要理解这事，得先看AI圈刚发生的一幕。

就在几天前，OpenAI在GitHub上一口气开源了722篇AI写的数学手稿（整理成372个结果族）。什么概念？这堆手稿是拿约4000道公开研究问题喂出来的——平均每出一个成果，要烧掉3小时的深度思考算力（OpenAI README原文口径）。头条标题一个比一个炸：什么"AI逼近菲尔兹级问题"之类的说法满天飞。

但我把OpenAI自己的README翻出来看了，人家写得明明白白：这批成果并非全部有Lean机器验证——只是一部分主结果做了形式化验证，其余的只是论文稿；而且全部未经同行评审。OpenAI甚至自己承认："有些未形式化的结果可能有问题。"

看出来了吗？AI搞数学，正处在一个"能交作业，但还没人批改"的阶段。

丘成桐出手的位置，就在这道裂缝上。数学圈公认：AI现在解题本事不小，但"证明"这门手艺还没过关——它能猜出答案，却给不出严密到每一步都经得起推敲的推理链。而数学的地基，恰恰是证明。联盟专攻的"AI推理短板"，打的就是这一拳。

老爷子在仪式上那句"不躲"，其实是有潜台词的。躲是什么样？是争论"AI会不会取代数学家"，是站队"AI搞的不算真数学"。这两种都是躲。冲浪是另一种：承认浪潮已经在了，然后站上去，让它驮着你往前走。

二、这届老爷子给中年人上了一课

我为什么专门挑这条写？因为这事的滋味，不在科技，在人。

你想想这位的履历：1982年菲尔兹奖得主——华人里的头一号，搞定过卡拉比猜想，清华求真书院是他一手办起来的。按常理，77岁功成名就，在家写字画画带学生，谁也挑不出毛病。

但他选的路是：拉起一支千人队伍，扎进一个自己未必熟悉的新领域，跟一帮比他小六十岁的AI工程师抢牌桌。

这让我想起我们这行一句老话：人永远是在有牌可打的时候最想弃牌，真到没牌那天，想打也来不及了。老爷子现在手里的牌，是数学——人类知识里最硬的那张。他没犹豫，直接押上了。

反过来看咱们普通人：多少人三十几岁就开始念叨"学不动了"？人家77岁在干嘛？不是77岁还能学会什么，是77岁还认为自己能上场。这两句话差着十万八千里。

三、真正的看点：谁能把AI从"答题机器"变成"思考机器"

这事往大了说，是两条路线的竞争。

一条是OpenAI的路线：砸算力、堆规模，让模型自己在题海里扑腾，扑腾出722篇手稿再说。快，猛，但如我们所见——批改跟不上交卷。

另一条是丘成桐们的路线：把数学的严谨性当地基，先教会AI"怎么证明"，再谈它能证明什么。慢，笨，但数学这行干了上千年，大家心里清楚：一个定理值不值钱，不看谁先喊出来，看两百年后还有没有人引用。

对我们读者，这事的实用启示就一条：甭管AI多热，判断一门手艺还值不值得练，标准没变过——它做的东西，经不经得起别人挑刺。AI写的证明要同行评审，你写的方案、做的账、教孩子的作业，同理。这山望着那山高的毛病，古今一个样。

得，今天就唠到这。老爷子77岁还在组队冲浪，我这写字的要是哪天断更，可真没脸了。

你说AI到底能不能替代数学家？还是说它顶多算个"超级草稿纸"？评论区聊聊，我挺想听反对意见的。