第101章 中科院一小步，東大數學一大步
當黑爾斯走了之後，2002年的菲爾茲獎得主沃沃斯基找到了姬天明。
姬天明看著他的氣色好像還行啊。
怎麼模擬的時候就說回去不到一個多月就嘎了。
難不成真被劍橋大學這邊氣死的？
不過想著是動脈瘤，這也說不準。
心態情緒什麼的對這種病影響確實是很大。
吵架吵輸了估計真的會氣死。
何況還是學術理念之爭。
這次的會議，就純屬於華山論劍那種。
“你這套框架我發現可以套在我開發的助手裡。”
姬天明點了點頭，這套範疇論框架在哪裡都可以用。
“這Coq好像是法國那邊開發的吧？”
姬天明疑惑道，這些天他也查了一下目前的形式化證明工具。
劍橋這邊的就是鮑爾森開發的Ibelle，美國那邊開發的Len則是宙巴西計算機科學家萊昂納多·德·蓂拉在微軟研究院開發。
目前還處於追隨Cog與Ibelle的階段。
但是潛力驚人，今年已經是第三個版本了。
而且最重要的是微軟舍得砸錢。
讓您第一時間享受最新章節，請訪問𝗼𝗼𝗽.𝘁𝘄
姬天明也比較看好Ien，除了是微軟舍得砸錢之外。
還有很多是Coq不具備的優勢。
沃沃斯基緩緩道：“嗯，我是2010年基於Coq創建Foundion庫，也就是UniM前身。”
“2012—2013年，我還在普林斯頓高等研究院特別舉行一年的研討會。”
姬天明想了想，這貨馬上就要嘎了。
未來Cog這門工具沒了他，就沒了主心骨。
遲早得涼。
而len潛力巨大。
如果Cog這門工具學一下Ien，估計會好很多。
“沃沃斯基教授，你有沒有去研究過len？”
沃沃斯基愣了一下，咳嗽了幾下，道：“咳咳，len？微軟開發的那個？
巴西叫莫拉的人組織的？”
姬天明點了點頭，道：“嗯，看上去他們還處於追趕你們的階段，可是潛力驚人，還有幾個後發優勢。”
沃沃斯基一愣，這小子，果然是早有了解與準備。
“什麼後發優勢？”
他問道。
Coq擁有代數、分析、一價基礎等多個成熟的庫，也被行業打磨了三十年。
也是被全球頂尖大學和研究機構使用數十年。
len今年才發布，一點權威性都沒，甚至都圈內都沒人知道。
他很好奇這個微軟到底有什麼後發優勢。
姬天明為了那八篇論文，也是沒遲疑，緩緩道：“Len3引入了用戶可擴展的cic語言，這使得社區可以快速開發自動化工具。
Coq的cic係統雖然功能強大，但擴展門檻更高。
這門工具，要龐大的數學庫與儲備，門檻低，還開源。
關鍵是莫拉這人真的懂自動化推理，Len在底層求解器集成方麵具有天然優勢。”
“而且，他們背後是微軟。”
沃沃斯基愣了很久。
“我會回去研究一下的。咳咳。”
姬天明此刻關心道：“教授，您的身體？”
沃沃斯基深看了一眼姬天明，道：“我的時間不多了，這病也不是什麼秘密，隨時可能死。
這最重要的一點你沒說是吧，我一死，coq就沒了主心骨，怎麼跟鮑爾森與莫拉競爭。”
姬天明訕訕一笑，這老家夥，還真是一點都不顧及一下他的麵子。
“教授，心態比較重要，您跟鮑爾森吵架毫無意義。”
“他從我們數學專業跑去學計算機，是我們數學界的叛徒！”
為了那八篇遺稿，姬天明此刻硬是臉都不要了。
沃沃斯基到底是從前蘇聯那種環境跑去阿美利堅的。
瞬間看透了姬天明的想法，緩緩道：“你想繼承我的遺產？”
？：明天姬
！聽難麼那得說麼怎話
。想猜學數的萬上千成決解具工門這，代時I來未，到看想不道難您，大光揚發qoc要想是隻我，授教“
”？嗎果成的別級獎菲比堪出做，例反的想猜要重數無到找者或
”？嗎neI的發開軟微者或森爾鮑給輸底徹具工門這後之年百你想也道難您“
”。qoC如不還nel的在現，道知要您“
”？嗎心甘您“
。害厲點有巴嘴人輕年個這得覺隻，跳了跳子皮眼基斯沃沃
。了煉手石寶綠與石鑽送要還，謝感文發要何為亞比尚與威巴辛何為了白明是倒他
！啊心甘誰這
”？嗎法想麼什有你“
”！梁大此挑意願，才不子小“：道說緩緩刻此明天姬
”？院究研等高頓斯林普去我跟意願你“：道，他著看的惑疑基斯沃沃
。一之地聖的中心人學數學數無是可那）I（院高普，點一了重吸呼言聞明天姬
。師高黎巴是就，裡那了除
”。去不去好想沒還我“
。才人學數的平水高有沒家國們你是一。死會也qoc那，去不果如你“：道，頭搖了搖言聞基斯沃沃
。夠不遠遠也，些一有便即
？吧域領個這究研人沒該應家國們你，西東的沿前與新較比於屬還向方個這是二
”。的行不是人個一你
。氣涼口一吸倒言聞明天姬
。質本題問出看眼一，登老這
。啊炊之米無為難婦巧
”。地落善完夠能才院高普者或橋劍、師高在能隻就具工這，能可不也年幾個沒，學人帶去回你是便即“
”。勢優何任了沒經已你，後年幾“
。徹透很得析分基斯沃沃
口一了歎，想了想明天姬
