10月20日，SAIR基金会官方播客放出陶哲轩与邓煜的独家对谈，标题就是那道被问了很久的问题：数学与AI究竟是什么关系。对谈发生在一次冲击之后——一家商业AI巨头一口气公开了700多份由内部模型生成的前沿数学证明，「AI要取代数学家」的讨论瞬间刷屏。两位对谈者都是菲尔兹奖得主：陶哲轩现任SAIR基金会主席，邓煜今年7月在国际数学家大会上当选、现为芝加哥大学教授。而他们给出的共同判断，恰恰与热搜相反：AI能给出数学证明，不代表人类真正理解了这道题。对不写论文的普通人，这场对话其实在描述接下来十年的科研：「答案」会越来越便宜，稀缺的是理解、核查、溯源和下一个问题——科研的竞争点，正在从「谁解出来」转向「谁能消化」。微博36氪
「解出来」和「弄明白」，从此是两条边界
邓煜在对谈里给过一个值得记下的框架：所有问题之中，有证明的问题构成一条边界；已有证明的问题之中，能理解其证明的问题又构成第二条边界。过去第二条边界形同虚设——定理有证明，就意味着有人读懂了它；而现在，如果只有AI「知道」证明，人类第一次可能面对一个自己看不懂的真理。36氪
担忧并非空穴来风。对谈主持人提到，批量发布之后，这家公司因为基本符号错误撤回了数篇预印本，文字证明与Lean形式化代码之间也存在很大脱节，不成熟的结果被快速抛向公众，可能污染学术文献，让研究者沦为「免费调试员」。验证端同样力不从心：这三百来项结果，陶哲轩自己只看了大约十篇。几个流传的数字口径不同，需要说清：该批次原始材料为722篇手稿、归为372组结果，其中3篇预印本后被撤回——「700多」数的是手稿，「三百来项」数的是结果，两个数并不矛盾。36氪知乎
真正要改变的是激励和署名
陶哲轩把问题追到学界自身的激励上：数学一直奖励「解题」，而过去的解题人顺带完成了解释、提出新问题、培养学生，奖项名义上奖解题，实际奖励的是这一整套；AI公司则把数学题当作训练通用模型的基准，顺带解出的题成了副产物——他的原话是「有毒废料」，公司得想办法处理，或者「得由我们来处理」。他的处方是让数学家在开工前就参与进来，而不是事后收拾残局；同时把社区的立场挑明：只解题、不产出理解的成果，不算值得进入文献的东西。邓煜补了一句限定：做数学从来是为了理解世界，价值观没变，变的是情况。36氪
署名机制也在被抹掉。AI可以吸收人类上千年的数学文献，再以不透明的方式把它们转化成答案，有时标注出处，有时根本追不回去。陶哲轩说被切断的是真正意义上的思想链条，而科技公司有动机淡化来源——它们希望让人觉得AI是凭空解决了问题。邓煜举了个更具体的例子：别人的想法此前被输入过ChatGPT，后来被直接用来生成证明。36氪
他们的答案是OpenMathOS——但模型还没做出来
两人没有停在表态，手里有一个具体计划：开放数学模型（OpenMathModel）。一个被二手报道普遍说错的细节需要澄清：对谈时点，他们还没有自己的新模型。率先推出的是OpenMathOS——把现有开源模型、研究工具和协作功能整合在一起的工作平台，使用者不用自己部署模型、不用自购GPU；陶哲轩说，再过几个月才会在开源底子上做出自己的模型。这也不是对抗商业AI——他本人常用专有模型，还专门称赞它们的文献检索能力；他们要防的，是科学家手里只有一种工具，而规则只由公司提供。36氪
紧迫感是事件逼出来的：据媒体报道，9月，OpenAI的模型就千禧年大奖难题纳维–斯托克斯方程给出了相关证明。邓煜在对谈里说，正是这件事之后，推出开放数学模型变得更迫切；随后他发现，南加州大学的朋友在做几乎一模一样的计划，世界各地许多不同团队也开始了同样的事。他判断这是一种趋势：先是数学界，继而是更广泛的学术界，都会努力让数学和科学保持开放。新智元36氪
未来十年，能力留在人这边
工具变强之后，人做什么？陶哲轩的尺子是「工具要让使用者更有能力」：开车不等于永远不许走路，但处处开车，人会忘了怎么走路；他选择相信年轻一代会玩出更有创造力的用法。邓煜点名三种能力：提出正确的问题、整体规划、产生全新的想法。他给过一个分工的真实案例：一个随机偏微分方程问题，人类大致知道路线，AI跑了一两天就完成了推导——但前提是人类已经对问题有了充分理解。36氪
反对的声音同样存在：知乎同一话题下的高赞回答直言，两人复读的只是市面上常见的观点——AI是工具，人要保住能力。这个评价不无道理，对谈没有给出新的预言，它的价值更多在行动上：两位最负盛名的数学家开始造自己的工具，而不只是评论别人的工具。陶哲轩自己在同期访谈里也留了句更警惕的话：同样的做法拿去模拟天气、管电网，迟早会出事。知乎
「理解跟不上」的压力也不会停在数学系：同一批事件里被讨论的一档播客中，麻省理工一位副院长抱怨机器学习顶会ICLR的投稿量十年间从一两千份暴增到今年的六万份，评审连点开PDF都来不及。这场对谈留给普通人的，是一把可复用的尺子：拿到AI给的答案之后，你是更有能力解释它、核查它、接着提出下一个问题，还是只是更快交差。「解出来」和「弄明白」已经在数学最难的问题上分家，而接下来十年，这场分家会走向整个科研。新智元
