首页财产ai正文 AI「生肉证实」堆爆GitHub！陶哲轩重磅发声：只会解题没用了 陶哲轩提出数学正从证实稀缺进入多余时代，因AI加快证实天生，致消化环节跟不上，他以多渠道亮相，猜测学术评价系统将重构。 2026-04-30 14:09 ·微信公家号：新智元新智元 AI投资人解读· AI 年夜幅加快数学证实天生，验证环节有东西兜底，但消化环节跟不上，致使年夜量证实聚集无人理解。如 Erdős 问题 #1196 是独一跑通“天生、验证、消化”三阶段的案例。数学家焦点竞争力正从证实天生转向问题选择、流程设计和成果消化。· 行业竞争加重，学术评价系统或者重构AI 东西利用不妥可能孕育发生年夜量无价值证实。总结：AI 给数学范畴带来厘革，转变数学家事情方式与学术评价逻辑，各强证实型学科也将受影响。虽证实数目增长，但理解证实的价值愈发凸显，投资需存眷相干范畴人材能力与学术评价系统变化。内容由AI天生，仅供参考

近来，陶哲轩于 Mastodon 抛出一记重磅判定——

数学正于从证实稀缺时代，进入证实多余时代（from an era of proof scarcity to an era of proof abundance）！

于AI对于Erdős问题的孝敬Github页面上，20多份 AI 提交的全数或者部门解，正堆于「pending assessment」（待评估）那一栏。

而于此以前，这个分类常年只有1-2份。

一晚上之间，AI 正于以使人梗塞的速率疯狂输出数学证实。

问题是——没人来患上和看。

问题求解「三件套」

天生、验证、消化

陶哲轩把此次的思索成立于一个简便的框架上。

他说，数学问题求解从来不是一件事，而是三件事：

Proof generation（证实天生）：把一个料想从「未解决」推到「有解」。

Proof verification（证实验证）：确认这个解是对于的，逻辑没有缝隙。

Proof digestion（证实消化）：把证实读懂、讲透、提炼出要领论，让整个范畴受益。

于已往的几百年里，三件事基本由统一拨人完成——你证了一个定理，你天然理解它，你写论文注释它。

这三个环节之间不存于「瓶颈差」。

但 AI 来了以后，环境变了。

天生环节被 LLM 年夜幅加快，验证环节有 Lean、Coq 等情势化东西兜底，惟独消化环节——阿谁需要人类年夜脑去理解「这个证实到底象征着甚么」的环节——彻底跟不上。

陶哲轩用了一个切确的工程术语来形容这类错位：impedance mismatch（阻抗掉配）。

三个环节的速率不匹配了：证实像洪水同样涌来，但理解的堤坝还有是手工砌的。

他说，想象两种社会。

食品稀缺的社会，最受尊重的人是猎手及农民——是那些「bring home the bacon」（把食品带回家）的人。

你猎回一头鹿，无论肉质怎样，整个部落城市感谢你，会有人自动帮你洗濯、烹调、分配。险些任何没有毒的食品孝敬都受接待。

食品多余的社会则彻底差别。

想象一个 pot-luck 派对于（每一人带一道菜的会餐）。假如一个生疏人闯进来，扔下一块来路不明的生肉，让各人本身行止理——没有人会兴奋。

甚至超市买来的预包装食物，也只是委曲算数。

真正受接待的，是社区里受信托的成员精心烹制的家常菜——不仅由于好吃，更由于缭绕这道菜的对于话自己就是社交的一部门，也是造就下一代厨师的时机。

回到数学——AI 跑出来的「生肉证实」（raw proof），就是那块被生疏人扔于派对于上的神秘肉。

它多是准确的。它可能经由过程了情势化验证。

但没有人洗濯过它、烹调过它、也没有人能告诉你它到底好欠好吃。

陶哲轩直言：这类「孝敬」不仅没有推进问题的现实进展（do not measurably advance the progress），反而可能孕育发生一个「负面效果」——它杀死了人们继承研究这个问题的兴致。

问题被宣告「已经解决」了，但没人懂这个解。

比如一道菜被端上桌，但没人敢动筷子。

在是这道菜——连同缭绕它可能孕育发生的所有对于话及灵感——就如许凉了。

Erdős #1196，唯 一跑通「三件套」的案例

理论都需要一个切片去查验。

陶哲轩重复提到的阿谁切片，就是 Erdős 问题#1196。

这是一个关在「primitive sets」（来源根基集）的料想：于一个整数调集中，假如没有任何元素整除了另外一个元素，那末对于所有元素 a 按 1/(a·log a) 乞降，当调集元素趋在无限年夜时，这个及是否趋近在1？

1968年，Erdős、Sárközy 及 Szemerédi 提出了这个料想。

今后快要60年，数学家们不停迫近——斯坦福数学家 Jared Lichtman 花了数年证实了一个相干的上界（约1.399），但终极的渐近料想始终悬而未决。

2026年4月的某个周一下战书，23岁的 Liam Price 把这道题丢进了 GPT-5.4 Pro。

Price 没有数学博士学位，没有多年的专业练习。他用的是一个20美元/月的 ChatGPT Pro 定阅——任何人都能用的东西。

80分钟。

模子走通了一条数学界轻忽了近90年的路径：用von Mangoldt 函数（一种经典的解析数论权重函数）联合马尔可夫历程理论，组织出了一个全新的证实框架。

这个技能组合已经经存于了几十年，但从未有人想到把它用于来源根基集问题上。

证实出来了。

但若故事到这里就竣事，它只不外又是一块「神秘肉」。

要害于在接下来发生的事：陶哲轩亲自下场。

他于24小时内验证了证实的焦点思绪，随后将其扩大、重组、打磨，终极展现出这个证实暗地里隐蔽着一条更深层的接洽——整数剖解学（integeranatomy）与马尔可夫历程理论之间一条此前未被描写的全新桥梁。

这就是证实消化（proof digestion）。

不只是「对于不合错误」的问题，而是「它象征着甚么」的问题。

陶哲轩称#1196是今朝唯 逐一个三阶段——天生、验证、消化——都基本跑通的案例。

也正因云云，他重复夸大一个原则：抱负状况是统一拨人完玉成部三件事。

而实际中，愈来愈多的人于用 AI 天生证实后，没时间去验证及消化，就直接提交了。

这恰是 Erdős 问题近20多份待评估方案聚集的直接缘故原由。

三处亮相，统一判定

陶哲轩不是于一个处所随口说说。

他于险些统一期间，经由过程三个差别渠道发出了统一个旌旗灯号。

4月27日，Mastodon 长帖：正式提出「证实稀缺→证实多余」的范式判定。

4月27日，Nature 访谈（The job description is changing）：他对于记者 Davide Castelvecchi 说，数学家的「岗亭描写」正于转变。一个拒绝碰 AI 东西、只想用传统方式做证实的研究生，将来可能会发明本身的时机愈来愈少。

能于传统数学功底之上纯熟应用新东西的人，才会真正繁荣。

3月29日，博客官文《Mathematical methods and human thought in the age of AI》：他及 Klowden 花了跨越一年写成这篇论文，试图逾越面前的技能细节，直面更底子的哲学问题——数学证实的素质是甚么？论文的目的是甚么？咱们这个职业存于的意义是甚么？

他于博客中写道：假如咱们本身不回覆这些问题，它们就会被科技公司或者经济激励机制替咱们回覆。

三处亮相，统一个内核：数学家的焦点竞争力正于迁徙——从「谁师长教师成证实」，转向「谁能选对于问题、设计事情流、验证并消化成果」。

稀缺的再也不是谜底，而是理解。

更年夜的震荡：学术评价系统要重写

假如只是数学家的事情方式变了，那还有只是一个学科内部的事。

但陶哲轩看到的远不止此。

当证实的成本被 AI 压到靠近在零，当证实验证被 Lean/Coq 等情势化引擎年夜幅主动化——证实消化这个环节的价值就会被重估。

已往，消化证实是「免费的」。

你证了一个定理，你天然会理解它，会于论文里注释它。这个劳动从未被零丁计价。

但当证实的出产者（AI）及理解者（人类）被拆开以后，消化就从隐性劳动酿成了显性稀缺资源。

这象征着整个学术声望的分配逻辑要变。

Citation 系统、论文评审尺度、奖项评比法则、甚至雇用及提升的依据——所有这些缭绕「谁先证了甚么」成立起来的激励布局，都将面对重构。

陶哲轩猜测：就像现代社会再也不把生食原料看成一顿饭同样，数学研究文化将再也不把「未消化的裸证实」（raw, undigested proofs）视为对于一个问题的解决方案。

将来的评判尺度，将聚焦在一个孝敬毕竟于多年夜水平上富厚了整个范畴，而非仅仅「解决」了问题自己。

并且这不只是数学一个学科的事。

AI for Math 的范式漂移，将成为所有强证实型学科的预演——理论物理中的计较验证、暗码学中的安全性证实、软件工程中的情势化验证——所有依靠「准确性论证」作为焦点产出的范畴，都将面对一样的「阻抗掉配」。

证实会愈来愈多，愈来愈快，愈来愈自制。

证实的时代没有竣事。

但「证实即一切」的时代，正于落幕。

将来属在那些不仅能「算出来」，更能「批注白」的人。

【本文由投资界互助伙伴微信公家号：新智元授权发布，本平台仅提供信息存储办事。】若有任何疑难，请接洽（editor@zero2ipo.com.cn）投资界处置惩罚。