姚期智楊植麟首次聯手給 AI 出的博士級題目，Kimi 多畫出了「關鍵一條邊」

Kimi 刷新 629 條邊圖論參考紀錄，只多加了1條邊，為什麼數學界等了這麼多年？作者丨鄭佳美 編輯丨岑 峰 給 124 個點連線，不能出現三角形，也不能出現四邊形。此前的參考記錄是 629 條——數學界認為這已經接近極限。而Kimi K3 構造出了 630 條邊的圖，並通過程序驗證。多1條邊，聽起來不多。但在組合數學裡，你每試圖多塞進一條邊，都需要在全圖 124 個點之間重新完成一次精密的結構大重構。這1條邊意味著AI第一次在“極值構造”這類研究級任務上，把人類參考紀錄往前推了一步。這項成果來自圖靈獎得主、中科院院士、清華大學交叉信息研究院院長姚期智與月之暗面創始人楊植麟等人的聯合研究。

他們真正想回答的問題是：AI到底能不能做數學研究，而不只是做數學題？01「多 1 條邊」算不算真突破？姚期智，圖靈獎得主、清華大學交叉信息研究院院長，是中國理論計算機科學的奠基者之一；楊植麟，月之暗面創始人，Kimi背後的推動者。兩代人、兩種身份：一位是理論計算機科學的泰斗，一位是大模型創業的一線操盤手，第一次聯合署名。這個組合本身就說明了一件事：AI做科研，已經不是“實驗室裡的猜想”，而是需要理論計算機科學家和大模型團隊坐在一起定義“什麼叫算做出來了”。但在另一面，爭議同樣如影隨形：多構造出一條邊，到底算不算真正的科學突破？這算不算只是暴力搜索蒙對的個例？AI真懂背後的數學機理嗎？

這正是姚期智團隊的核心初衷。如果無法區分‘運氣好撞上’和‘邏輯上證明’，AI 就永遠只是個黑盒計算器。於是，他們沒有繼續在傳統基準上打轉，而是聯手搭了一套前所未有的評測系統——TCSExam。為回答這個問題，他們提出 TCSExam，用 100 項理論計算機科學科研任務，測試前沿 AI Agent 能否證明定理、開發 Solver、構造數學對象，甚至挑戰長期未解決的猜想。論文地址：https://arxiv.org/pdf/2611.

07962v1實驗中，GPT-6 Astra 完成了 20 項研究級定理中的 14 項，還將一個有限域矩陣猜想在特定條件下的已知證明範圍從 8 維推進到了 9 維。TCSExam 的核心創新，是將 AI 科研能力轉化為可以獨立驗證的研究成果。它通過 Lean 4、程序檢查器和 Checkpoint 機制，分別驗證數學證明、算法表現及中間推導，避免把局部進展誤判為完整成果。其中，Astra 的 9 維證明將複雜的矩陣問題壓縮為整數約束，最終利用 143 條方程構造出可核驗的矛盾證書。從任務形式化、研究證書設計到數學證明的自動檢查，這套框架展示了 AI 參與真實科研的一條技術路徑。

02TCSExam 如何建立評測框架？一句話：把“AI 做科研”拆成四條可驗證的軌道，再用三層機制防止“局部進展被誤判為完整成果”。普通數學考試有標準答案，而理論計算機科學涉及的研究工作差異很大，有的需要證明新定理，有的需要開發最優算法，有的要構造滿足約束的數學對象。這些成果的形式不同，評價方式也必須隨之調整。研究團隊因此將 100 項任務劃分為四條軌道：定理證明（20 項）：覆蓋 13 個理論計算機科學領域，要求模型提交 Lean 4 證明。

Solver 工程（30 項）：要求開發可重複運行的算法程序，在獨立測試實例和統一資源限制下評測；數學構造（20 項）：考察模型能否生成符合嚴格約束的圖、糾錯碼等對象；開放猜想（30 項）：允許模型從證明成立或尋找反例兩個方向展開研究。任務劃分之後，更復雜的問題出現在數學語言的轉換過程中。人類研究者能夠理解一段定理描述，但機器驗證需要明確的定義、量詞、假設和參數範圍。任何一個條件發生變化，最終證明的數學含義就可能不同。例如，一個定理原本要求某種性質對任意規模的圖成立，如果轉寫成 Lean 時額外增加了圖規模限制，那麼模型即使完成證明，也只解決了範圍縮小後的問題。

形式化證明系統能夠檢查代碼中的邏輯，卻無法自行判斷它是否忠實於原始研究目標。TCSExam 為此建立了任務編寫與獨立審核機制。編寫 Agent 根據研究材料構建形式化命題、提交接口和驗證程序，審查 Agent 再核對定義、量詞及參數條件，並通過邊界樣例和試運行排查問題。研究領域專家負責審定任務的研究意義。開發過程中，超過 40 道候選定理因試運行階段已被解決而退出題庫。Solver 軌道還額外做了兩件事：對部分實例做保持數學性質不變的變換，減少直接複用已有答案；數學構造軌道則固定合法性條件與參考紀錄，保證可比性。對於證明任務，研究團隊還進一步控制模型能夠獲得多少研究指導。

Bare 模式只提供定理和必要定義，Ladder 增加中間引理，Guided 則提供證明思路。這三種條件使用相同的主定理，讓研究者能夠分析模型是在尋找證明路線時遇到困難，還是已經知道關鍵步驟後仍無法完成推導。經過這些設計，TCSExam 將研究問題轉化成了有明確輸入、執行條件和交付要求的任務。但模型提交的成果可能包含大量中間推導，如何從中識別真正成立的數學結論，還需要另一層驗證機制。03怎樣區分局部推理與完整證明？TCSExam 的底層設計利用了理論計算機科學中的一個重要特點：找解難，驗解易。研究團隊將這種思想應用於科研評測，要求 Agent 把探索結果整理成驗證器能夠檢查的研究證書。

對於定理證明，這份證書就是 Lean 代碼。Lean 內核根據形式邏輯規則檢查推導，系統還會審計證明依賴，排除未完成證明佔位符和未經允許的額外公理。不過，研究級定理往往需要多箇中間引理，模型可能完成大部分推導，卻始終無法處理某個關鍵步驟。僅憑主定理是否通過，很難判斷具體的能力缺口。TCSExam 因此設計了 Checkpoint 機制，把複雜證明拆成多箇中間目標。驗證其中一個 Checkpoint 時，系統會暫時把其他 Checkpoint 的命題作為假設，檢查模型能否在這些條件下完成當前推導。這種處理有一個重要的邏輯邊界。

假設證明 A 時借用了 B，證明 B 時又依賴 A，那麼即使兩個局部檢查分別通過，整體證明仍然存在循環依賴。因此，Checkpoint 的成績只能反映條件性推導的完成程度，主定理必須在移除未經證明的中間假設後，再接受獨立檢查。一個案例很能說明這種區別：Kimi K3 在某次嘗試中完成了 7 箇中間 Checkpoint，覆蓋程度達到 87.5%，卻沒有完成主定理所需的最終推導。系統保留了局部成績，同時拒絕將其認定為完整證明。結合三種指導條件，還能進一步看到模型能力的差異。

Kimi K3 在 Bare、Ladder 和 Guided 模式下分別至少完成 3、4、7 道不同定理，DeepSeek V4.1 Flash 0910 則分別完成 0、2、6 道。提供中間引理與證明思路後，模型的完成數量明顯增加，說明困難往往集中在關鍵引理的發現，以及如何將分散的推導組織成完整證明。另外，Checkpoint 只是一種輔助分析方式。如果模型繞過預設的中間引理，直接構造出完整有效的主定理證明，系統同樣能夠接受。這為 Agent 保留了自主尋找證明路線的空間。研究證書機制在 Solver 中採用不同實現。

模型需要提交可重複運行的程序，檢查器重新判斷輸出是否合法，並計算實際目標值。以 IWLS 2023 邏輯綜合任務為例，GPT-6 Astra 在 100 個實例中均生成了有效電路，其中 22 個優於公開參考電路，31 個達到參考水平，另外 47 個使用了更多 AND 門。為了避免不同實例的數值尺度影響整體評價，系統還引入相對於 Kimi K3 多次運行結果的標準化評分，使有效性與優化質量能夠分別衡量。數學構造軌道也採取類似處理，先檢查對象是否滿足結構約束，再比較它取得的數學參數。當研究目標進一步擴展到開放猜想時，僅靠局部覆蓋或數值改進已經不足以判斷結論是否成立。

模型需要找到一條完整的數學證明路線，並將其中複雜的結構分析轉化成可以逐步核驗的證據。GPT-6 Astra 在 Alon–Jaeger–Tarsi 猜想上的研究，正好展示了這個過程。04從 8 維到 9 維Alon–Jaeger–Tarsi 猜想研究有限域上的可逆矩陣。簡單理解，給定一個可逆矩陣，研究者希望找到一個所有座標均不為零的向量，並且經過矩陣變換後，新向量的所有座標仍然不為零。此前相關研究已經覆蓋五元有限域中不超過 8 維的情形，Astra 將這一範圍推進到了 9 維。隨著維度增加，需要考慮的矩陣與向量組合迅速膨脹，直接枚舉難以完成證明，因此它採用了另一條數學路線。

證明首先假設存在一個不滿足猜想的 9 維矩陣，再利用低維情形已經成立的結論，限制這個反例必須滿足的條件。接下來，Astra 不再逐個分析矩陣元素，而是轉向研究向量經過矩陣變換前後的非零座標數量。它構造了兩組 10×10 的非負整數數組，分別描述原矩陣和轉置矩陣作用下，不同座標數量之間的對應關係。矩陣可逆性限制了數組的行列總數，有限傅里葉恆等式則建立了兩組數組之間的聯繫。結合反例的結構性質，還可以推導出部分計數必須為零。這些條件將原本複雜的矩陣問題逐漸轉化成整數約束，但仍然需要進一步縮小檢查範圍。

Astra 隨後分析矩陣中兩個列向量的座標關係，將它們按照零元素分佈及非零元素之間的消去比例劃分為 7 種類別。由於矩陣維度為 9，各類別的數量之和必須為 9，因此可能出現的類別計數組合只有 5005 種。這個步驟完成了關鍵的規模壓縮。系統無須枚舉全部 9 維可逆矩陣，只需要檢查這些有限類別組合對應的數學約束。在此基礎上，Astra 將相同的結構分析應用於原矩陣、逆矩陣、轉置矩陣及其逆矩陣，得到四組額外的非負約束。結合此前構造的兩組計數數組，最終形成一個包含 204 個非負變量的整數線性系統。此時，證明已經轉化為判斷這些整數約束能否同時成立。

Astra 從原始的 197 條方程中，選取 143 條具有非零乘子的方程，按照特定整數係數進行組合，得到一個無法成立的關係：204 個變量的係數全部非負，等式右側卻是負數。由於變量本身也必須非負，這樣的關係必然產生矛盾，因此假設中的 9 維反例無法存在。這份證書將複雜的矩陣推導壓縮成有限的整數計算。獨立核驗確認，組合後的 204 個係數中，93 個為正，111 個為零。整個證明還被整理成包含 71 個 Lean 模塊的項目，在獨立環境中重新編譯，並完成公理依賴檢查。

從極小反例出發，通過座標計數建立約束，再利用有限類別分析縮小問題規模，最終以整數矛盾排除反例，這條證明路線體現了 AI 將數學結構分析與計算工具結合的能力。不過，Astra 完成的是五元有限域上的 9 維特殊情形，完整的 Alon–Jaeger–Tarsi 猜想仍未解決。TCSExam 的其他開放猜想實驗同樣表明，當前模型距離獨立解決一般性難題仍有差距。部分被接受的 Ryser 和 MIRUP 反證來自對 OpenAI 已公開成果的檢索與適配，其餘 28 項開放猜想沒有得到完整解決方案。

05從局部發現走向長期研究TCSExam 的實驗顯示，AI 已經能夠完成部分研究級證明，並在算法優化與數學構造中取得可核驗的進展，但獨立尋找關鍵引理、規劃長程證明，以及將特殊結論推廣到一般情形，仍然存在明顯困難。研究證書機制為未來的科研 Agent 提供了一種可迭代的工作基礎。模型可以利用 Solver 搜索候選結構，通過形式化工具檢查數學性質，再根據驗證失敗的位置修改證明策略，將已經成立的中間結果用於後續研究。

這次實驗最值得記住的，不是“630比629多1”，也不是“9維比8維多1維”，而是：AI已經能在部分研究級任務上產出“機器可核驗”的新結果，雖然離“自己提出關鍵引理、自己規劃長程證明”還有明顯距離。對Kimi和月之暗面來說，這是一次“AI for Science”的能力展示；對數學界來說，這是一套可以複用的評測框架；對普通讀者來說，這可能是一個信號：AI做科研，正在從“幫人查文獻、寫代碼”，走向“幫人證定理、找反例”。