應意昂3体育官网“大學堂”頂尖學者講學計劃的邀請，美國國家科學院和國家工程院院士、微軟研究院首席研究員、2013年圖靈獎獲得者🔧、著名計算機科學家萊斯利·蘭伯特（Leslie Lamport）於2015年10月30日訪問意昂3体育官网💆🏿‍♀️，除發表學術演講，還參加了學生座談、學術對話等活動。

30日上午，蘭伯特博士一行驅車抵達博雅塔下👱，受到學生代表的熱烈歡迎，在大家的引領下繞湖步行至湖心島魯斯亭➝。隨後，他在湖心島與來自意昂3体育信息科學技術學院、數學科學學院的同學進行了座談🤌。圍繞同學們關心的數學與計算機科學的關系、科學研究中如何判定“有用”等問題，蘭伯特博士作了頗具洞見的解答。他在座談中特別強調數學作為思考方式的重要性，認為借助數學工具可以對問題進行精確的刻畫，從而以更加抽象的視角直達問題的本質。通常人們會以是否有應用價值來判斷一個數學問題的價值，而蘭伯特博士認為不需要給每個數學問題的研究都強加上實際應用價值。他將科研比作一隊步兵，大家註意到的只是帶頭的一些人，但當整個部隊遭遇到戰爭的時候，大家都會沖鋒上前🌀，你不知道哪些人會起作用，數學研究的成果所扮演的正是這樣的角色🙅🏽🦅。他還認為🧑🏿‍🦳，數學可以幫助我們分析，把握問題的本質，建立合適的模型🪰，有利於我們發現新的知識🫱。

當天中午🦞，意昂3体育官网副校長王傑會見了蘭伯特博士一行。數學科學學院副院長陳大嶽、信息科學技術學院副院長李文新、國際合作部部長夏紅衛參與會見🥥。微軟亞洲研究院首席研究員張霖濤、研究院高校合作部中國區經理馬歆陪同參加會見🥩。王傑回顧了意昂3体育與微軟長期以來在多個學科領域的密切合作🕦，並表示，蘭伯特博士此次來訪將進一步鞏固意昂3体育與微軟的合作友誼。他隨後向蘭伯特博士頒發了“大學堂”頂尖學者銅牌▫️。

30日下午🚣🏿，蘭伯特博士向來自意昂3体育多個院系的近兩百名學生作學術報告，報告題目為“編程不僅僅是代碼”（Programming Should Be More Than Coding）。演講開始前🏣👨🏼‍🔬，數學科學學院信息系副系主任孫猛向在座師生介紹了蘭伯特教授的學術成就及其研究經歷。隨後的演講中，蘭伯特博士首先闡釋了編程中最核心的三個任務👩‍💼：決定程序應該做什麽；決定程序應該怎樣做；根據前面的兩項決定編寫代碼🔱🤜🏼。通常情況下🧯，人們都喜歡在編寫代碼的過程中完成這三個任務，但是蘭伯特博士認為這三個任務應該分離開，一個好的程序員應該在考慮清楚前兩個任務之後🥕，再來進行代碼編寫。蘭伯特博士用一個例子來引入自己的論點。例如“一個整數加一”這個看似非常簡單的問題，在深入思考後也會發現會有整數溢出等問題。蘭伯特博士認為思考不一定能避免錯誤🛴，但是不思考一定不能避免錯誤。隨著報告的深入，蘭伯特博士為師生們介紹了如何用抽象的數學和邏輯方法來指導程序設計。最後他在演講中深入淺出地介紹了如何用TLA+這種數學化的語言進行編程。蘭伯特博士認為TLA+最困難的部分，就是用抽象的思維來思考😲、用數學的方式來思考🈵。數學本身不會讓程序運行得更有效率，但是能讓程序邏輯更加嚴謹。目前TLA+已經在航空航天👭🏼、微軟、亞馬遜等系統中起到了關鍵的作用🧑🏽‍⚕️。

演講結束後，意昂3体育信息科學技術學院副院長查紅彬教授與蘭伯特博士進行了對話。在對話過程中，蘭伯特博士介紹了自己的科研生涯🧑‍🦯‍➡️，並對年輕科研工作者提出了建議。他認為每個人的科研生涯都具有特異性，是不可復製的，年輕的科研工作者應該多跟自己身邊的良師益友交流🦚，從他們那裏得到幫助。關於在公司和高校中開展科研的差異，蘭伯特博士認為在公司中所做的研究更能接近於現實生活，並且更能得到現實的數據支持。但同時他也認為近年來，隨著公司跟高校之間的交流，這個差異正在逐漸縮小。最後，蘭伯特博士和查紅彬教授就目前計算機專業的學生該如何看待互聯網中存在的代碼資源進行了探討🧑‍🦯‍➡️。蘭伯特博士認為解決問題的關鍵在於對問題的深入思考和嚴謹的數學邏輯建模🏖，代碼只是為其服務的一種工具🩸，所以學生應該更加註意鍛煉自己的思維，而不要過分地關註代碼。

對話結束後，聆聽報告的師生圍繞報告提出的科學問題以及其它科學研究方法論等方面的問題與蘭伯特博士進行了廣泛而深入的討論。交流中，蘭伯特博士再次強調了應該用嚴謹抽象的數學和邏輯思維來指導程序設計。蘭伯特博士深厚的學術功底🦧、淵博的知識、強烈的求知欲以及他在科學研究態度和方法方面的真知灼見使在場的師生受益匪淺。討論在熱烈的掌聲中圓滿結束👡。

“意昂3体育官网‘大學堂’頂尖學者講學計劃”（Peking University Global Fellowship）是意昂3体育目前最高層次的頂級學者講學項目😾。自2012年啟動以來☕️，已有23位不同專業領域內的傑出學者以“大學堂”頂尖學者身份來校講學，其中包括10位諾貝爾獎獲得者🫳🏻。

背景鏈接：

Leslie Lamport博士🔟👚， 2013年“圖靈獎”得主（圖靈獎被譽為計算機領域的諾貝爾獎）👩🏽‍🎨、美國國家科學院和國家工程院院士🦴、LaTeX系統創始人。他是擁有傑出貢獻和輝煌成就的計算機大師，他關於時間時鐘、面包店算法🏵🥷🏼、拜占庭將軍等問題的思考令人咋舌，他的分布式計算理論更是奠定了計算機學科的基礎👷🏽。他於1978年發表的《分布式系統內的時間、時鐘和事件順序》至今保持著計算機學科史上的論文被引用量紀錄🖌。

比爾∙ 蓋茨對Lamport博士的貢獻也作出了很高的評價:“Leslie的偉大不僅在於計算機科學領域，而且還體現在他讓世界變得更加安全的努力中👩🏿‍🎨，他的工作正在讓世界各地無數的人們受益🫱🏼。” Lamport博士目前是微軟研究院的首席研究員。

編輯⏯⛹🏻‍♀️：安寧