綠燈亮了，題目對上了嗎：一份AI數學證明留下來的三層功課

先把時間點放回原處。2026年9月，OpenAI公布Navier–Stokes方程的長篇解答與Lean形式化；10月6日，三位研究者Alexander Bastounis、Fabian Circelli與Anders C. Hansen發布預印本，指出論文與程式內容之間存在若幹差異。半個多月後，討論沒有停在「證明對不對」，而是轉向一個更實際的問題：外人要怎麼檢查一份AI產出的研究成果。

Lean通過了，數學家為什麼還在問

很多人的直覺是：Lean既然逐步檢查過，證明應該就可信了。但Lean檢查的是輸入程式所陳述的命題與推理，它不會自行判斷這個命題是否忠實對應論文文字或原始研究問題。

預印本提出的疑點正是落在這一層。研究者比較論文的自然語言證明與Lean程式後指出，一項估計在論文中使用輸入函數的第m+4階導數，形式化結果卻要求第m+5階；另一項壓力通流估計也有額外依賴。程式加強了前提條件，結論的適用範圍就可能跟著縮小。

要留意兩件事。研究者的分析針對的是論文敘述與形式化內容的對照，並未宣稱Lean核心檢查器失效；而這份預印本本身也還在等待同儕與數學社羣檢視，局部疑點不能直接當成整份證明已被推翻。OpenAI則說明，形式化與檢查是在模型提出解答之後才完成，這屬於提出方對流程的描述，讀者本來就該與論文、程式碼及獨立審查分開判讀。

三層檢核：從題目到重現

判讀一份AI數學成果，可以把問題拆成互相銜接的三層。任何一層缺資料，都只能標示為尚待確認。

第一層是問題與命題。研究聲稱的結果，是否符合原始問題及其完整條件？Navier–Stokes問題的初始條件、外力限制或解的範圍不同，都會形成不同命題。核對時應逐項比對論文定理與Clay數學研究所的正式問題描述，不能只看「解決千禧年問題」這類摘要標題。

第二層是命題與程式。Lean實際檢查的定理，是否就是論文要證明的命題？讀者可以先找論文的定理、引理與方程式編號，再到程式碼中找對應的theorem或lemma，逐項確認前提、變數範圍與結論。前述m+4與m+5的差異就屬於這類對照：不必先讀懂整個程式庫，挑出核心主張依賴的引理，查程式是否證出相同界限即可。

第三層是論證與重現。不同研究者能否理解證明、找出疑點，並在公開環境中重做？這需要獨立審查紀錄、可執行環境與重現步驟。值得注意的是，Clay的獎項規則要求解答先刊於合格出版物，刊登後還須達到數學界普遍接受，並經至少兩年嚴格檢視，才進入獎項評估。Clay在9月11日的公告中稱此問題「apparently been settled」，但也強調程序刻意不倉促；這仍屬審查狀態，並非正式認定。

機械驗證的邊界

機械檢查能確認的是既定命題下的推理。命題是否忠於論文，仍須人工比對定義、符號、假設與量詞的轉換。換句話說，編譯通過無法自行辨認語意落差，這正是這次爭議最有教育意義的地方。

這個原則也適用於AI研究的其他場景。一份輸出看起來完整，甚至能在工具中成功執行，也不代表它回答了原本的問題。無論是程式分析還是技術決策，可驗證性都需要分層檢查，並保留讓其他人重做的紀錄。這與先前開發者討論AI讓寫程式能力退化的脈絡有點相似：工具的輸出越順手，人這一端的檢核功夫反而越不能省。

目前這份證明的最終評價還在數學社羣手裡。但「檢查通過的究竟是哪個命題」這個問法，已經足夠讓每一次AI成果發表，多出三層值得追的線索。