AI解決數學難題的時代來臨：人類研究者的價值何在？

5年時間，數學家陳大偉和Quentin Gendron一直在解決代數幾何學中的一個難題。他們試圖證明一個關於微分的定理，但遇到了意外的障礙：他們的論證依賴於數論中的一個奇怪公式，而他們無法解決或證明它。最終，兩人只能將想法以猜想而非定理的形式發表論文。

陳大偉最近花了數小時讓ChatGPT嘗試解決這個仍未解決的問題，但沒有成功。然而上個月，在華盛頓特區的一次數學會議招待會上，陳大偉偶遇了著名數學家Ken Ono。Ono最近離開維吉尼亞大學，加入了由他的學生Carina Hong共同創立的AI新創公司Axiom。

陳大偉向Ono描述了這個問題，隔天早上，Ono就帶來了解答——由他的新創公司的數學解題AI「AxiomProver」提供的證明。

AI發現人類遺漏的關聯

「一切都自然而然地解決了」，陳大偉說道。Axiom的AI工具發現了這個問題與19世紀首次研究的數值現象之間的關聯，然後設計出證明，並自我驗證。「AxiomProver發現的是所有人類都遺漏的東西」，Ono表示。

這個證明是Axiom系統在最近幾週內解決的多個未解數學問題之一。雖然AI尚未解決數學領域最著名（或最有價值）的問題，但它已經找到了困擾不同領域專家多年問題的答案。

Axiom的方法結合了大型語言模型和名為AxiomProver的專有AI系統，該系統被訓練來推理數學問題並得出可證明正確的解答。2024年，Google用名為AlphaProof的系統展示了類似的概念。Hong表示，AxiomSolver融合了幾項重大進展和更新的技術。

超越文獻搜尋的創新

Axiom的系統不僅僅是一個普通的AI模型，它能夠使用名為Lean的專業數學語言來驗證證明。這使得AxiomProver不只是搜尋文獻，而是能夠開發出真正新穎的問題解決方法。

AxiomProver生成的另一個證明展示了AI完全獨立解決數學問題的能力。該證明解決了「Fel猜想」，涉及代數中數字排列的數學表達式。值得注意的是，這個猜想涉及100多年前傳奇印度數學家拉馬努金筆記本中首次發現的公式。在這種情況下，AxiomProver不僅填補了拼圖的缺失部分，更是從頭到尾設計出完整的證明。

「即使作為多年來密切關注AI數學工具演進並親自使用它們的人，我也覺得這相當驚人」，熟悉Fel猜想和Axiom技術的哈佛商學院教授Scott Kominers說道。「不僅僅是AxiomProver成功完全自動化地解決了這樣的問題並即時驗證，這本身就很了不起，它產生的數學的優雅和美感也令人讚嘆。」

數學之外的商業價值

Axiom開發的技術可能在高等數學世界之外也很有用。例如，同樣的方法可以用於開發對某些類型網路安全攻擊更有抵抗力的軟體。這將涉及使用AI來驗證程式碼是可證明可靠和值得信賴的。

「數學確實是現實的偉大測試場和沙盒」，Axiom執行長Hong說道。「我們確實相信有很多具有高商業價值的重要應用案例。」

對於華人世界的科技產業來說，這項技術進展特別值得關注。台灣的半導體產業、香港的金融科技領域，以及新加坡的智慧城市發展，都可能從數學證明的自動化中受益。特別是在密碼學和資訊安全領域，這種技術可能為亞洲的科技競爭力帶來新的優勢。

研究典範的轉變

Ono認為AI生成的陳-Gendron猜想證明顯示了AI現在如何有意義地協助專業數學家。「這是證明定理的新典範」，他說。Ono希望AxiomProver不僅能協助數學家工作，還能揭示關於新發現如何產生的更根本的東西。「我有興趣嘗試理解是否可以讓這些『啊哈時刻』變得可預測」，他說。

見證自己猜想被Axiom解決的陳大偉對AI對其領域的影響也感到樂觀。「數學家在計算機發明後並沒有忘記乘法表」，陳大偉說。「我相信AI將作為一種新穎的智能工具——或者更恰當地說是『智能夥伴』——為數學研究開啟更豐富、更廣闊的視野。」