數學嚴謹性至關重要，但數位化證明是否做得太過火了？

背景

這篇文章探討了數學界在追求嚴謹性上的歷史演進，特別是當前將數學證明全面「數位化」並轉譯為 Lean 等電腦語言的趨勢。隨著微積分從直覺走向形式化，數學家們正處於一個轉折點：究竟該擁抱能自動驗證真偽的電腦證明，還是擔心過度的形式化會扼殺數學發現所需的直覺與創意。

社群觀點

在 Hacker News 的討論中，社群對於「嚴謹性」的本質與必要性展開了激烈的辯論。支持者認為，嚴謹性始終是數學的靈魂，過去數學家之所以不夠嚴謹，往往是因為受限於工具而非主觀意願，自動化證明工具正好填補了人類大腦容易出錯的空缺。然而，反對者則提出警示，認為數學的核心價值在於「理解」而非單純的「證明」。如果一個證明是透過電腦窮舉數百萬種情況而得出的，雖然它在邏輯上無懈可擊，卻無法為人類提供深刻的洞察力或啟發新的數學分支。

部分留言者將數學的形式化比作軟體工程中的組合語言。他們指出，現代數學教育往往過於強調底層的定理與引理推導，卻忽略了高層次的抽象概念與直覺建立，導致數學變得難以親近。這種「低階語言」的傾向雖然保證了正確性，卻可能讓數學家在繁瑣的細節中迷失，甚至耗費數十年才能到達研究前沿，進而壓抑了革命性的創新。此外，也有觀點擔憂數學數位化會導致「想法僵化」，就像作業系統為了相容性而保留過時的標準，數學可能也會因為過度依賴特定的數位框架，而難以重新想像更優雅的基礎架構。

有趣的是，討論中也觸及了數學的社會屬性。有評論者認為數學本質上是一種社會建構，是人類透過故事、技術與關係來滿足好奇心的過程。如果將證明完全交給機器，數學將失去其作為人類智力活動的意義。但另一派意見則樂觀地認為，自動化證明就像計算機的出現一樣，只是將枯燥的驗證工作抽離，讓數學家能轉型為「啟蒙者」或「吟遊詩人」，專注於闡述動機、解釋直覺以及建立理論與現實應用之間的橋樑。

最後，針對當前 AI 發展的現況，社群也討論到形式化證明在過濾「AI 垃圾論文」上的潛力。隨著學術期刊被大量錯誤百出的 AI 生成內容淹沒，要求論文附帶可驗證的數位證明，或許是維護學術誠信的必要手段。同時，將歷史文獻形式化也能為未來的 AI 訓練提供更高質量的數據，讓機器在邏輯推演上更加穩固。

延伸閱讀

• William Thurston 的論文《On Proof and Progress in Mathematics》：探討數學進步不應僅視為定理的累積，更在於人類理解力的提升。
• Aristotle (harmonic.fun)：一個能將數學論文轉譯為 Lean 程式碼並進行推理的大型語言模型工具。
• Lisp 64k 與算術邏輯：探討如何從最基礎的列表結構（Nothing）中建構出算術與邏輯系統。