很多人第一個會想到，Lean 既然逐步檢查過，數學證明是不是就可信了？這裡還要先問一個更前面的問題：程式檢查的形式化內容，是否忠實表達論文聲稱的命題？OpenAI 在 2026 年 9 月公布 Navier–Stokes 方程的長篇解答與 Lean 形式化；10 月 6 日，三位研究者發布預印本，指出兩者之間有若干差異。爭議焦點因此落在「檢查通過的究竟是哪個命題」，以及讀者能否把程式、論文和研究問題逐項對上。

這對使用 AI 做研究、程式分析或技術決策的人都很實際：一份輸出看起來完整，甚至能在工具中成功執行，也不代表它回答了原本的問題。可驗證性需要分層檢查，並保留讓其他人重做的紀錄。

一、Lean 通過檢查，為什麼數學家仍質疑證明？

Lean 檢查的是輸入程式所陳述的命題與推理，不會自行判斷該命題是否忠實對應論文或原始研究問題。 研究者提出的疑點集中在論文敘述與形式化內容之間的對照，並非宣稱 Lean 核心檢查器失效。

OpenAI 表示，內部系統提出 Navier–Stokes 解答，並公開論文與 Lean 形式化，形式化及檢查在模型提出解答後才完成。OpenAI 的說明屬提出方對成果與流程的描述，須和論文、程式碼及獨立審查分開判讀。

10 月 6 日，Alexander Bastounis、Fabian Circelli 與 Anders C. Hansen 發布預印本，比較論文的自然語言證明與 Lean 程式。他們指出，一項估計在論文中使用輸入函數第 m+4 階導數，形式化結果則要求第 m+5 階；另一項壓力通量估計也有額外依賴。預印本將此列為形式化與原文可能不一致的案例。

這類差異可能改變結論的適用範圍，但預印本分析仍待同儕及數學社群檢視，局部疑點不能直接視為整份證明已被推翻。

論文須經定義、符號、假設與量詞的轉換，才能成為 Lean 命題。若程式加強了「對所有符合條件的函數」中的條件，結論適用範圍就可能縮小；遺漏條件也會使形式化結果脫離原命題。編譯通過無法自行辨認這類語意落差。

二、判讀 AI 數學成果的可驗證性，先分清三層問題

先確認研究問題和命題相符，再確認形式化程式證明了該命題，最後由獨立研究者檢查論證並嘗試重現。 三層互相銜接，任何一層缺資料，都要標示為尚待確認。

檢核層次核心問題可留下的證據
問題與命題研究聲稱的結果是否符合原始問題及其完整條件？原始問題版本、定義、假設和量詞的逐項對照
命題與程式Lean 實際檢查的定理是否就是論文要證明的命題？程式碼連結與固定版本、定理陳述、依賴項、檢查結果
論證與重現不同研究者能否理解證明、找出疑點並在公開環境中重做？獨立審查紀錄、執行環境、重現步驟、未解問題

第一層確認題目是否被正確理解。Navier–Stokes 問題的初始條件、外力限制或解的範圍不同，都可能形成不同命題。核對時應比對論文定理與 Clay 的正式問題描述，不能只看「解決千禧年問題」等摘要標題。Clay 問題頁可作為正式問題設定的對照入口。

第二層要把「論文文字」與「形式化程式」接起來。讀者可先找論文的定理、引理與方程式編號，再找程式碼中對應的 theorem 或 lemma，逐項確認前提、變數範圍、結論和依賴定理。上面的 m+4 與 m+5 差異就屬於這類對照：不必先讀懂整個程式庫，挑出核心主張依賴的引理，查程式碼是否證出相同界限即可。

第三層檢查獨立審查與可重現性。另一位研究者應能在自己的環境重跑，理解定理如何對應原文，並從公開版本重建結果。

三層之外還有機構程序。Clay 規則要求解答刊於合格出版物；刊登後，還須依序達到數學界普遍接受，並經至少兩年嚴格檢視，之後才進入獎項評估。獎項規則 PDF

Clay 於 2026 年 9 月 11 日公告稱 Navier–Stokes 問題「apparently been settled」，表示將依獎項規則評估、程序刻意不倉促；這仍屬審查狀態，並非正式認定或授獎。Clay 公告

左右兩欄分別列出 Lean 核心檢查能確認的證明項與推理，以及需要人工核對的命題對照、文字對應和獨立重現。
機械檢查能確認既定命題下的推理，命題是否忠於論文仍須人工比對。

三、機械驗證為何不能單獨完成研究驗收？

機械檢查只能在既定定義、假設和定理敘述下驗證推理；研究驗收還要確認這些輸入本身就是原文要表達的內容。 翻譯、模型或人工都可能在這一步改變問題。

Lean 由精簡的核心檢查器（kernel）依型別理論規則檢查證明項（proof term），自動化策略產生的證明也須通過這項檢查，Lean 官方語言參考說明了這個範圍。kernel 不會判定論文敘述是否和程式中的 theorem 一致。

這屬於形式化工作的邊界，與工具缺陷無關。形式系統只能驗證收到的定義與命題；若輸入寫成另一個更容易證明的問題，系統仍會正確地驗證它。研究者因此要核對：假設是否改變、全稱或存在量詞是否保留、結論是否縮窄、常數是否依賴額外參數，以及前置引理是否提供原文所需的條件。預印本指出的壓力通量界限差異，就涉及右側項目與時間量詞。

多代理系統的投入規模也不能直接代表貢獻。OpenAI 稱約一萬個代理同時運作，約 88 小時後提出解答，Lean 形式化與檢查另花約 17 小時。要判斷代理數量是否帶來差異，需比較不同代理規模、相同算力的單代理組及工具配置，並公開成功率、失敗案例、評分方式，以及由誰選定形式化命題、人工是否介入修改；少了這些，重現與歸因都無從判斷。

四、研究與技術分析如何留下可重現的檢核紀錄？

把來源、命題、程式版本、執行環境、複核者與未解疑點記在同一份紀錄中，並保留可重跑的指令和結果。 這樣下一位研究者才能判斷檢查覆蓋了什麼，也能從相同起點重做。

  1. 固定來源版本：保存論文版本、發布日期、正式問題描述與程式碼 commit，不只留下會更新的首頁連結。
  2. 對照命題：為每個核心主張記錄論文頁碼或方程式、形式化定理名稱、定義與假設，標出量詞、條件和結論是否一致。
  3. 封存執行環境：列出 Lean 版本、依賴套件版本、建置指令與檢查輸出，讓其他人能按相同條件重跑。
  4. 安排獨立複核：記下複核者檢查了哪些引理、是否有不同專長，以及他們提出的問題和回覆版本。
  5. 公開尚未完成的部分：清楚標示沒有對照的主張、無法重現的步驟、目前爭議和下一次更新方式。

操作上可先挑一項最關鍵的主張做小範圍驗收：驗證命題、最重要的中間引理與程式依賴，再請未參與原始推導的人照紀錄重做。小範圍就出現不一致時，先釐清定義或假設，再決定是否把整套結果納入產品、報告或決策。

複核時還要把「重跑成功」拆成可追問的步驟：先從乾淨環境取得指定 commit，再依鎖定的套件版本建置，記下完整指令、輸出與耗時。若結果仰賴特定設定或公理，也應列出名稱與用途，確認沒有把待證結論直接放進前提。核心命題可另外檢查邊界案例，例如條件取等號時是否仍成立、移除某個假設時哪一步失效。

重現紀錄要連失敗一起保存：失敗的建置與檢查要註明錯誤來自環境設定、依賴版本或證明項；修正過命題或程式，就保留前後版本與變更理由。後續複核者因此能分辨差異來自程式版本、環境還是命題本身，也知道哪些疑點已處理、哪些仍未解決，一次成功執行不會被誤當成整份研究已完成驗收。

由左至右呈現封存論文與程式版本、對照定理與程式、記錄執行環境、重跑檢查、獨立複核及登錄未解問題的流程。
固定來源與執行環境，再由獨立研究者重跑，才能留下可追查的驗證紀錄。

Bastounis、Circelli 與 Hansen 在 2026 年預印本中說明，他們不判定 OpenAI 自然語言證明是否正確，分析範圍是轉譯到 Lean 時可能出現的差異。

五、讀者判斷 AI 研究成果時，應看哪些證據？

分開看模型產出、形式化檢查、同行審查與社群接受，並確認每個狀態有哪一份可查證的證據支持。 一篇公告可以提出重要結果，正式接受仍要看獨立審查和相關機構程序。

讀者可以先問四個問題：原始問題是否完整公開？論文中的核心定理能否對到程式中的同一命題？有沒有不依賴提出方的專家檢查並公布理由？其他研究者能否拿到固定版本與環境，重做關鍵步驟？讀者不必親自讀完龐大的證明，靠這四題就能判斷目前公開資訊支持到哪一層。

套回這起事件：OpenAI 已公布解答、論文與 Lean 形式化，研究者預印本提出了可核對的疑點，Clay 仍在評估程序中。

從 AI 研究到企業技術分析都適用同一原則：對外結論要和驗證範圍相稱。遇到 AI 產出的研究結論，先記下原始主張與版本，再核對程式實際檢查的內容，最後確認是否有獨立複核與重現紀錄。少了其中任何一層，就把成果標示為尚待驗證，並清楚寫出還缺哪項證據。

  • Lean 通過檢查，表示形式化命題在指定系統中的推理通過檢查，不會自動證明翻譯忠實。
  • 對照論文與程式時，優先查假設、量詞、結論強度、依賴引理和版本差異。
  • AI 研究成果的可信度還要看獨立審查與可重現紀錄；代理數量或算力不能單獨證明因果貢獻。

常見問題

Q1：Lean 驗證通過，代表數學證明正確嗎？

它表示 Lean 檢查器接受程式中指定的命題及其證明項。仍需確認命題是否符合研究問題，以及程式是否忠實對應論文論證。

Q2：預印本指出論文和程式不一致，等於整份解答已被推翻嗎？

不等於。預印本提出的是可檢查的差異與分析，仍需其他研究者核對，也要看差異是否影響後續推論與最終主張。

Q3：一般讀者怎麼判斷 AI 研究目前可信到什麼程度？

查看原始論文、程式版本、形式化命題、獨立審查和重現紀錄，並把「已提出」「已機械檢查」「已同行審查」分別標示。