50萬行代碼庫揭示數學命題壓縮600倍展開達10^104奧秘

當談及數學時，我們近乎本能地認為，數學是一個嚴謹、精確、不容置疑的完美邏輯體系，但在菲爾茲獎得主邁克爾?弗里德曼（Michael Freedman）眼中，人類真正創造和關心的數學，本質上是「柔軟且可塑」的。

Michael Freedman 是當代最具影響力的數學家之一，曾因解決四維龐加萊猜想獲得菲爾茲獎。這一成果被認為是拓撲學領域的里程碑。

此后，他并未停留在純數學領域，而是轉向應用前沿，創立了 Microsoft StationQ，成為拓撲量子計算的重要推動者之一。

近年來，Michael Freedman 又將研究興趣延伸至人工智能，嘗試用數學視角理解人類知識的結構與生成機制。

這種數學家們在幾十層抽象之上輕松將龐大的演繹鏈條凝練為簡潔的概念背后，揭示了一個被數學家們使用了 3000 年、卻很少被言明的秘密：數學的本質，不是證明，而是壓縮。

人類做數學，從來不是在窮舉推理路徑，而是在一個幾乎無限的空間中，不斷尋找可以被壓縮的結構。相較之下，AI 卻是一直在「窮舉」……

因此，在 AI 正處于關鍵發展階段的當下，理解這一機制，或許正是人類與 AI 在數學領域實現真正協作的起點。

下面是此次 Michael Freedman 的采訪內容，為了更好地閱讀，我們在不改變原意的基礎上進行了調整。

主持人：當我們談到數學時，通常會認為它是一個嚴密、完美的邏輯體系，但你的研究似乎在說，人類真正使用的數學并不是這樣。你能否從「壓縮」這個概念開始講起？

比如「10」可以用一個「1」放在特定位置表示，「100」也是類似。就是通過把「1」放在不同的位置，從而用極少的符號表示極大的數。這種表示方式讓整數的表達具備對數級增長，卻能在有限符號中表達指數級數量的數。

這就是一種極其強大的壓縮方式，它甚至和現代物理中的一些思想（比如自旋鏈狀態）有關。但壓縮遠不止是數字表示，它貫穿整個數學體系。

主持人：能舉一個更具體的例子嗎？

Michael Freedman：我剛上大學時，第一次上微分方程課，教授在黑板上寫下一個一個巨大的 Ω，并說它是「向量叢截面的芽層」（sheaf of germs of sections of a vector bundle）。

那一刻，我甚至不知道什么是向量叢？后來我才意識到要理解這句話，你需要理解背后的多層概念：向量叢、截面、層、芽，以及它們之間的映射關系。如果再往下深思，還涉及自然數、整數、有理數、實數、向量空間、流形等基礎結構。

也就是說，數學家在思考時，其實是站在十幾層抽象之上。這就是為什么微分方程「看起來不難」，因為大量信息已經被壓縮了。

這就是「壓縮」的力量：大量信息被隱藏在高層概念中。

而如果你用 Lean 這樣的形式化語言表達，就必須把這些壓縮全部展開。所以可以說：壓縮是數學的核心，而且已經存在了 3000 年。

我們研究了兩者的關系，發現這種層次關系將相對簡單的數學命題變成了源自基礎 Lean 術語的、極其巨大的樹狀結構。

主持人：我記得這可以達到一個非常荒謬的數字：10 的 104 次方，對吧？那我想問，你做這些事因為你想強調這本質上是數學的核心，對嗎？

Michael Freedman：是的，我們將這個庫中的內容視為人類行為的一個良好樣本，雖然它在數學各領域的分布并不完美 —— 數論和代數幾何比分析或拓撲多得多。它不是人類數學思想的完美副本，但它與「從一組公理出發進行每一種可能的邏輯推演」截然不同，后者會導致「混沌數學」。

而無論如何進行形式化，發現結構都會呈雙指數級增長。最終的結果就像你說的，我們在 Lean 庫中找到的最長的解包命題（Unwrapped statement），其大小為 10 的 104 次方），比 Googol（10 的 100 次方）還要大。而它對應的包裝命題（Wrapped statement）只有 600 個 Token。

這展示了驚人的膨脹，但反過來也展示了通過使用概念所獲得的巨大壓縮。

我想說的是，數學家和他們的智能體實際上在同一條船上。但當你看到像 Googol 這樣的數字，即使我們的機器比我們快 100 萬倍，100 萬在 Googol 的尺度下也是微不足道的。

所以，真正的問題不是人類與機器將探索什么，而是在龐大的形式推理空間中，哪一部分是可以被壓縮成我們和智能體能夠理解的形式（我稱之為形式數學）。

我相信人類數學（在此將我們的智能體也視為「人類」的一部分）正是如此。

主持人：在你們分析的這些方程中，是否發現存在某些方程或過程，不具備與其他事物相同的「公分母」？如果是這樣，如何決定什么是「最基礎」的？或如何知道自己「觸底」？

Michael Freedman：對于 Lean 來說，很容易知道什么時候觸底，因為庫的結構就是這樣設計的。

基本上，有原始項，你可以用它們構建更復雜的命題，所以這個「展開后長度」有時被稱為樹表示法。每個命題，你看它的子節點，即它是由什么構建的，然后你看那些子節點的子節點，形成一棵越來越深的樹，直到它終止于原始的 Lean 項。之后統計所有這些節點的調用，每個節點根據其調用的先前節點的權重被賦予權重，從原始項權重為 1 開始。當把樹上頂層的權重加起來時，就得到了展開后命題的巨大數字。

而壓縮在于，人類設計并利用 Lean 表達了一種語言，可以用大約 600 個 token 寫下這個 Googol 量級的數字。

幺半群類似于群，只是未必有逆元，最簡單的幺半群就是計數數字，即自然數。在幺半群一側，可以放入「宏」（macros），即「新思想」，代表新的抽象，可以幫助我們更高效地表達信息。

比如「10 的冪次方」，就是一個能實現壓縮、高效表示整數的宏的例子。一旦在幺半群中有宏，就可以推導出層級屬性、衡量壓縮程度。

研究結果顯示，宏越多，實現的壓縮程度就越高；宏越少，壓縮就越少，表達能力越弱。

而在數學這一側，在 Lean 庫中，我們不知道宏是什么，這有點像在問數學的使用手冊，我們對此獲得的洞察越多，「人類」（我們和智能體）在探索數學時就會越順利，想法是去學習已經在數學中使用的機制：原則是什么？推論是如何組織的？

現在的主要挑戰是解決「逆問題」，即看看在數學側對應的「宏」到底是什么。

主持人：在數學推理中，機器往往需要遍歷指數級的可能性，而人類卻能以更慢、近似多項式的（速率）方式直接切中要點。這種差異是否源于一種「數學品味」？我們是如何從海量可能性中篩選出真正有意義的路徑的，以及這種能力是否可以被建模和復制到機器中？

Michael Freedman：這是實驗科學，正是我們試圖發現的。我們試圖在某種程度上循環分析數學的歷史，試圖理解是什么引導我們走向這些高度可壓縮的形式推理領域，也許澄清這個概念，舉一些宏的例子會更好，就能看到什么是可壓縮、什么是不可壓縮的。

主持人：有沒有更為直觀的例子？

Michael Freedman：比如有一個定理：任何整數都可以表示為四個平方數之和（拉格朗日定理）。

這意味著，如果你將「平方數」當作宏，那使用這種增長極快的宏，每個整數只需要四步就可以表示。

聽起來很瘋狂，但解釋是表達這些平方數本身需要很多比特，所以這并不違背信息論。它只是，說明如果有更稠密的宏集，就可以用更少的步驟表達更多內容，即宏的「密度」決定表達效率，而「10 的冪次方」正好處于平衡點，在宏的簡潔性（不要太大）和表達能力（能夠大量擴展）之間找到了一個最佳平衡點。

而根據經驗和數值研究，我們發現數學具有高度可壓縮性。如果它能被一個幺半群很好地表示，那么它必須是一個多項式增長的幺半群，才能展現出我們面前看到的這種壓縮。

因此可以推測：數學的結構本質上是多項式的。

Michael Freedman：這是個好問題。PageRank 基本上是一種尋找馬爾可夫鏈平衡的算法。

換句話說，它是尋找某個微分方程的吸引不動點，你有許多互相交流的節點，想通過觀察誰調用了誰來確定誰最重要。這是一種分配重要性的自然想法，但它需要對結構和互連有全局性的了解 。

「還原壓縮」是「展開長度」與「壓縮長度」的比值，如果一個陳述處于極高的抽象水平，展開后會變得巨大，那么這個比值就會非常大。這不僅是自動智能體可以使用的局部指標，還可以用來判斷是在提升還是降低抽象層級。

「演繹壓縮」則是觀察證明長度與命題長度的比值，這個比例告訴我們有多少數學工作被壓縮進了那個命題中。比如費馬大定理，可以用一句話描述，但證明需要數百頁。這個比例證明了現象級的力量：該命題具有極高的「壓縮密度」。

AI 可以在探索證明路徑時追蹤這些指標，以此感知它正在穿越的「景觀」。

而至于我個人為什么選擇這個研究方向？

更具體來說，我們正在學習，尋找能夠引導發現「有趣數學」（即人類數學）的簡單組織原則將是富有成效的。我們已經看到，這種可壓縮性在數學中有著非常不同的形式。

所以，數學家使用局部壓縮，而全局壓縮是不可計算的。但可能存在某種中間地帶，通過仔細研究壓縮，我們和智能體也許能探索超越局部壓縮的新思維模式。這是一個模糊的想法，但我想呈現給大家。

所以，我認為我們和 AI 在某種意義上是「同一條船上的人」。它們也無法通過暴力計算探索全部空間，必須像我們一樣依賴「直覺」。而未來的關鍵是：我們如何與 AI 一起，發展新的數學直覺。