人類數學天才解不開的難題，AI「Gauss」(高斯) 三週搞定，數學家也要面臨工作危機了嗎？

今年 7 月，澳籍華人數學家陶哲軒（Terence Tao）與 Alex Kontorovich 提出的一項數學挑戰，歷經 18 個月 仍只取得初步進展；然而，一個名為 Gauss 的 AI 系統卻在短短三週內完成了解答，令學界與 AI 界震撼不已。

這個 AI 來自一家名為「Math」的人工智慧新創公司，據介紹，Gauss 是第一個能協助頂尖數學家進行形式化驗證的 自動形式化（Autoformalization）Agent。

形式化（Formalization）是指將人類撰寫的數學內容，轉換成電腦可讀、可驗證、無歧義的語言，並透過電腦來驗證其正確性。這項工作原本仰賴高度專業的形式化專家，可能需時數年才能完成。

而 Gauss 在這次的應用中，自動產生了約 25,000 行 Lean 語言的程式碼，包含數千個定理與定義，並成功形式化了「複分析（Complex Analysis）」中的關鍵缺失結果。這是陶哲軒與 Kontorovich 卡關的地方，AI 最終成功突破。

這個規模的形式化過去通常需多人、跨年進行；相比之下，Lean 的標準數學庫 Mathlib 花了 8 年、由 600 多位貢獻者完成，目前約有 200 萬行程式碼、35 萬個定理。

為了支撐 Gauss 的大規模運算，Math 團隊還與 Morph Labs 合作，打造出 Trinity 環境基礎架構，能同時支援數千個並行 Agent、每個 Agent 各自運行 Lean 環境，整體佔用數 TB 記憶體資源，是個極具挑戰的系統工程。

Math 團隊表示，這種系統未來將可讓大型數學專案所需時間大幅縮短，甚至讓形式化程式碼量在未來 12 個月內增加 100 至 1000 倍。這將是「可驗證的超級智慧」與「通才型 AI 數學家」的試煉場。

陶哲軒本人隨後也在 Mastodon 上發表對形式化與 AI 工具的看法。他認為，AI 的工作方式與人類不同：AI 可能會成功完成「明確目標」（如完成某定理的形式化證明），卻跳過了「隱含目標」——像是幫助建立合作機制、訓練新手、整理更好理解的證明結構、補充可納入 Mathlib 的子命題等。

他提醒，未來的數學專案應更清楚定義所有目標，避免 AI 完成「指令」卻犧牲了原本人類在過程中自然建立的價值。

Math 公司創辦人 Christian Szegedy 是 2015 年 Batch Normalization 論文的共同作者之一，這篇論文在 ICML’25 獲得「時間檢驗獎」，至今引用數超過 6 萬次，是深度學習史上的關鍵技術之一。

這項技術解決了深層神經網路難以穩定訓練的問題，為後來的大規模模型鋪路。如今，他轉向數學 AI 領域，再度帶來新突破。

許多網友對 Gauss 的成果表示驚嘆，但也紛紛呼籲 Math 公司盡快公開技術細節與完整論文。目前官方尚未發布完整技術報告，是否會開源還有待觀察。