很多人第一個會先想到，Google DeepMind 的 AlphaProof Nexus 解出九個 Erdős 問題，是否代表 AI 已能獨立做數學研究。這個問題要先定義清楚：九題從哪裡來、證明如何檢查、《Science》刊登又增加哪種可信度。這些證據支持特定研究成果，不能直接代表 AI 已具備普遍的數學研究能力。

一、九個 Erdős 問題的分母是什麼？

九個是 353 個已被嘗試的形式化敘述中，系統成功證明的數量。這 353 個來自研究當時開放的 Formal Conjectures 專案裡、已寫成 Lean 形式的 Erdős 問題敘述，不是全部 Erdős 未解問題，也不是隨機抽出的數學題。

Paul Erdős 留下大量數學問題，研究論文提到線上目錄收錄超過 1,200 個仍未解的問題。AlphaProof Nexus 實際處理的是其中一部分：Formal Conjectures 開源專案已經把問題翻譯成 Lean 可讀的形式陳述；研究團隊在執行當時對這 353 個形式敘述逐一進行搜尋。每題最多搜尋 3,000 個 episode（模型反覆推進證明草稿的回合），研究報告其中九個成功得到無 sorry 的證明。分母反映的是既有形式化工作的範圍與本次實驗設定，不應簡寫成「AI 在全部未解數學問題裡解出九題」。

題目須先有人形式化，並寫入所需定義與輔助定理，才成為搜尋輸入；因此可測題目可能偏向定義成熟、適合現有 Lean 函式庫表達的領域。九除以三百五十三只描述這次測試，不是 AI 解決任意數學問題的通用機率。

研究還報告另一組不同來源的結果：系統證明了 492 個 OEIS（整數數列線上百科）猜想中的 44 個。OEIS 與 Erdős 題集在問題來源、形成方式和評估資料上不同，不能把兩組數字混成「解出五十三個 Erdős 問題」或拿來當成同一個測試的成功率。研究亦提及代數幾何、凸最佳化、量子光學與圖論等延伸工作，但這些案例的工作方式和證據型態也不完全相同；每一項都應回到論文內的說明判讀。

閱讀「數十個未解數學問題」時，應確認它涵蓋哪些猜想、計數單位與成功分母，再判斷題目是否貼近自己的研究領域。

二、AlphaProof Nexus 如何找到可檢查的證明？

AlphaProof Nexus 讓語言模型代理反覆修改 Lean 證明草稿，再由 Lean 編譯器檢查形式推導是否成立。模型負責提出候選路徑，形式系統檢查輸入命題下每一步推導；這降低自然語言證明中漏步或邏輯跳躍未被察覺的風險。

Lean 是互動式定理證明器，定義、定理與證明都寫成可檢查的程式。AlphaProof Nexus 以包含目標定理、依賴定義和未完成證明的 Lean 檔案為輸入。多個子代理各自嘗試，並依編譯器錯誤修改草稿；較完整的代理還會將草稿存入共享資料庫，以評分和搜尋挑選方向，或調用 AlphaProof 處理特定子目標。

對使用者而言，這種流程的差異在於「看起來像證明」和「形式規則接受的證明」不再是同一件事。一般語言模型能寫出流暢、步驟看似合理的文字，卻可能在中間推論偷換條件。Lean 需要每個子目標依照已載入的定義與定理成立；沒有完成的目標或保留的 sorry（暫代證明的標記）不能算作完成的證明。研究團隊公布了 Lean 證明檔，讓其他人可以取得材料，嘗試重新編譯檢查。

Lean 定理與未完成證明草稿經多個代理嘗試，依編譯器回饋反覆修正，最後得到不含 sorry 的完整證明。
代理提出候選推導，Lean 編譯器逐步檢查，兩者分工讓形式證明可被核對。

不過，機器檢查的前提，是輸入定理表達了人原本要問的問題。若定義翻譯時少了限制、條件寫錯，或形式命題只是原問題的某個變體，Lean 仍可能正確驗證那個已寫下的命題。形式化證明的成功因此包含兩個層次：Lean 確認形式推導成立，研究者再核對形式陳述有沒有忠實對應原始猜想。論文說，研究團隊在每次成功後安排專家確認 Lean 陳述是否忠實表達原猜想。這項核對很重要，但仍要看公開材料和社群後續檢查如何補充。

這也解釋了為什麼「Lean 通過」不能被擴張成「原始問題的所有意思都已確認」。編譯器處理的是形式語言中的定義與推理規則，不會自行判斷題目選擇是否公平、研究問題是否有價值，或證明是否帶來新的數學洞見。形式系統提供的是可重複檢查的一層可靠性，問題定義與數學詮釋仍需研究者負責。

「因證明草稿已形式化，數學家合作者可聚焦尚未解出的子目標，不必重驗整段論證。」（Tsoukalas 等人，研究論文，Discussion，本文譯）

三、《Science》同儕審查替成果增加了什麼？

論文刊於《Science》表示研究以期刊論文形式發表；同儕審查增加了專家檢視的程序證據。這不等同於每一份證明都已由期刊外的數學家獨立重做，也不表示論文中的所有延伸解讀都獲得同等驗證。

研究先以預印本公開，後刊於《Science》。同儕審查會檢視方法、數據解讀及主張的論據，並可能要求補充或修正；正式論文也讓研究方法與材料有可追溯的來源。

「經審查」不代表審查者逐行重跑 353 題，也不等於外部團隊已獨立重現。研究團隊公開 Lean 證明與部分自然語言證明；重現仍需以相符版本和依賴套件重新編譯，並核對題目、定義與證明的對應。材料可取得、機械可重跑、獨立重現是不同證據層次。

三張並列卡片分別呈現期刊同儕審查研究主張、Lean 編譯器檢查形式推導，以及外部研究者取得材料後重做檢查。
期刊審查、形式驗證與獨立重現各自回答不同問題，判讀成果時應分開確認。

看到《Science》刊名後，仍可查論文是否提供程式、題目清單與運算設定，形式命題是否附原始問題來源，以及有無外部數學家檢視證明與翻譯。這些資訊分別影響對方法、形式證明及命題對照的判斷。

研究論文的成本估算段以推論費用描述計算成本，並說明估值未涵蓋找出可解題目所需的完整計算成本（Tsoukalas 等人，研究論文）。

研究估計完整代理平均每題推論成本為數百美元；這是計算資源估值，不能與數學家的研究工時、專業訓練或成果價值直接相比。

四、九個成功結果有哪些評測限制？

因為成功率只描述特定題集、輸入形式、搜尋上限與系統配置下的結果。題目如何進入測試、形式化品質如何、每題跑了多少次，以及不同數學領域是否被充分涵蓋，都會影響結果可以外推到哪裡。

第一個限制是題目偏差。353 個敘述經人整理與形式化後才進入搜尋，未必涵蓋 Erdős 問題的各領域，也不代表尚未形式化或難以用現有 Lean 函式庫表達的題目。其他領域若缺少定義或前置引理，結果便不能直接類推。

第二個限制是搜尋預算。不同配置使用多個代理或多輪嘗試，完整代理也會調用子代理，因此這不是單次問答測試。平行搜尋增加找到證明的機會，也耗用時間與算力；解讀九題時須一併看方法、預算與成本。

第三個限制是「解出」不等於產生易懂或可延伸的新方法。證明是否簡潔、能否揭示一般結構或用於其他問題，仍需數學社群閱讀和延伸，不能由機械檢查判定。

導入評估還須計入題目形式化、函式庫整理、研究者核對及維護等人工成本。這組結果顯示代理能在特定形式化題集中搜尋證明；比較其他工具時，應一併列出題目來源、搜尋預算、機器檢查及人類核對方式。

五、研究者與工具採用者該看哪些證據？

先查題目與形式陳述，再查證明如何驗證、結果能否重現，最後看同儕審查涵蓋的主張。這套次序能把「答案看起來正確」拆成可以逐項確認的證據，也讓讀者知道哪些判斷仍需專家完成。

研究團隊或大學可從小規模任務評估工具：選取來源公開、形式陳述可核對的題目，記錄所有嘗試與失敗；以相同版本的 Lean 和程式庫重編譯完整證明；再核對形式命題是否等同原題。最後比較時間、推論費用、人工複核成本，以及證明能否理解與延伸。

這些步驟讓責任分工更具體。AI 可以探索候選解法、拆分子目標、從編譯器錯誤中調整證明草稿；研究者要定義問題、檢查形式化忠實度、判讀新穎性和研究意義。若用於團隊工作，還需記錄模型、代理設定、Lean 版本、函式庫、搜尋預算和人工修改，讓同事能分辨哪些部分由系統提出、哪些部分由人整理或修訂。這些紀錄同時是重現研究結果和追查錯誤來源的基礎。

對一般讀者來說，閱讀 AI 研究新聞時可先問三件事：它嘗試了哪些題目，成功與失敗的母數是什麼；系統檢查的是自然語言答案、形式化推導，還是兩者都有；期刊審查、公開材料和獨立重現分別到哪一步。遇到「AI 解決數十個難題」之類說法，先找研究論文與附錄，看數字的計數單位，再查看公開證明或資料庫。當來源只提供成功案例、沒有測試分母和查證方式時，適合把它視為需要後續確認的主張。

  • 九個是 353 個當時已形式化並受測的 Erdős 敘述中的成功數，並非全部未解數學問題的抽樣結果。
  • Lean 能檢查形式化命題下的推導，仍需要人確認形式命題忠實對應原始問題。
  • 《Science》同儕審查、公開證明與獨立重現是不同層次的證據，應逐項確認。

對 AI 能力的判斷，關鍵是把結果拆回問題定義、原因和方法：它能在怎樣的輸入下找到什麼，形式系統替哪一段把關，還需要哪些人類工作。AlphaProof Nexus 的成果顯示，AI 輔助形式化證明搜尋在這項研究設定下已有可檢視的成果；是否適用於其他題集或實際研究流程，則要看相同標準下的後續驗證與重現。

常見問題

Q1: AlphaProof Nexus 解出九個 Erdős 問題，代表成功率約 2.5% 嗎？

九除以 353 約為 2.5%，只描述論文設定的形式化題集和搜尋條件。這個比率不代表系統處理任何數學問題的通用成功率，因為題目來源、形式化門檻和搜尋預算都會影響結果。

Q2: Lean 驗證通過後，數學家還需要檢查什麼？

Lean 驗證表示證明符合程式中的形式定義和推理規則。數學家仍要確認定義及定理是否準確表達原始問題、所用假設是否合適，並判斷證明的新穎性、可理解性與研究價值。

Q3: 論文經《Science》同儕審查，是否等於外部獨立重現？

不等於。期刊審查增加專家檢視研究設計和論述的程序；獨立重現則由未參與團隊的人另行取得材料、設定環境並重做檢查。兩者是不同的驗證步驟。

Q4: AlphaProof Nexus 的 44 個 OEIS 猜想可以和九個 Erdős 問題合計嗎？

不宜直接合計成同類的成功題數。OEIS 與 Erdős 題集來自不同資料庫，題目如何選取、形式化與評估也不同；應保留各自的分母和方法來解讀。