九章雲極問鼎SAIR數學蒸餾挑戰賽 四賽道滿分全球第一
/朝聞通/近日，SAIR Foundation 數學蒸餾挑戰賽(Mathematics Distillation Challenge)第二階段公布主榜成績。九章雲極言表實驗室(yanbiao.ai)參賽團隊在全部四個賽道均取得滿分第一，進入全球主榜滿分陣營。同期，九章雲極與北京大學計算機學院聯合完成的論文《Trace-Tree Magmas: Proof-Producing Infinite Countermodels and 28 New Order-Five Austin Classifications》公開發表(arXiv:2609.05690)，首次為28個長期開放的數學等式建立新的 Austin 分類。
據了解，本次挑戰賽由 SAIR Foundation 發起，菲爾茲獎得主、加州大學洛杉矶分校(UCLA)教授、SAIR Foundation聯合創始人Terence Tao(陶哲軒)，以及賓夕法尼亞大學統計學與數據科學副教授Damek Davis共同組織。言表實驗室(yanbiao.ai)作為九章雲極旗下的AI4S研究機構，聚焦自動推理、形式化驗證與科學發現等場景。
一場不一樣的數學比賽：
這項賽事為何叫“蒸餾”?參賽者的目标不是讓 AI 生成更長、更複雜的推理，而是把機器産生的大量推演結果，壓縮成泛化能力更強的證明文本，學界認為壓縮是知識變成智能的原因，也是期待通過蒸餾壓縮看到更強大的智能體。
本階段比賽聚焦等式理論中的推理問題：給定兩個等式，判斷前者是否必然推出後者。參賽系統不能隻回答“是”或“否”——蘊含成立時提交 Lean 4 形式化證明，不成立時提交反例，所有結果由确定性的 Lean 驗證器逐一檢驗，驗證未通過不得分。
這一機制把評判标準從“答對率”改寫為“可驗證性”：猜對不算數，證明通過才算數。在數學推理領域，這被視為衡量系統真實推理能力的硬标準。在這一機制下，言表實驗室的求解器完成了全部賽道的所有評測題，以滿分位列主榜并列第一。
從
比賽證明的是“會解題”，論文展示的則是更難的能力——“能發現”。
這項由九章雲極與北京大學計算機學院合作完成的研究，瞄準等式理論中的公認難題 Austin 法則：這類等式的所有有限模型都是平凡的，卻存在非平凡的無限模型——沒有哪張有限的乘法表，能夠見證一個無限的存在，傳統有限模型搜索器在原理上就無法觸及。
論文的主要貢獻者來自北大-九章雲極多智能體聯合實驗室。該實驗室由北京大學計算機學院楊仝教授與九章雲極AI首席科學家缪旭博士共同領導，聚焦多智能體自進化能力研究。
團隊的方法另辟蹊徑：用有限條規則，在無限的構造樹上“有限呈現”一個真正無限的數學結構;每一個被報告的模型，都必須附帶一份自包含的 Lean 4 證明：
·在國際等式理論項目(ETP)鎖定的 96 個五階候選等式中，為其中 28 個此前沒有任何公開分類的等式首次構造出非平凡無限模型，建立 28 項新的 Austin 分類，歸于 14 個對偶類;
·一次完整搜索共生成 636 份 Lean 4 證書，全部被賽事驗證器接受;
·與國際主流自動定理證明器 Vampire等同資源對比中，三者對這 28 個等式無一能夠判定，也無一能産出模型或形式化證書;
·經系統的文獻與公開成果審計，這是全球首個能夠合成此類模型、生成其良基證明并輸出自包含 Lean 4 證書的自動化系統。
支撐這些成果的，是一套“信任邊界”設計：搜索與生成程序本身不被信任，任何候選結果必須通過 Lean 内核驗收才會被計數。這與比賽的評測哲學一脈相承，也正是團隊能在“滿分”與“新發現”兩條戰線上同時成立的原因。
從工程底座到AI4S：
自動數學推理對 AI 提出的要求，恰是推理能力與強化學習的交叉點：推理側要求長鍊條邏輯推導保持穩定一緻;強化學習側則要在“證明搜索—驗證反饋”的循環中持續優化策略。九章雲極的求解器正是運行在這一交叉點上的一類特殊負載——大規模并行搜索、長周期疊代、集群持續高壓下的穩定，這些需求與強化學習負載高度同構。這與九章雲極的智算布局同向。訓練工廠支持異構算力上的大規模預訓練、微調與強化學習，Token 工廠承載高吞吐推理任務，二者構成從訓練到落地的完整工程底座。從行業趨勢看，強化學習正成為智算需求的第三曲線，此次的科研成果，正是這條曲線在科學問題上的一個切面。
而這次突破并非孤立的參賽獲獎，而是九章雲極科研脈絡上的新節點：從早年團隊在 Kaggle 登頂世界第一，到此次與北京大學計算機學院合作向基礎研究延伸，九章雲極在AI4S上的投入始終圍繞一個交彙點——向下，以自研智算雲平台提供可調度、可計量的算力底座;向上，讓智能具備進入科學場景的可信資質。
AI4S的真正含義，不止于“算力+推理”的簡單疊加。科學結論必須經得起複核：每一步推導可被獨立驗證，AI才能從“工具”走向“科研參與者”。算力決定AI能算多快，可驗證性決定AI能走多遠——九章雲極給出的答案是兩者都要：以自研智算雲底座支撐“算得動”，以對可驗證性的堅持保證“走得遠”。這條既需要算力、又需要信任的路，正是九章雲極選擇的AI4S之路。
