以為你已經到宴會廳了。”
“傑克打電話給我，說你要回趟房間，我就正好在這裏等你了。”
“有什麽事嗎？正好邊走邊說。”喬喻扭頭看了眼身邊的鄭希文，老鄭乾脆放慢了腳步。
彼得·舒爾茨開口問道：“還記得之前你問我最近在做什麽嗎？”
喬喻點了點頭，說道：“當然記得你跟微軟的lean社區合作，參與液態張量實驗，希望能將數學定理形式化，並使用Lean對其進行驗證。”
彼得·舒爾茨熱切的說道：“所以你是否對這個項目感興趣？你知道的，如果能用一個統一的語言來對數學進行描述，這將大大提升定理證明器的工作效率。
在這方麵，廣義模態公理體係的潛力巨大。事實上不止是我，達斯汀·克勞森對你的研究也非常感興趣。
但現在我們缺少對你的廣義模態公理體係足夠了解的人。毫無疑問你是最適合的。相信我，這是一項很有意義的工作。
如果我們能成功的話，將複雜的數學定理形式化，未來我們將能使用電腦去驗證許多複雜的數學定理，大大減輕未來數學的研究工作。”
喬喻有些猶豫。
說實話，他對這個項目的確有些興趣的。因為他對人工智能很感興趣。
雖然lean的本質是一個交互式定理證明器和函數式編程語言，其核心並不是人工智能。
但對於喬喻來說，如果能夠參與這項工作，喬喻覺得可以嚐試將這項工作跟人工智能結合，開發出專用的智能定理輔助證明工具來。
這其中最有價值的就是這個項目本身跟彼得·舒爾茨這麽多年的積累跟研究。
猶豫自然還是因為喬喻那為數不多的道德感在作祟。
主要是彼得·舒爾茨現在已經很熟悉了，而且之前也算是幫過他不少，不太好意思直接黑。
如果是跟昨天早上那批人一樣的關係，喬喻可以毫不猶豫的答應下來，先把之前的研究資料要到手再說。
說不定未來他還能比微軟先擁有能夠輔助數學家證明驗證各種定理的技術，甚至說不定還能更進一步。
但這種事太熟了真就不好下手……
所以猶豫一會後，還是忍痛說道：“彼得，你知道的，我接下來的工作很多。真不一定抽得出時間來做這件事情。”
“沒事，我已經跟達斯汀·克勞森商量過了，你可以在華夏跟我們合作。我們遇到問題了，可以隨時用會議軟件溝通。”
彼得·舒爾茨熱情的說道。
。道問眼眨了眨喻喬”？我給發程遠接直就道難究研的們你竟畢？嗎好樣這……額“
”。區社源開個是就本nael？好不樣這得覺會你麽什為“：道問的異詫茨爾舒·得彼
ｗｔ．ｐｏｏ到請，節章新最書本看
。來出布公料資的細詳有沒並，究研的你過找我。的源開是不並究研性節細體具的目項定特，知所我據但“：道答喻喬
義定的準標些一到及涉能可來未在這且而
”，司公家一開算打也我，道知不還能可你。
。西東的麵方利專多太到及涉會不並究研的們我上實事。節細些這意在要不，喬，哈哈“
”。的談以可是也得覺也我，利專的值價用應際實備具了現發的真，中程過究研果如，然當
。道釋解著笑大茨爾舒·得彼
！？的方大麽這軟微，信相敢不些有，眼眨了眨喻喬
)完章本(
