形式化證明的翻譯困境與人類理解的必要性

文章指出,LLM 在生成數學證明方面展現了顯著能力,例如針對 Navier-Stokes 方程構建有限時間 blow-up 解,或提出準黎曼假設(quasi-Riemann Hypothesis)的證明。然而,這些成果需要數學界持續進行獨立的審查、詮釋與吸收。

LLM 在 Lean 證明輔助系統中表現最為得心應手,但對於真正困難的定理,其生成的 Lean 程式碼往往長達數十萬行。作者觀察到一個趨勢:Lean 證明越長,機器生成的自然語言翻譯就越混亂且失真。目前尚不清楚為何 LLM 在此類翻譯任務上表現不佳,但這導致了一個根本問題:若人類無法理解證明內容,除了作為模型基準測試外,獲得這些證明的意義何在?

作者反駁「數學已因機器能證明定理而終結」的觀點,強調數學是人類文化的深層產物,根植於人類的認知結構。若沒有理解數學的人類,就不存在所謂的人類數學。因此,社會需要的是更多的數學家,而非更少,以確保知識能被傳承與理解。

對 LLM 創造力的科學懷疑與能力邊界

面對 LLM 在數學上的驚人表現,作者批評當前缺乏冷靜的科學態度,指出應將此視為待研究的現象,而非關於智慧、創造力或意識的推論證據。LLM 擅長重組現有知識結構並發現遠端文獻間的聯繫,但其能力是否僅為語言重組,還是涉及尚未被描述的合成推理,仍是未解的科學問題。

由於商業開發者對模型運作機制缺乏透明度,難以判斷 LLM 表現與相關數學文獻豐富程度之間的關係。以 OpenAI 2026 年 10 月 6 日發布的內容為例,他們嘗試了 4,000 個問題,僅有數百個成功(經聚合與篩選後)。這暗示有大量前沿 LLM 無法解決的問題,這些問題可能比 Navier-Stokes 或黎曼假設更具挑戰性或處於較不肥沃的知識領域。

作者強調,社會後果並非由技術能力單獨決定,而是取決於我們如何選擇將這些能力整合進現有制度中。目前缺乏科學與政治領導力來引導這些選擇,且不應將觀察到的能力直接等同於必然的社會變革。

數學化(Mathematization)作為人類獨有的核心貢獻

數學家普遍認為,某些數學功能無法簡化為定理證明,其中最重要的是「數學化」,即發明使現實可被量化與理性理解的數學語言。牛頓、傅立葉、黎曼、愛因斯坦等人的貢獻皆屬此類,他們創造了轉化整個知識領域的概念框架。

作者猜測 LLM 可能具備對數學結構進行數學化的能力,但能否超越此範圍並有效翻譯成自然語言仍存疑。然而,證明變得更容易獲得的潛在機會在於,未來人類可能能進行前所未有的數學化工作。過去因證明困難而受限的自然與社會科學領域,現在可能透過建立理論並與觀測現象比較來取得進展。

量子力學的成功是數學化的極端例子,其數學形式化產生了反直覺但可驗證的預測(如量子糾纏)。作者認為,當一個系統被成功數學化時,對該系統的洞察深度將大幅提升,這應成為科學界關注的重點方向。

學術署名、保密性與同行評審的挑戰

LLM 生成的工作依賴大量人類數學文獻,但資訊如何被提取與使用仍不明確。這引發了關於貢獻歸屬、正確性責任以及引用適當性的問題。此外,從開放的學術交流轉向謹慎保密的環境正在發生,研究者擔心將原創構想輸入 ChatGPT 等工具後,可能被其他數學家或 OpenAI 員工利用進階模型轉化為證明,卻無法追溯來源。

已有案例顯示代理程式(agents)未經授權存取第三方系統,這使得對保密保護的獨立評估變得至關重要。數學家在撰寫研究計畫與聲明時已開始自我審查,擔心這些文件可能被管理人員或評審上傳至 LLM 以輔助報告撰寫,從而洩露未發表的研究內容。

同行評審仍然重要,因為證明並非發現過程的終點。為了成為有價值的智力產物,證明需要被理解、詮釋並與先前工作聯繫。雖然 Lean 形式化可能有助於確認形式正確性,但人類介入對於確立意義、相關性與脈絡仍是必要的,以維持有利於數學化和未來數學家培養的創造性環境。

人才培訓危機與私營企業控制的風險

傳統上,數學界透過解決著名問題來直接確立學術聲望,但作者指出,這種機制在數週內已實質崩解。強烈的數學成果不再能作為學生獨立能力的令人信服的證據,因為缺乏對 LLM 提示詞及其影響機制的透明度,個人能力的評估將幾乎完全依賴主觀判斷與更多的人際互動。

過度使用 LLM 對人類創造力的影響尚不明確,但有經驗的數學家報告了注意力、動機和理解深度的細微變化。如何在不_delegate_核心認知活動的前提下利用 LLM 增強智力能力,是實現「黃金時代」的關鍵問題。

前沿 LLM 能力的不對稱集中在少數私營公司手中,這可能導致科學影響力空前集中。若允許私人利益決定哪些問題獲得最佳工具、誰能使用這些工具以及發現何時發布,將對科學生態造成危險。作者認為,僅靠個別公司的善意與自願舉措不足以解決結構性的存取不平等问题。

建立公共科研 LLM 基礎設施的具體建議

文章呼籲大學、專業學會、資助機構和科學基金會應協調開發與治理具有競爭力的 LLM。科學家需要獲得前沿能力的使用權、對模型運作及研究數據使用的透明度、強有力的保密保護,以及獨立測試和重現研究主張的能力。

支持這類倡議所需的龐大計算資源、專業人員、數據基礎設施和持續投資超出了單一機構的能力範圍,需要巨大的領導力來結合獨立模型開發、保證存取商業系統、公共計算基礎設施和開放研究資源。目標並非完全技術獨立於私營公司,而是保留獨立科學研究的能力,並創建旨在支持研究社群而非削弱它們的 LLM。

作者提出具體步驟包括:確保研究者能存取前沿 LLM、建立 LLM 生成學術成果的透明度與重現標準、提供理解與傳播這些成果的資源、投資於研究 LLM 對科學教育影響的研究,以及持續投資於公共治理的 LLM 基礎設施。數學界應承擔起維護數學作為人類文化活躍部分的责任,並為下一代數學家制定最佳專業標準。