數學家的“消失”與一場新的AI革命

你有沒有想過，有一天，全世界最有錢的人，會瘋狂地追逐同一種人——數學家？

這不是科幻小說的開場白，而是眼下正在真實上演的一幕。過去兩年，全球頂尖大學里，許多數學教授正從課堂上“神秘消失”，悄然進入一家家剛成立幾個月的初創公司。它們像雨后春筍般冒出來，而背后，站著OpenAI、谷歌這樣的巨頭，還有嗅覺最靈敏的風險資本。這個時刻太特殊了——數學被當成了提升人工智能的“秘密配方”，而AI，又反過來可能徹底改變數學本身。一位親歷者形容這個時刻，就像佃農第一次在田間撞見內燃機，起初是震撼，然后是狂喜：原來換一個工具，我們能耕出完全不同的天地。

我就是帶著這種好奇，在4月走進了硅谷帕洛阿爾托。那里有兩家公司特別引人注目：一間叫Axiom Math，另一間叫Harmonic。它們門面毫不起眼，會議室卻以高斯、阿達·洛夫萊斯這樣的數學巨匠命名。它們正在做的事，聽起來像是要讓數學擁有“自我驗證”的能力。而它們的賬上，已經流入了投資人砸下的數億美元。

這筆錢的邏輯，得從數學家正在經歷的這場集體“出走”說起。故事的核心人物之一，叫Ken Ono。2025年，他從弗吉尼亞大學請假，加入了Axiom Math。他告訴我，去年5月的那一刻，他一度在為自己“科學身份”的消散而悲傷。教授不做了，去一家連產品都還沒影的小公司，這在傳統學術圈里幾乎是一種背叛。

可轉變，發生在他和另一家叫Epoch AI的公司接觸之后。Epoch AI請他幫忙設計一批超高難度的數學題，用來測試AI的解題能力。Ono一開始可能只是抱著考考AI的念頭，但當他親眼看到這些模型一步步推開數學的深門時，他發現自己大大低估了對手。用他的話說：“讓它們跑了一陣子后，我意識到，也許那個佃農撞見內燃機的時刻真的來了——我們或許能借助這些技術，做到遠超從前的事。”

Ono的頓悟，并不是個案。Axiom Math是過去兩年間冒出的那一串新公司里的一個代表。它們的目標出奇地一致：打造一種不但能“做數學”，還能“自證正確”的人工智能。這里的關鍵詞，是“證明它做對了”。

這聽起來可能有點繞。我們不妨先停下來問一句：為什么數學領域會突然變成AI落地的一塊理想試驗田？

想想你熟悉的ChatGPT。你可以把它想象成一個世界上最龐大的圖書館管理員，它讀過人類公開的、幾乎所有領域里的書和對話。你問什么，它幾乎都能給出一個像模像樣的答案。但問題也藏在這里：這個管理員會不會在深夜犯困時，把《三國演義》和《三國志》里的情節搞混，然后編出一段看似合理、實則漏洞百出的故事？答案是，它不但會，而且經常這么干。在需要精確、不可篡改的領域，比如醫療診斷、工程計算、法律條文，或者非常前沿的科學研究上，這種“不可靠”是致命的。

但數學不同。數學是唯一一個你可以用一套冷冰冰的規則，百分百檢驗“對還是錯”的領域。Ono有一個很精妙的比喻：“ChatGPT就是那個圖書館員，你不可能從它那里找到它沒讀過的東西，但你愿意讓你的圖書館員來給你開顱做神經外科手術嗎？”答案顯然是不。人類需要先讓圖書館員配上一套絕對嚴苛的鑒定眼鏡，而數學的真理體系，剛好就是那副可以被機器戴上并且自動運行的眼鏡。

這副“眼鏡”其實幾十年前就已經有了雛形。數學家們創造了一種叫“證明助手”的編程語言。目前最流行的那一個，名字叫Lean。把數學證明翻譯成Lean語言，就像把一篇手寫的潦草草稿，重組為一段語法嚴格到容不下一個標點錯誤的代碼。接著，計算機就可以逐行檢查這段代碼，并給出一個不容辯駁的結論：要么對，要么錯，沒有“差不多”。

在過去，這個翻譯工作由人來完成，極度耗時。一篇中等難度的數學證明想變成Lean能讀懂的形式，往往需要一個小團隊花上好幾個月。但現在，Axiom Math和Harmonic這樣的公司想干的事，就是教AI學會這門翻譯的功夫，甚至更進一步——直接生成自帶驗證標記的數學推演。這就相當于，以前需要一個人類抄寫員一個個字母去謄抄古籍，現在突然有了一個能高速掃描并自動校對的智能掃描儀。

我走進Axiom Math的辦公間時，這種“加速”的興奮感幾乎寫在每個人的臉上。辦公室門口就是斯坦福大學，創始人是Ono曾經的學生，Carina Hong。幾步之外，Harmonic的團隊也正朝著同一個方向前進，目標是用數學構建一種“數學超級智能”，產出可驗證的結果。在它們不張揚的門禁背后，資金正以前所未有的密度匯入。如果你只看它們簡樸的工位和起了數學家名字的會議室，很難想象這些公司已經拿下了數以億計的美元。投資者賭的，并不僅僅是一個工具，而是一條全新的道路——你不再需要相信AI的“黑箱判決”，因為數學驗證會把每次推理的每一環，都變成陽光下的透明鏈條。

這個邏輯反過來，又會反哺AI本身。讓AI學會用Lean這樣的語言去證明自己，相當于逼迫它養成一種內化的、無法作弊的嚴謹習慣。這比起今天大語言模型那套“猜下一個詞”的機制，是一種本質上的升維。研究者們推測，當模型為了通過嚴格的形式驗證而不得不調整自身時，它內部的表征，可能會更接近一種真正意義上的“理解”，而不只是高級模式匹配。

不過，這些終究還是發生在大約2025到2026年間的早期故事。我在硅谷看到的一切，都在一種“奔跑中組裝”的狀態。數學家和工程師們坐在白板前，反復爭論著同一個證明的多種表述。墻上貼著的時間表，常常在一周內被刷新掉。他們面臨的挑戰同樣巨大：現有的定理驗證系統，還遠遠覆蓋不了前沿數學那些常人無法讀懂的抽象概念；而要求AI既會天馬行空地猜想，又把每一步都塞進形式化的緊身衣里，本身就是一個矛盾的難題。

但別忘了，兩年前，許多人還認為AI無法在面對未見過的高等數學競賽題時取得像樣的分數。而僅僅幾個月后，那些硬核的測試題就被接連打穿。Ono就是最早一批親眼見證這種躍遷的人。他從“哀悼自己的學術身份”，轉向全身心擁抱這場變革，不過短短幾個月。他的故事像一滴顯影液，讓整幅圖景突然清晰起來：人們爭相押注的，并不是一個靜態的“數學AI”，而是一個會自我進化、自己給自己判卷、而且越變越嚴謹的智能循環。

再往深處想一步，數學只是第一塊試驗田。如果AI能學會用邏輯鐵鏈鎖住自己的每一步推理，那么未來，同樣的架構也許會滲入藥物發現（每一步分子設計的邏輯可追溯）、工業設計（每一條參數變動的依據可驗證），甚至法律條文推演（每一條結論必須標出它在法典中的出處）。那個靠“我猜”運轉的人工智能，可能正處在一個升級成“我證”的轉折點上。

當然，這些延展還停留在一種合理的期待里。眼下在帕洛阿爾托那幾間安靜的辦公室里，人們正在一行一行敲下Lean代碼，試圖讓機器讀懂人類幾千年積攢下的那些最優雅的證明。沒有人能斷定這場實驗會在何時看見盡頭，但所有走進這個田野的人，都覺得自己聽到了內燃機發動時的轟鳴。那個佃農最終上了駕駛座，而我們現在，正站在扶手邊，聽著引擎一點一點熱起來。