Math Inc. 剛剛推出 Gauss ，一個 AI 系統，它僅用 三週 就解決了一項名為 強質數定理（Strong Prime Number Theorem, PNT）的複雜數學定理 —— 而頂尖數學家們之前花了 18 個月 仍在掙扎中。Math Inc. 團隊推出 Gauss，是一個首創的 自動形式化代理（autoformalization agent），用於協助數學專家進行形式驗證。透過 Gauss，完成了由費爾茲獎得主 陶哲軒（Terence Tao） 與 Alex Kontorovich 在 2024 年 1 月提出的挑戰 ，在 Lean（GitHub） 中形式化 強質數定理（Strong Prime Number Theorem, PNT）。
使用 Gauss，產出了 約 25,000 行 Lean 代碼，包含超過 1,000 個定理與定義。這類規模的形式化證明在歷史上常是重大里程碑，通常需多年努力才能完成。歷來最大型的單一形式化專案通常需要十年以上、堪稱研究生涯巔峰的成果，也僅比這大一個數量級（約 500,000 行代碼）。而 Lean 的數學標準函式庫 Mathlib 則大兩個數量級，擁有 約 2,000,000 行代碼、35 萬個 Lean 定理與定義，並由 600 多名貢獻者歷經 8 年建構完成。
內容摘要：
- Gauss 完成了由知名數學家 陶哲軒（Terence Tao） 與 Alex Kontorovich 在 2024 年提出的強質數定理形式化挑戰。
- 人類專家僅在該挑戰上取得「中期進展」，數學界在 18 個月後（2025 年 7 月）才完成較簡化的 中等版本（Medium version）。
- Gauss 可自主連續工作數小時，並生成 25,000 行經過驗證的數學程式碼，其中包含 1,000 多個相互關聯的證明與定義。
- Math Inc. 計劃在未來 12 個月內 將數學代碼量擴展 100 到 1,000 倍，以此作為訓練數據，推動「機器數學多面手（machine polymaths）」與「驗證型超級智慧（verified superintelligence）」的發展。
重要性：
複雜數學是 推理的基礎，而 AI 正快速掌握這一領域，這是 系統能創造新思想並加深我們對世界理解 的最強信號之一。隨著 Gauss 的突破，以及 Google、OpenAI 等 在國際數學奧林匹亞中獲得金牌，AI 在數學上的加速正在飛速發生。
Gauss 展現了形式化在未來如何擴展。目前，它仍依賴數學家提供的自然語言框架，並需要高階專家的指導與開發。預期未來版本的 Gauss 將更具能力與自主性。Math Inc. 團隊將開始部署這項技術，讓數學家與證明工程師能實際使用。目前Math Inc. 團隊正與部分數學家接洽，進行封測（beta testing）。你可以在此註冊 Gauss 早期使用權。若你有關於自動形式化的雄心計劃，歡迎與Math Inc. 團隊聯繫。（👉聯絡網址：https://www.math.inc/）
- 如果你對內容有共鳴、想分享想法，
- 歡迎在下方留言互動 💬 你的支持就是我持續寫作的動力！
- 📮 也歡迎來信交流：childbenefits@gmail.com
