一封由約一千名數學家聯署的公開信已發布,表達對人工智慧在數學研究中日益增長作用的擔憂。簽署者警告,過度依賴 AI 生成的證明可能威脅該領域的準確性與獨立可驗證性。此舉具重大意義,因為純數學過去被認為對自動化具有抵抗力,這標誌著基礎知識生產方式的轉變。
信中強調潛在風險,包括研究優先級可能偏向適合 AI 處理的問題,以及研究人員面臨經濟替代的壓力。此外,信中指出參與與 Anthropic 和 OpenAI 等主要 AI 公司相關活動,可能會對研究人員的聲譽產生負面影響。最後,驗證負擔正從人類直覺轉向 Lean4 等正式系統。
事件背景
數學中的形式化驗證是指使用電腦系統以絕對確定性來證明數學命題的正確性,這與概率性的 AI 輸出不同。Lean4 等工具最近使 AI 能夠生成可由這些正式系統嚴格檢查的證明,從而改變了定理證明的格局。
社群觀察
社群情緒反映了對經濟替代的焦慮,有評論將此情況與程式設計師面臨的類似挑戰進行比較。讀者還指出,無論人類意見如何,數學最終會自我驗證,同時有人強調了關於產業對學術聲譽影響的「霸凌」面向。



