如何评价菲尔兹奖得主 Vladimir Voevodsky？ 第1页

每年年初 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) 是一个命题. 所以 , 其中 Type 是所有类型形成的“类型”（这当然是不可能的，但可以通过给类型标号解决这个问题；并不影响这里的讨论）. 如果我们想证明 , 我们需要做的就是给出一个 n, 并给出 Prime(n)——一个类型——中的一个 inhabitant, 也就是一个偶对 (n, p), 其中 n : N, p : Prime(n). 注意这个和前面提到的积类型的相似之处. 事实上这就是 dependent type theory 中 dependent sum 的构造，记为 或干脆记为 . 当然对任意的类型 X 及其上的一个 dependent type P : X→Type 都可以做这样的构造.（为什么“积”类型和 dependent sum 类似留给有兴趣的读者思考.）类似地，一个 的（当然不可能存在的）证明应当是 N 上的一个函数 f，其类型随自变量的取值而变化——f(n) : Prime(n). 这个类型称为 dependent product, 记为 .

等式的情况比较微妙。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) 的话， 就是这个空间的一个 section. 而 total space, 不难看出正是 dependent sum type . 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 的讲稿中都有提到，这个 MathOverflow 问题 做了很好的总结. 1991 年他和另一人合作，“证明”了某命题 T. 1998 年，另一个数学家构造了命题 T 的一个反例，但没有发现他们证明中的错误所在. 但没有人去当面质疑 Voevodsky, 大家只是默默地不引用他的结果了. Voevodsky 一直都觉得这个反例的构造有问题，到了 2013 终于发现自己的证明确实有错，命题 T 并不成立. 另外他也有一位友人遇到了张益唐式的事故——引用了某篇文章中的某个结果证明了某个定理，结果所引用的结果被发现是有问题的. 这些事件之后，Voevodsky 致力于将数学证明形式化并用机器验证. 于是就有了 UniMath (https://github.com/UniMath/UniMath).

To be continued ...