OpenAI 最新內部推理模型，一次發布了十項驚人的數學進展。
其中包括：
- 首次證明了非 Sofic 群（Non-sofic groups）的存在性；
- 给出了全新的電路下界（Circuit lower bounds）；
- 攻克了最近向量問題（Closest Vector Problem，CVP）難度極限；
- 以及雙人量子博弈並行重複指數衰減定理（Quantum parallel repetition）。
最令哥倫比亞大學副教授 Henry Yuen 在乎的是最後一個——
2016年，Yuen 在該問題上取得了重大進展，但並未徹底解決。10年來，他屢戰屢敗，甚至一個月前他還用 ChatGPT 5.5 再次向終極證明衝鋒，但收穫寥寥。
而AI在他的肩膀上，輕輕一腳，把球送進了球門。
證明對了，人類卻沒理解
幾天前，陳立傑發送了一份論文草稿給袁海亨和其他幾個人。
當時生活很忙，他無暇深入研讀。現在，論文已經公布。他不吐不快，有話要說。
量子並行重複定理（Quantum parallel repetition theorem）是 Henry Yuen 在研究生階段耗費數年心血鑽研的領域，也是他最引以為傲的成果。
Henry Yuen，現任哥倫比亞大學 Srivani 家族計算機科學副教授
他記得那些泡在咖啡館裡的午後，坐在辦公室裡的深夜，還有無數個本該休息的週末，反覆拆解研讀 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 弃子如泥沙，毫無預警、毫無解釋地丟在了第四節。
Correct proof, but the most important idea has been hidden.
He hopes OpenAI can spend a few more prompts to properly organize this manuscript.
更扎心的是第二層：Lean 驗證通過，不等於理解。
機器可以保證每一步推導無懈可擊，但「為什麼這一招有效」「它在更大的理論版圖裡意味著什麼」「還能用在哪裡」——這些問題，Lean 一個都答不了。
Yuen坦言，他到現在還在消化這份證明。
答案就在眼前，他卻要像閱讀外行的論文一樣，一行行還原 AI 沒說出口的直覺。
沒錯，是有個 Lean 證明在那兒。但那只是形式化，不代表我懂了。真要消化，恐怕只能靠時間慢慢磨。
的確，AI 擴寬了人類理解的疆域，但然後呢？研究的樂趣和意義還剩什麼？要是 AI 把他魂牽夢縈的難題都解決了，他還剩什麼？
問題接踵而至。但有一點他越來越確定：數學家接下來的日子不會閒，既要馴服這些思想巨獸，還得把它們的黑話翻譯成人話。
AI「證偽」百年數學猜想遭打假！Lean 也不是保險箱
上週，Ramana Kumar 以 300 行 Lean 證偽了最著名的數學未解之謎「科拉茲猜想」（Collatz conjecture）。
它問的問題特別簡單：給你一個正整數，按照兩條規則反覆操作——偶數就除以 2，奇數就乘以 3 再加 1——最後是不是不管從哪個數出發，都會一路跌到 1？
你可以算一下：
This conjecture states that no matter which positive integer you start with, you will eventually fall into the 4→2→1 cycle.
自數學家 Lothar Collatz 於 1937 年提出此問題以來，沒有人能證明其成立，也未找到反例。
它被數學家 Paul Erdős 稱為：「數學還未準備好應對這樣的問題」，而美國國家科學院院士、數學家 Jeffrey Lagarias 則認為：「這是一個異常困難的問題，完全超出了當今數學的範圍」。
If falsified, it would undoubtedly be a groundbreaking news in the mathematical community.
可惜的是，3 天後，這份形式化的 Lean 證明被判定無效，因為它實際上只是利用了 Lean 核心的一個底層漏洞。
OpenAI 的 Daniel Selsam 搭配一名專攻網路安全的 AI，協助 Lean FRO 進行了一次核心審計。
結果，他們在 Lean 核心中發現了不止一處漏洞！
幾乎同一時間，羅格斯大學數學教授、Lean 專項研究組織顧問 Alex Kontorovich 發文提醒：別把 Lean 當全能驗證者。
他直指死穴——Semantic Alignment。
即使 Lean 核心無懈可擊，Lean 也只負責代碼編譯。誰來確保你寫在代碼中的「定義」與人類在自然語言中的「直覺意圖」是一回事？
Lean 能確認的只有一件事：代碼編譯通過，形式邏輯無誤。但它絕不驗證一個更致命的問題：這段形式化陳述，真的對應你想證明的那個定理嗎？
Theorem proved correct, but problem copied incorrectly—Lean still green-lights it.
而這個對齊問題，無法單靠電腦解決。
在 ICM 2026 的演講中，Kontorovich 曾指出：形式化數學最大的盲區，不在「推對了導」，而在「說對了話」。最後把關的，還得是人類專家。
當年 Liquid Tensor Experiment 能夠封神，靠的正是研究者對每個數學定義近乎偏執的人工審查。
將兩位教授的話放在一起看，指向同一個事實：AI 能證明，機器能驗證，但理解和把關，還是人類的活。
最後，還有個關於 AI 推理模型的八卦：
參考資料：
https://www.henryyuen.net/posts/on-openai-and-quantum-parallel-repetition/
https://x.com/AlexKontorovich/status/2083919186825236831
https://x.com/henryquantum/status/2083623700608237956
本文來自微信公眾號「新智元」，作者：ASI 啟示錄；編輯：大衛