新智元报方式OpenAI内部最新推理模型，证伪一口气发布了十项惊人的百年被打数学开展。其中涵盖：首先次说明了非Sofic群（Non-sofic groups）的数学n说授破存在性 ；给出了全新的电路下界（Circuit lower bounds）；攻克了最近向量状况（Closest Vector Problem，CVP）难度极限；以及双人量子博弈并行重复指数衰减定理（Quantum parallel repetition）。猜想最令哥伦比亚大学副教授Henry Yuen在乎的明惊是最后一个——2016年，Yuen在该状况上取得了重点开展，现漏学但并未彻底处理。洞哥大教订阅10年来，防定他屡战屡败，理算量数甚至一个月前他还用ChatGPT 5.5再次向终极说明冲锋，网易但收获寥寥。证伪而AI在他的百年被打肩膀上，轻轻一脚，数学n说授破把球送进了球门。猜想说明对了，明惊人类却没理解几天前，Lijie Chen发给Henry Yuen和同时几个人一份比如文草稿。当时生活很忙，他无暇深入研读。目前，比如文已经公布。他不吐不快，有话关键说。量子并行重复定理（Quantum parallel repetition theorem），是Henry Yuen在探究生时期耗费数年心血钻研的领域，也是他最引以为傲的成果。Henry Yuen，现任哥伦比亚大学Srivani Family方式算机科学副教授他记得那些泡在咖啡馆里的午后，坐在办公室里的深夜，还有无数个本该休息的周末，反复拆解研读Ran Raz的经典并行重复定理。他想处理这个定理的量子版本，为此夜不能寐、辗转反侧。他吞下了成吨的数学工具，最后成功说明了多项式衰减。https://arxiv.org/pdf/1604.04340更题的是，他从中建立了信心，终于认清自己的实力，说明了他确实能处理那些（至少一部分）别人也在乎的状况。他相信OpenAI的这份说明应该是正确的，毕竟已经有Lean形式化说明。但关键消化这个新说明，Henry Yuen还需一些时间。虽然新证清楚实从他之前结束的地方后续出发，但AI突破了他原有说明对策的限制，采取了一些技巧和方式。这些方式或许已经被算子理比如（operator theory）和泛函探究（functional analysis）领域的探究者所掌握。兴奋之外，Yuen的首先个感受是失望，对比如文写作风格的失望。他说这份说明读起来满是AI味儿：冗首先的铺垫绕了半天，题环节却像变魔术，让人一头雾水。OpenAI的说明，读来颇有意思，却也有些令人头疼。它先把状况端端正正地摆在桌上，然后忽然一跃到「用预解式去找正确的purification」这个方向，中间几乎不留任何逻辑阶梯。接下来，便是一连串颇为另类的矩阵熵方式算，弯弯绕绕地算下去，末了告诉你：这条路走得通。可那最题的一步，那个直觉究竟从何而来，它没有说。而最精妙、最考验创造力的那一笔——利用Uhlmann 变换（Uhlmann transformation）开展算子空间膨胀的技巧，本应是整篇说明最动人心魄的高潮，却被AI弃子如泥沙，毫无预警、毫无验明正身地丢在了第四节。正确的说明，却藏起来了最题的想法。他希望OpenAI能多花几个提示词，把这篇文稿好好理一理。更扎心的是第二层：Lean验明正身通过，不等于理解。机器可以保证每一步推导无懈可击，但「为什么这一招有效」「它在更大的理比如版图里意味着什么」「还能用在哪里」——这些状况，Lean一个都答不了。Yuen坦言，他到目前还在消化这份说明。答案摆在面前，他却关键像读外行的比如文一样，一行行去还原AI没说出口的直觉。没错，是有个Lean说明在那儿。可那只是形式化，不代表我懂了。真关键消化，恐怕只能靠时间慢慢磨。的确，AI拓宽了人类理解的疆域，但然后呢？探究的乐趣和意义还剩什么？关键是AI把他魂牵梦绕的困难都处理了，他还剩什么？状况接踵而至。但有一点他越来越选定：数学家接下来的日子不会闲，既关键驯服这些思想巨兽，还得把它们的黑话翻译成人话。AI「证伪」百年数学猜想被打假！Lean也不是保险箱上周，Ramana Kumar用300行Lean证伪了最出名的数学未解之谜「科拉兹猜想」（Collatz conjecture）。它问的状况尤其便捷：给你一个正整数，按两条规矩反复操作——偶数就除以 2，奇数就乘以3再加1——最后是不是不管从哪个数出发，都会一路跌到1？你可以算一下：这个猜想说的就是：不管你拿哪个正整数开头，最后都会掉进这个 4→2→1 的圈里。这个状况自数学家Lothar Collatz在1937年提出后，没有人能说明它成立，也没有找到反例。它被数学家Paul Erdős称为：「数学还没准备好处理这样的状况」，而美国科学院院士、数学家Jeffrey Lagarias则认为「这是个异常不易的状况，完全超出了当今数学的范围」。如果被证伪，无疑是数学界爆炸性新闻。可惜的是，3天后，这份形式化的Lean说明被判无效，因为它实际上只是利用了Lean内核的一个底层漏洞。OpenAI的Daniel Selsam，带着一个专攻网络安全方向的 AI，协助Lean FRO做了一次内核审方式。结荚，他们在Lean内核里发现了不止一起漏洞！几乎同一时间，Rutgers大学数学教授、Lean专项探究组织顾问Alex Kontorovich发文提醒：别把Lean当全能验明正身者。他直指死穴——语义对齐（Semantic Alignment）。即使Lean内核无懈可击，Lean也只管代码编译。谁来确保你写在代码里的「定义」和人类在自然语言里的「直觉意图」是一回事？Lean能确认的只有一件事：代码编译通过，形式逻辑无误。但它不过不验明正身一个更关键命的状况：这段形式化陈述，真的对应你想证的那个定理吗？定理证对了，题抄错了，Lean照样绿灯放行。而这个对齐状况，没法纯靠方式算机处理。在ICM 2026的演讲里，Kontorovich就点过：形式化数学最大的盲区，不在「推对了导」，而在「说对了话」。最后把关的，还得是人类专家。当年Liquid Tensor Experiment之因此封神，靠的恰恰是探究者对每个数学定义近乎偏执的人工审查。把两位教授的话放在一起看，指向同一个事实：AI能说明，机器能验明正身，但理解和把关，还是人类的活。最后，还有个关于AI推理模型的八卦：参考材料：https://www.henryyuen.net/posts/on-openai-and-quantum-parallel-repetition/https://x.com/AlexKontorovich/status/2083919186825236831https://x.com/henryquantum/status/2083623700608237956编辑：大卫