一根針要轉身，面積可以是零
一根單位長度的針平放在桌面上，針尖朝北。現在讓它轉過一百八十度，針尖朝南，過程中掃出的面積，最小可以是多少。直覺的答案是一個以針心為圓心、半徑二分之一的圓盤。一九一七年，日本數學家掛谷宗一把這個問題擺上檯面。他當年限定在凸區域裡問，後來得到的最佳解是三尖內擺線，一個由滾動的圓描出的圓角三角形；而拿掉凸的限制之後，答案跌破所有直覺，面積可以壓到任意小，甚至為零。
這種在每個方向都容得下一根單位線段、總面積卻趨於零的集合，被稱為掛谷集合。以造形而論，它是幾何裡少見的極端物件：細長的針狀碎片自中心向四面八方伸出，彼此層疊、互相借位，用最小的佔地容納所有方向。輪廓像一朵被拆開重組的花，每一瓣都是一條方向的通道。放射狀構圖推到極限，大概就是這個樣子，只是這裡的約束條件寫在數學裡。
十月二十六日，OpenAI 發布新一批研究成果，其中一篇論文題為《Local smoothing for the Euclidean wave equation》，歐氏空間波動方程的局部平滑。論文對所有不小於二的空間維數給出局部平滑的證明，並由此推出一串經典結果：Sogge 局部平滑猜想、Bochner–Riesz 猜想、Stein 傅立葉限制猜想，以及掛谷猜想。那根轉了一百多年的針，這次有了完整的著地點。
局部平滑：一條主幹撐起四個分支
局部平滑談的是波。石子落進水面，漣漪一圈圈擴散，波動方程描述的就是這類傳播。局部平滑指出一件事：把波在時間上前後取平均，得到的形比任何單一刻度都更平順，衰減多出一點。這一點聽來細微，卻是整篇論文的主樑，其餘三個猜想沿著蘊含關係逐層掛上來。猜想一詞在數學裡的意思很具體：暫時無人能證，也無人能否定，一掛就是幾十年。
Bochner–Riesz 猜想關於多重傅立葉級數的圓盤形部分和：用一塊柔邊的圓形遮罩截取頻率，邊緣的滲漏能控制到什麼程度。Stein 傅立葉限制猜想問的是頻譜能否安放在彎曲的曲面上，曲率在這裡扮演承重的結構，球面與拋物面撐得住，平面撐不住。掛谷猜想則把當年那根針的問題換了單位再問一次：這種零面積的方向集合，維度能否與整個空間相同。
四個問題分屬調和分析的不同角落，詞彙卻高度共用：方向、頻率、尺度、曲率。論文把它們收進同一份目錄，四類問題與其他推論集中在一篇文件裡，讀起來更像一份產品線說明，一章主功能，其餘章節是衍生的應用項目。
當證明取得檔案路徑
這次發布在論文之外，還附了一份 GitHub 儲存庫。說明頁列了一張清單：局部平滑、Bochner–Riesz、球面限制、掛谷，各自連到對應的 Lean 陳述。每個條目一行，名稱連到檔案，像一張圖書館目錄卡的電子後代。定理在這裡取得副檔名，證明取得可被機器執行的身分，下載到的東西因此超過一份 PDF，而是一套可以重跑的檔案。
在 Lean 這類證明輔助器的介面裡，遊標落在證明的哪一步，側欄就顯示當下待證的目標；步驟收尾的那一刻，目標欄清空，狀態只剩一句 No goals。傳統論文以方框或 QED 收尾，那個記號依賴讀者對前文的信任；形式化把句點交給編譯器。核對一份百年量級的證明，從同儕的長期閱讀，變成任何人都可執行的一次檢查。
形式化這條路有前例。四色定理在一九七六年靠電腦輔助完成時，可信度爭議延燒多年，直到後來由形式化工具補上機器可查的版本才算塵埃落定。這層人與工具的分工，我們先前在陶哲軒與鄧煜的對談裡讀過，增強與依賴的分界本身就是設計決策。形式化把界線畫得乾淨：機器管驗收，人管發明。
發布文法向軟體靠攏
公告的標題是 Working with academic communities to build scientific understanding，與學術社羣協作，建立科學理解。組合有三件：一篇論文、一份形式化儲存庫、一頁官方說明。這是軟體發表的文法，白皮書配原始碼配發布說明。一家以產品聞名的實驗室，把純數學放上同一個貨架，讓定理與模型更新共用一種發布節奏。
這種把規格一次攤開的溝通設計，先前在OpenAI 斷網訓練的說明裡也出現過，官方理由、沙箱邊界、紅隊流程一次給齊。差別在於這次攤開的是數學。數學界原有的流通包裝是期刊：審稿、刊出、被引用，週期以年計；形式化儲存庫把審查的一部分前置給編譯，把發現到驗收的距離壓短。
猜想的名字本身是一套老識別系統。掛谷、Bochner、Riesz、Stein、Sogge，人名掛在問題前面，Bochner 與 Riesz 之間那條連字號把兩個姓氏綁成同一塊門牌。問題以猜想之名懸置數十年，像貨架上長期等待補貨的品項，這次一次補齊四格，補貨通知發在一個 AI 實驗室的公告欄。這個畫面本身就說明，科學傳播的版面正在移動。
針的著地點
回到那根針。它從一九一七年的一個桌面問題出發，長成調和分析裡的結構件，這次停在一份可以編譯的檔案裡。掛谷集合的規格在證明裡補上最後一欄：面積可以是零，維度卻與整個空間相同。以設計的眼光看，這是一個把約束推到極限仍不散架的形；而證明它的文件，也取得了工程文件的性格，可檢查，可重跑。
數學成果向來以期刊與教科書的形式流通，這次多了一種包裝。至於哪一種更能累積信任，編譯器已經給出它的答案；其餘的，交給時間。