如何評價菲爾茲獎得主Vladimir Voevodsky？

01-14

可以從任何方面評價，如性格，愛好的運動等
9月30日更新:
Voevodsky於一小時前去世。RIP

每年年初 NRF 都會舉辦為期一周的 Global Young Scientist Summit, 邀請各路諾獎、菲獎、圖靈獎得主來新加坡做講座，今年的會場在 Singapore University of Technology and Design. 講座本身是科普性質的，受眾是 "Young Scientist"——從高中生到年輕的 postdoc 都有。今年 NRF 邀請的菲爾茲獎得主是 Smale 和 Voevodsky. NRF 會從新加坡的各科研機構招募 liaison officer 負責接送、陪同。系裡的教授決定由我來當 Voevodsky 的 LO. 這麼好的機會我當然不能說另請高明，就欣然接受了。

我因此有幸得到機會和他天南海北聊了很多，從數學到紅學到旅遊（當然主要還是數學），聽了他的科普講座，也問了他一些關於 HoTT/UniMath 的問題。題目說「從任何方面評價」，but who am I to judge? 所以我想就隨便講點日常趣事和數學，至於評價就留給各位讀者。

Voevodsky 與邏輯學家

vv: 「天一，我覺得你的姓很難念。」

xty: 「是的，很多人都覺得 Xu 里的 X 很難念。這個字母的發音類似 ?o? 里的 ?.」

vv: 「不，是 Xu 里的 u. 為什麼這個念徐，毫無道理啊。(That doesn"t make much sense.) 我會念成 Sh-oo. 還有，?o? 是誰？」

xty: 「哦！其實 u 上應該有兩點，does that help? 順便問一下，這種字母上面的點和橫線之類的有什麼名字嗎？」

vv: 「That helps a lot! 我想應該有名字，但我不知道。」

xty: 「?o? 就是證明 ?o?"s 定理的那個人，關於 ultraproduct 的那個定理，you know, 關於 ultraproduct 中哪些語句為真。」

vv: 「ultraproduct 是什麼？」

xty: 「你不知道 ultraproduct? 那是模型論裡面一個常用的構造。You know, nonstandard analysis 之類的。」

vv: 「我不怎麼懂邏輯，我也不喜歡和邏輯學家交流。(I don"t know much logic, and I don"t like talking with logicians.)」

xty: "為什麼？"

vv: 「因為我不理解他們，他們也不理解我。(Because I can"t understand them and they can"t understand me.)」

xty （汗）: 「好……吧……沒關係，我想我們可以假設我是做數論的。」

（第二天他很開心地告訴我，"those little things we put over the letters, they"re called decorations."）

紅樓夢

vv: 「我正在讀一本中國小說，我想你可能聽說過。」

xty: 「中文的？」

vv: 「英文的。」

我心想讓西方人感興趣，還有英文翻譯的小說，多半要麼是《三體》要麼是《紅樓夢》，兩者我都讀過，就說「是的，很可能聽過。標題是什麼？」

vv: 「叫做 Dream of the Red Chamber.」

xty: 「那個可有名了！是中國古典文學四大名著之一。你讀了多少，感想如何？」

vv: 「我讀到秦可卿之死那裡。我很喜歡這本書，我覺得這裡面對女人的理解很深刻。(I like it, it shows a deep understanding of women. 我們兩人都笑了起來) 華人對這部小說的評價如何？」

xty: 「很多人認為它是四大名著中文學價值最高的。還有一門專門研究它的學問，叫紅學，研究內容比如角色的人名如何反映他們的性格、前面章節中的詩詞如何預言了角色的命運，之類的。」

vv （非常緊張地）: 「千萬別告訴我他們的命運！(Oh please don"t tell me the fates of the characters!)」

xty （笑）: 「別慌，老師，我沒打算這麼做。(Relax, Professor, I"m not going to.)」

vv: 「你剛剛提到了四大名著，另外三個是怎樣的？」

xty: 「有 Journey to the West, 講一個和尚帶著幾個徒弟經歷磨難去古印度取經的故事，基本上就是講神魔鬼怪；有 Tale of Three Kingdoms, 中國歷史上有一段時間分裂成三個國家，這部小說講的就是這些國家之間的戰爭故事。」

vv: 「我看過這種戰爭故事，我覺得一直在描寫戰鬥場面，誰又殺了誰，很無聊。」

xty: 「這個不一樣！這個更注重策略，比如會軍師向將領提議說『對方的糧草一定在那裡，我們不用跟他們剛正面，只要派一支部隊燒了他們的糧草就行了。』真正的戰鬥場面反而描寫得非常少。」

vv : 「那應該會很有趣！我以後讀讀看。」

其實我聽到學長告訴我 Voevodsky 離世的時候除了震驚和惋惜之外，第一個想法竟然是「希望他讀完了《紅樓夢》，否則多遺憾啊」。不過轉念一想，Supreme Fascist (if there is one) 的圖書館裡肯定少不了《紅樓夢》的各種版本，說不定還有曹雪芹寫的 true end, 也就釋懷了。

晚宴

第一天下午的小組討論之後是晚宴，在 SUTD 的宴會廳舉行。宴會廳在一個花園之中，花園的風格是完全中式的亭台樓閣。而宴會廳本身則是水邊的一座榭，白牆黑瓦，裝飾精緻。我們到了宴會廳，已經有服務員等在那裡了。他們手中的托盤裡裝的是某種紅酒和某種氣泡酒。我拿了一杯氣泡酒，和其他 liaison officer 攀談起來。這時我看到 Voevodsky 從另一個托盤裡拿了一杯雪碧。

SUTD 里的亭子。By Smuconlaw (Own work) [CC BY-SA 4.0 (Creative Commons - Attribution-ShareAlike 4.0 International - CC BY-SA 4.0)], via Wikimedia Commons

晚宴結束之後剛出門，他指著旁邊的水面說：「天一，你看水上有幾隻鳥。」就走到水邊觀察了起來。正好我也是能夠和路邊的貓/鳥「玩」上半個小時的人，於是在別人紛紛回去的時候我們就在水邊看起了鳥，並討論了「為什麼鳥能夠夜行」（我覺得那些「鳥」其實是蝙蝠）。他還告訴我他遇到了一個對紅學有研究的新加坡學者，這位學者告訴了他一些紅學的考據。他指著旁邊的亭子問我：「紅樓夢裡的建築是不是就是這種風格？」我回答：「我讀的時候一般都想像成這樣。」

回去的路上，我調侃說：「老師，不是我刻板印象，不過我覺得俄羅斯人都超愛喝酒的？(Professor, call it a stereotype but I thought Russians all love alcohol.)」他說：「是的，我以前很愛喝，但是我到 IAS 以後就不喝酒了。」

本來還想再寫點趣事的，不過作為（前）傳教士，實在忍不住 preach 的渴望。先寫點數學吧。當然由於篇幅原因，完整介紹 HoTT 是不可能的，不過我希望對不同背景的讀者都能有幫助。

"In fact," he continued with enthusiasm, standing there in the rain by the dead student"s grave, "let us consider a function of a complex variable...."
- David Hilbert 在學生葬禮上的致辭

這段話很可能只是一個傳說（我看到了各種不同版本，有的說考慮一個單複變函數，有的說考慮一個 [0, 1] 上的連續函數，也有說「令 ε &> 0」的）。但這告訴我們：懷念一位數學家最好的方式就是讓更多人了解他的工作。

類型論作為推理系統

正如大部分數學理論一樣，類型論作為推理系統的基本想法十分淺顯：一個命題 T 視為類型，其 inhabitants 就是 T 的所有證明. 從這個想法出發，我們可以構造邏輯連接詞. 例如，P∧Q 應該對應什麼類型？我們考慮 P∧Q 的一個證明應該是什麼形式。答案很簡單：應該是 P 的一個證明和 Q 的一個證明組成的偶對，即具有 (p, q) 的形式，其中 p 的類型是 P（記為 p : P），q : Q. 這不就是我們熟知的積類型嘛！因此 P∧Q 其實就是 P?Q. P→Q 是什麼？要說明 P 蘊涵 Q, 也就是說「一旦我們證明了 P, 就能證明 Q」，我們只需要構造一個從「P 的證明」到「Q 的證明」的函數。但回憶「X 的證明」就是 X, 所以我們得出：P→Q 對應的類型就是 P 到 Q 的函數類型，記作——十分巧合地——P→Q. 而要證明 P∨Q——任何一個 P 的或 Q 的證明都可以，所以就是和類型，也就是無交並. 注意這裡有一個細節：因為是無交並，所以如果 r : P∨Q, 那麼 r 中包含了實際上究竟是 P 成立還是 Q 成立的信息.

接下來我們來考慮量詞. 為了構造含有量詞的命題對應的類型，首先我們需要考慮「性質」這個對象怎麼刻畫. 比如我們想表達「存在一個自然數 x, x 是素數」，那麼這裡的「素性」就是自然數的一個性質，也就是對每一個自然數 n, Prime(n) 是一個命題. 所以 $mathrm{Prime} colon mathbb N o mathbf{Type}$ , 其中 Type 是所有類型形成的「類型」（這當然是不可能的，但可以通過給類型標號解決這個問題；並不影響這裡的討論）. 如果我們想證明 $exists n colon mathbb N (mathrm{Prime}(n))$ , 我們需要做的就是給出一個 n, 並給出 Prime(n)——一個類型——中的一個 inhabitant, 也就是一個偶對 (n, p), 其中 n : N, p : Prime(n). 注意這個和前面提到的積類型的相似之處. 事實上這就是 dependent type theory 中 dependent sum 的構造，記為 $sum_{n colon mathbb{N}} mathrm{Prime}(n)$ 或乾脆記為 $sum mathrm{Prime}$ . 當然對任意的類型 X 及其上的一個 dependent type P : X→Type 都可以做這樣的構造.（為什麼「積」類型和 dependent sum 類似留給有興趣的讀者思考.）類似地，一個 $forall n : mathbb{N} (mathrm{Prime}(n))$ 的（當然不可能存在的）證明應當是 N 上的一個函數 f，其類型隨自變數的取值而變化——f(n) : Prime(n). 這個類型稱為 dependent product, 記為 $prod_{n:mathbb{N}} mathrm{Prime}(n)$ .

等式的情況比較微妙。HoTT 中的「相等」或 identity type, 大致相當於 Leibniz 的 identity of indiscernibles: 如果 x : X 具有的所有性質 y : X 也具有，那麼 x = y. 反過來，如果 x = y 且 P(x), 那麼 P(y). 也就是說如果 P 是一個性質 X→Type, 則 p : x = y 給出了 P(x) 到 P(y) （兩個類型）之間的一個函數，且這個函數必定可逆（因為 y = x）. 注意如果 X 是一個類型，x, y : X, 那麼 x = y 本身也是一個類型——「x = y 的證明」的類型.

實際上在這裡我迴避了 judgemental equality 的討論，但這需要比較多形式語言的知識，和 HoTT 的核心「精神」關係也不大.

以上的一些構造，除了 dependent product 外都可以視為一種一般的構造——inductive type 的特殊情況.

類型與拓撲

dependent product 的性質 f(n) : Prime(n) 讓我們想起拓撲中一種熟悉的構造——一個 fiber bundle （確切地說是 fibration）的 section. 實際上，如果把 N 作為底空間，並要求 n 處的 fiber 為 Prime(n) 的話， $f colon prod_{n colon mathbb{N}} mathrm{Prime}(n)$ 就是這個空間的一個 section. 而 total space, 不難看出正是 dependent sum type $sum_{n colon mathbb{N}} mathrm{Prime}(n)$ . Things are getting a little interesting! 這些命題本身可以在 dependent type theory 中形式化並證明.

從 dependent type theory 到 homotopy type theory 的飛躍也來自一個看似簡單甚至平凡的觀察：「一個類型中兩個變數相等」與「一個拓撲空間中兩點之間道路連通」有相同的結構：自反性、對稱性與傳遞性. 於是前面所說的這種對比還可以推廣到等式類型. 如果 X 是一個類型，x, y : X, 那麼 x = y 這個類型可以看成是 X 這個空間中的兩點 x, y 之間的道路空間. 於是前面所講的三個性質恰好對應了 fundamental group(oid) 上的三種操作：單位元、逆和乘法（連接）. 我們可以定義一個類型的 fudanmental group(oid)! 等等，還缺一樣原料：什麼時候兩條道路同倫？所謂 x, y 之間的兩條道路 p, q （固定端點）同倫，無非就是 p, q 之間由一系列的 x,y-道路「連接」，也就是說 p, q 在道路空間中是道路連通的. 回到前面的拓撲—類型對應，我們發現如果 p, q : x = y, 那麼 p 與 q 同倫當且僅當 p = q. 於是我們可以很方便地定義同倫間的同倫，同倫間的同倫間的同倫……從而定義一個類型的 fundamental ∞-groupoid. 實際上我們還可以證明一些同倫論中的經典結果，例如第二（和之後的）同倫群總是交換群. 我們同樣也可以研究 fibration 的同倫群和底空間及 fiber 之間的關係.

小插曲：liaison officer 之間交流的一個話題就是自己陪同的教授的研究內容. 大部分都是一句話就能介紹清楚（並 induce awe）的，比如 Smale 證明了 Poincaré 猜想 n&>4 的情況，後來興趣轉向生物數學；比如 Ada E. Yoneth, 確定了核糖體的結構，這項研究幫助人們製造更有針對性的藥物；比如 David Gross, 發現了漸進自由現象，這在量子色動力學中有多重要就不用說了. 輪到我了，我說："Homotopy type theory, you see, if two things x and y are equal, that can happen in many different ways. Now "the way they are equal" can also be equal or different, etcetera etcetera, and that gives ... a nice structure. So it"s the study of .. the ways objects can be equal." 大家禮節性地點頭說："That"s ... interesting."

自動形式證明驗證與 UniMath

HoTT 能夠引起關注，很重要的一個原因就是它可以形式化整個數學，並且驗證證明的正確性. 事實上，如果 Alice 聲稱她證明了某個命題 T，她只需要給出一個項 t, 並且 t 能夠被驗證為類型 T 即可. Voevodsky 關心這個問題的理由在他四處 preach 的講稿中都有提到，大概是說他證明了某問題，但另一個數學家構造了反例但沒有發現他們證明中的錯誤. 但沒有人去當面質疑 Voevodsky, 大家只是默默地不引用他的結果了. Voevodsky 一直都覺得這個反例的構造有問題，到了 2013 終於發現自己的證明確實有錯. 另外他也有一位友人遇到了張益唐式的事故——引用了某篇文章中的某個結果證明了某個定理，結果所引用的結果被發現是有問題的. 這些事件之後，Voevodsky 致力於將數學證明形式化並用機器驗證. 於是就有了 UniMath (https://github.com/UniMath/UniMath).

To be continued ...

還不了解motvic homotopy theory，從基礎數學的方面說，他不僅是fields medalist, 更是一個極富人格魅力的組織者。他號召一群計算機，數學家，在 2012年，IAS，為Homotopy type theory 組織了一年的special program,寫出了Homotopy type theory這本書。

HoTT 的意義在於，之前除去集合論，Category theory 作為基礎理論也已經有一席之地了，但是最有實力（HoTT的Univalence 能極大簡化機械證明）Formalize所有數學而且正在進行的，目前只有Hott，書里已經給出了HIT構造的實數。

關於voevodsky 工作的意義，我自己的看法是（hott book 在讀, 用agda 嘗試過hott library)

如果數學不能被Computer checked,那數學的複雜性最終會超出人類的掌控能力。而我感覺Voevodsky的工作，就像是重建Babel tower，能夠給予人們關於數學的統一，精確的表達方式。雖然計算機程序也有這個問題，但是好歹通過反覆測試還勉強能用。

他的離去，絕不僅是世界少了一位天才，更像是少了一位未來你可能與之交談的朋友。根據資料，他十分平易近人，從未因為自己的學科是所謂鄙視鏈頂端而不屑其他學科。相反，他甚至用數學去研究生物學。此外，攝影也是他的愛好之一。

美國主流的媒體的報道

New york times: https://www.nytimes.com/2017/10/06/obituaries/vladimir-voevodsky-revolutionary-mathematician-dies-at-51.html

Wired ： Will Computers Redefine the Roots of Math?

HoTT google group上人們對他的懷念

https://groups.google.com/forum/#!topic/homotopytypetheory/K_4bAZEDRvE

Hott 更詳細的介紹： Martin awodey：什麼是homotopy type theory？

代數幾何方面是Grothendieck的motivic program的忠實追隨者之一. 一代天才,不必多言.

不過搞HoTT好像並沒引起什麼impact.

在讀 https://homotopytypetheory.org/book/，暫時還沒搞明白，希望近兩年能徹底讀懂。

大神對數學基礎做了巨大貢獻。我覺得大神重新統一了數學、邏輯與理論計算機科學。

剛知道他已經去世了，讓人震驚。

讓他到Shiva大神，或者耶和華大神的世界享受幸福吧！

最好把評價改成介紹二字。

2002年兩個菲爾茲獎得主，一個處於半退休狀態，一個英年早逝。

難道上帝要加速數學走向衰亡的歷史行程？

Voevodsky教授早年致力於代數幾何與代數拓撲的研究並榮獲菲爾茲獎。但這些理論過於精深，影響力有限。他早前就放棄了這個方向，轉嚮應用數學和數學基礎的研究。

從歷史角度看，Voevodsky教授最大的科學貢獻可能是指出了數學的巨大危機：大多數數學論文中證明的細節是沒有經過仔細驗證的，可能存在漏洞。

「A technical argument by a trusted author, which is hard to check and looks similar to arguments known to be correct, is hardly ever checked in detail.」 ------V. Voevodsky

一個典型的例子是他自己和Kapranov在1991年的一項得意工作。1998年被Carlos Simpson構造出「反例」，而直到2013年他才確信自己是對的（謝 @徐天一指正）。

因此，Voevodsky教授設想可以利用計算機來驗證數學證明的細節。他最後幾年也致力於這方面的工作，可惜不是很成功。

【推薦】一份 Voevodsky 的幻燈片

現代數學是一座沒有經過質量驗收的大廈，搖搖欲墜。

希望人工智慧的發展能實現Vladimir的理想。

如果這個理想成為現實，恐怕現代數學的大廈就要轟然坍塌了。