東海大學 智慧計算暨應用數學系 Department of Smart Computing and Applied Mathematics

在大眾的想像裡，數學研究似乎有一條非常清楚的路： 提出問題、找到證明，然後問題宣告解決。

但真正的研究並不是在證明最後一行寫下來的瞬間就結束。 一個結果還需要被重新閱讀、驗證、說明， 並交給其他研究者檢查與理解。

Terence Tao 在談論 AI 時代的數學研究時， 將數學工作的流程區分成證明生成、證明驗證、 說明、同行接受以及後續消化等不同階段。 這也提醒我們： 「得到一個證明」和「建立一個值得信任的數學結果」並不是同一件事。

數學證明的錯誤不一定長得像一個非常明顯的算錯答案。

有時候，問題可能來自一個沒有說清楚的假設； 有時候是某個極端情況沒有被納入； 也可能是在一段很長的推導中， 某一步被作者認為「顯然成立」， 但實際上仍需要額外條件。

長篇公式中也可能出現更日常的問題： 打字、複製、修改長公式時產生筆誤， 都可能讓錯誤藏在數十行計算之中。

即使作者已經仔細檢查自己的工作， 數學研究仍然非常依賴其他研究者的閱讀與檢驗。

論文可能先以預印本形式公開， 接著投稿期刊， 由熟悉該領域的研究者進行審閱。 而論文正式發表後， 其他數學家仍可能在後續研究中重新使用、推導或質疑其中的結果。

因此，同行審閱很重要， 但它並不是一張「百分之百永久正確」的保證書。

傳統的數學論文，是寫給人閱讀的。 因此其中經常會省略某些被認為熟悉或容易完成的步驟。

形式化數學則走向另一個方向： 將定義、條件與推理步驟寫成電腦可以逐步檢查的形式。

Lean 等 Proof Assistant（證明助理） 能依照形式化系統中的規則檢查推理是否成立。 它不是單純「看起來像對的」， 而是要求每一個被形式化的步驟都能通過系統檢查。

Tao 曾公開分享將自己的數學內容轉成 Lean 形式化證明的經驗。

在一個與對稱不等式相關的案例中， 原本紙本論證裡相對精簡的微積分步驟， 在形式化之後需要被拆成大量更細的邏輯與計算步驟。

這個差異非常有意思。 人類數學家可能會把某些內容視為熟悉的「常規計算」， 但電腦不會因為某件事情看起來顯然而直接跳過。

當生成式 AI 開始參與數學研究， 一個新的問題也出現了： 如果 AI 可以快速生成一段看起來非常合理的證明， 我們應該相信它嗎？

關鍵在於， 生成內容、形式驗證與理解數學意義，是三件不同的事情。

而在人類這一端， 還有另一個不可忽略的問題： 即使一份形式化證明通過驗證， 我們仍然需要理解它為什麼重要、 其中真正的新想法是什麼， 以及它如何與其他數學知識連結。

現在，我們可以回到最開始的問題。

如果一份證明有 100 頁， 我們真的能確定第 73 頁完全沒有問題嗎？

數學給出的答案並不是： 「因為數學家永遠不會犯錯。」

相反地， 數學之所以能建立高度可信度， 正是因為研究者知道人會犯錯， 所以證明必須能被重新閱讀、質疑、驗證、修正， 並在必要時透過新的工具接受更細緻的檢查。