【第145章 重裝證明】
------------------------------------------
8月12日,淩晨兩點四十分。
瑞士,蘇黎世聯邦理工學院,數學係G樓五層。
整層樓的感應燈早已熄滅。
唯獨走廊儘頭,Heinrich Voss教授辦公室的門縫還透著光。
Voss今年六十一歲。
他穿著一件洗得有些發白的深灰色羊毛衫,鼻梁上架著老花鏡,銀白色的頭發在台燈的逆光下顯得有些稀疏。
如果隻看外表,他就像蘇黎世街頭隨處可見的退休老祖父,安靜,嚴謹,甚至有些刻板。
但在這間堆滿手稿和預印本的辦公室裡,他是加性組合學中熵方法方向的一位老派人物。
三十年來,他始終隻做一件事。
在多變量概率分布的齒輪之間,尋找對稱性、熵耗散和結構壓縮的邊界。
他不是那種喜歡在公共論壇上發表意見的學者。
沒有Twitter賬號。
不參與學術圈的熱點爭論。
事實上,在一周前,他甚至沒有注冊過Lean Zulip賬號。
他習慣讓數學停留在紙麵、黑板、手稿邊緣那些密密麻麻的鉛筆批注裡。
他對Lin Jiang這個名字的最初印象,來自八月四日那天Manners打來的一通電話。
那時,Voss正在阿爾卑斯山下的采爾馬特度假。
說是度假,其實也隻是換了一個地方工作。
他坐在木屋露台上,膝蓋上攤著一本托馬斯·曼的德文小說,桌邊放著一杯黑咖啡。
遠處,馬特洪峰山脊上的雪線在午後陽光裡泛著刺眼的白光。
他的妻子端著一盤烤鬆餅走過來,看見他盯著雪線發呆,隻是無奈地搖了搖頭。
她太熟悉這種狀態了。
一個數學家所謂的休假,往往隻是從辦公室裡的黑板,換到山腳下的餐桌。
他的身體在山裡。
靈魂仍被囚禁在那些抽象符號之中。
就是在那個下午,Manners的電話打了進來。
電話接通後,連一句常規寒暄都沒有。
Manners的聲音透著一種異乎尋常的急促。
“Heinrich,你必須看一下這個,馬上看。”
Voss點開了Manners發來的文件包。
第一份,是江臨剛剛對專業審查圈開放的PFR/Marton v0.95流通版手稿。
第二份,是一份形式化依賴圖說明,列出了第31號到第47號節點的Lean4編碼進度。
第三份,是第38號節點雙重對合封裝器的自然語言藍圖。
最新小說章節盡在o o p . t w
Manners在郵件裡隻標出了一句話。
【從第38號節點開始看。】
於是Voss沒有從第一頁開始慢慢讀。
他徑直切入了第4.2節。
第三層損失回收。
殘餘譜賬目。
熵對合引理。
K大於等於8情形下的高維邊界。
那是他這三十年裡最熟悉的一片泥沼。
他坐在露台那把藤椅上,用了整整三天時間,隻讀了這一處。
反複讀。
反複算。
反複把江臨的自然語言證明、Lean形式化藍圖和依賴圖節點攤在同一張桌麵上,對照著推回去。
山裡的風吹過他的羊毛衫,但他仿佛失去了溫度感知。
到第三天傍晚,他合上電腦,長久地看著馬特洪峰的雪線。
隨後,他做了一件自己三十年學術生涯裡極少做的事情。
他提前結束假期,驅車三個小時趕回蘇黎世的辦公室,開始寫一份邊界測試note。
不是反駁論文。
。洞漏布宣是不也
。妒嫉的人輕年對者學輩一老於出是不更
。趣興種這有沒ssoV
。險風性見可的界邊維高處一了見看是隻,睛眼的年十三了泡浸裡法方熵在雙那他
。線路裝封合對重雙的輕當相條一了用采分部收回失損層三第在臨江,度測驗後量變四的雜複理處了為,裡稿手版通流59.0v在
。亮漂常非線路條那
。裡口接化式形的小短對相個一進壓生生硬,構結稱對的瑣繁其極點節號83第把,刀術手的利鋒而薄把一像
。的錯是不它,看輯邏局全的明證主從隻果如
。例反的理定主翻推以可到看有沒也ssoV
。了法方熵悉熟太他但
。深太得藏價代層界邊些某把會往往,西東的短簡亮漂於過,區水深的學數在,知深他
。了沒藏是不
。付支被裡哪在竟究它見不看者查審部外到藏是而
。失消空憑會不性雜複
。收吸地楚清被方地個某在須必就,扁壓被裡這在它
。住卡下形情K高維高在能可就者讀的來後,來出亮式顯程過收吸處一那把不者作果如
。了塌橋為因是不
。裡土凝混了進包被構結重承處一某的橋為因是而
。裡那在它道知者作
。見不看卻者查審部外
。試測的銳尖夠足個一了成縮壓點點一,覺直的糊模個那中海腦把,算演複反上板白在,間時天五了花,裡室公辦在關己自把ssoV
。型構界邊8=K的定特個一取,中型模維限有的流回簇譜露顯以足經已樣這⁵¹₂F在
。常正切一代迭輪兩前,進推線路裝封合對重雙的版通流59.0v著沿果如
。流回層界邊的眼顯不極次一現出會項失損譜餘殘,時代迭輪三第了到但
。塌崩理定主致導會不流回個這
。敗失明證主的臨江明說以足不也
它但