我是如何开始关心数学基础的
How I became interested in foundations of mathematics
记得我还在莫斯科大学上学的时候， 「数学基础 / Foundations of mathematics」 是一个特别不流行的学科。
当时有很多小组， 代数学小组，拓扑学小组， 分析学小组，微分方程小组⋯⋯ 当然也有一个数学基础小组。
在第二学年结束的时候，每位同学都必须选择他或她想去的小组。 这是一个重要的选择，我们经常讨论该去哪个小组，每个小组都有各自的名声。
在我那个时候，代数学小组非常酷，有很多名人在里面。 拓扑学与几何学的小组也很酷，也有很多名人在里面。
有一些小组就不是那么酷了，而其中最不酷的就数数学基础小组了。 （也许仅次于数学历史小组吧。）
没有哪个认为自己是位优秀数学家的人，会考虑去那里。
当时我去了代数学小组，到如今我还认为自己是一个代数学家， 我在把代数学的方法应用到数学的其它领域。
但是现在，我把所有的时间都投入到了数学基础的工作中。
我来这儿，就是为了解释解释，为什么我们发展数学基础的方式，会让它重新变得非常酷。 （我之所以说「重新」，是因为在 1910 和 1920 年代，它曾是非常酷的学科。）
但是，让我获得 2002 年北京的菲尔兹奖的数学，却并非如此。
但是，当找到解答时，它是否就是解答却一点儿也不明确。
假设你想要解某个五次代数方程。 通过某些方法，你找到了方程的解， 然后你可以把根带入方程中，来检查解是否正确。
但是当你想要解一个有二十个二十次方程的方程组时， 或者想要解类似复杂的问题。 通过某些方法，你找到了方程的解， 但是此时想要检查解的正确性，就需要做很多计算了。
如今没人会想用纸和笔来徒手做这类计算了， 你会用到某些软件来帮助自己做验证。
再设想，你的问题是要证明某个定理。 你找到的解是一个证明。 如何验证证明是否正确呢？
关于什么才是严格的证明，你从老师或教授那里，学到了一些惯例与原则， 但是你还不能把你的证明提供给计算机，让计算机去帮你检查它。
找这个解答花了我两年的时间，从 1993 年到 1995 年。
1995 年，我开始着手「把证明写下来」。 1995 年六月的时候，我完成了第一个预印本。
译者注：「预印本 / Preprint」是数学论文发表之前，分发给同事和朋友看的版本。
但是，对我的 Milnor 猜想证明而言，这只是故事的开始。
你可以看到，真正的数学工作是如何随着时间演进而慢慢展开的。 理想情况下，就是「数学家证明定理」，但是你将看到真实情况是如何。
别忘了，我找到证明是在 1995 年，而我得菲尔兹奖是在 2002 年。
我找到的证明依赖于另一个猜想。 这个猜想本身也很酷，它连接了数学的两个领域， 这两个领域在当时看似还是远远分离的。
我也确信，我知道如何证明这个猜想，但是我知道要花很长时间。
然后，我开始想办法修改我的第一个证明， 让它能不依赖这个额外的猜想。 大约一年之后，我找到了办法。 我在 1996 年十二月写出了新的证明的预印本。 这个预印本中的证明，包含了所有的主要想法， 但是略去了很多细节。
之后，我花了七年的时间去补充这些细节， 以发表一个完整证明的论文⋯⋯
这个证明所依赖的想法，最终都证明是可靠的， 而且我所依赖的他人的工作成果，最终也都证明是正确的。
1987 我认识了 Mikhail Kapranov。 我那时是莫斯科大学的本科生，他是研究生。
我们马上就发现，我们都梦想着发展一种新的， 受高阶范畴论启发的「高维」数学。
和可以相互学习的人一起做数学， 同时又一起发现着，对你、对他、对整个世界来说，都是新的事物， 真是美妙而强有力的的经历。
1990 年夏天，经 Kapranov 的推荐， 我不用申请就被哈佛研究生院录取了。 1990 年秋天，我离开了苏联，开启了我生涯中在美国的时光⋯⋯
Kapranov 和我写了一篇关于新的「高维」数学中关键猜想的论文。 这个猜想是 亚历山大·格罗滕迪克（Alexander Grothendieck）提出的。
直觉告诉我们，无穷阶广群（infinity-groupoids） 可以构成 同伦类型（homotopy types）的特别合适的模型， n-阶广群（n-groupoids）对应 截断同伦类型（truncated homotopy types）
（其中 pi(i) = 0 对所有 i > n 成立）。
-- Esquisse d'un Programme 1984
译者注：法语 "Esquisse d'un Programme"，英译为 "Sketch of a Programme"，中译可作「计划概要」。 是 格罗滕迪克 关于远期数学研究的重要提案，直到现在还是很多数学研究灵感的来源。
这个猜想并非表达地很精确， 因为如何定义 无穷阶广群（infinity-groupoid）还是公开的问题。
Kapranov 和我认为，我们知道定义是什么， 也知道该如何根据我们的定义来证明这个猜想。
我们写了一篇论文来描述证明的概要， 并且发表到了俄国最好的数学期刊之一， 完整的证明发表在了我们受邀参加的会议的会议记录中。
译者注：「会议记录 / The proceedings of a conference」也可称为「学报」， 是学术界集会结束后发表的论文集，其中会包含演讲者的论文。
我们感到这个猜想相关的问题结束了， 并且「高维」数学中的这个重要元素被理解透彻了。
之后，2003 年，我们论文的英文版发表十二年后， 网络上出现了一个预印本，其中 Carlos Simpson 非常礼貌地宣布， 他构造出来了我们的定理的一个反例子。
我当时正忙于「主旨理论的项目 / The motivic program」， 并且确信我们的证明是正确的， 所以忽略了这个预印本。
之后，我生涯中 主旨理论（motivic）的时期告以段落， 我开始着手「计算机证明验证 / Computer proof verification」， 和「新数学基础 / New foundations of mathematics」相关的工作。
无穷阶广群 和 同伦类型 之间的联系重新浮现在眼前， 成了「单值性基础 / The Univalent Foundations」的基石。
之后，在 2013 年的秋天， 我感到我思想中的一些「路障」倒塌了， 我突然想通了 Carlos Simpson 是对的， 而 Kapranov 和我在 1991 年发表的证明是错的。
不光这个证明是错的，论文中的主要定理本身就是错的！
译者注：据译者所知，"Univalent" 这一术语并没有公认中文翻译。
Vladimir Voevodsky 自己解释这一术语的选择时说，
..., this fibration should still satisfy the "uniqueness" part of the definition of "universal" but not the "for all" part.
"Universal" 出现在范畴论的 "Universal property" 中，可以译为「泛」或「万有性」； 而在数学中 "Univalent" 也表达函数作为关系时的单值性，所以暂且译做「单值」。
论文中的主要定理是错的， 是就 Kapranov 和我使用的那种无穷阶广群的定义而言的。 如今已经有了多种其他的定义，而且就这些定义而言，主要定理是对的。
现在我们知道，在 单值性基础 中使用「格罗滕迪克一致性 / The Grothendieck correspondence」 并不会有什么损害。
译者注：所谓「格罗滕迪克一致性 / The Grothendieck correspondence」 就是上面提到的 格罗滕迪克 的猜想，即「无穷阶广群 与 同伦类型 是一致的」。
但是，在这些年间，「相信我们其实错误的定理是正确的」这件事， 在我认知「多维范畴论 / Multidimensional category theory」这个领域方面， 扮演了重要而负面的角色。
由于我相信了一些错误的东西， 我没法相信其他某些正确的东西， 因为它们是相互矛盾的。
当我意识到论文中的定理是错误的时， 我联系了 Kapranov，告诉他我们应该对论文做点儿什么， 并且我告诉了 Carlos Simpson，他 2003 年的预印本是正确的。
这个故事中有趣的一点是， Carlos Simpson 没有指出我们长达 10 页的论文中哪里错了。 他只是针对最终结论构造了反例，证明了它不可能是对的。
我花了几周的时间才找到论文中哪条引理是错的， 并且找到了那条引理的一个反例。
我们起初想要解答的问题，即「如何定义 无穷阶广群，使得 格罗滕迪克一致性 成立。」 仍然是选而未决的问题⋯⋯
Kapranov 和我找到了我们所关心的问题的解答，即，一个定理的证明。
如果问题是解一个方程， 而我们找到了一个解， 在发表结果之前，我们首先应该检查它确实是方程的解，对吗？
并且，如果这个方程很复杂，我们可能会用电脑来做检查。
那么，为什么当解是一个定理的某个证明的时候，我们就不能检查了呢？
早在十几年前我就开始自己问自己这个问题， 因为我所创造出来的解答，也就是证明，变得越来越复杂了， 而我越来越担心它们包含着某些错误。
尝试回答这个问题，领我走向了我现在的兴趣所在，即「数学基础 / Foundations of Mathematics」。
检查，在此时就是对这些数进行一些运算， 然后将计算结果与另外一些数所比较。
但是，当解是一个命题的证明时，我们应该怎么做验证呢？
还是解方程，但是这次要求符号形式的解。我们可以从这个问题上找到启发。
这时如何检查解呢？ 我们可能会用某些可以进行符号计算的软件， 它们不只是能对数进行计算， 也可以对带有变元的表达式进行计算。
译者注：「表达式 / Symbolic expression」或简称 "Expression"，是程序员所熟知的概念了。
所以，为了检查一个命题的证明， 我们需要把命题和证明都写成表达式， 设 T 为命题，A 为证明， 然后用某些软件，这些软件可以对这些表达式进行运算， 而这些计算就是检查 A 确实是 T 的证明。
将存在于我们思维中的命题与证明编码为表达式， 这个过程就叫做 「形式化 / Formalization」。
形式化，就像编程，首先是一种工具， 凭借这种工具，我们可以将我们需要做的脑力劳动交给电脑去做。
但是，如今形式化的发展还远远不如编程， 在 2003 年，当我开始寻找可以帮我检查我的证明的形式化系统时， 我甚至一个都找不到。
此时首先要回答的问题是，什么阻碍了前人创造这样的系统？
首先我们需要关于如何设计形式推演系统的知识， 推演系统之于数学的形式化，正如程序语言之于编程。
就我所知，形式推演系统的理论起源于，Gottlob Frege 的一篇令人拍案叫绝的论文， 叫做「模仿算术的纯思维的形式语言 / A formula language, modeled upon that of arithmetic, for pure thought」。
顺便说一句，它叫「理论 B」并不是因为它不如「理论 A」重要， 而是因为一本「理论计算机科学手册」，它是分两卷 "A" 和 "B" 出版的， 而关于形式推演系统的理论是在第二卷中讨论的。
「理论 A」在亚洲个许多国家，以及美国和以色列，更为人们所熟知。 它主要关心的是算法的复杂度。
这里 "B" 其实意味着它更难， 因为更简单的东西要在第一卷讨论， 而更难的东西在第二卷讨论。
译者注：Gottlob Frege 的「模仿算术的纯思维的形式语言」是一个极富影响力的名篇， 原德语言标题以 "Begriffsschrift" 开头，英译大致为 "concept-script"，中译为「概念文字」。
这篇之所以影响深远，在于它丰富的哲学背景， 以及它的形式系统能够成功地捕捉到很大一部分数学与自然语言。
但是，为了形式化数学命题与证明，关于形式推演系统的理论，也还只是拼图的一部分。
这个理论研究所有可能的形式推演系统。 至于一个系统是否形式地表达着某些实际的，思维领域的推理系统， 这个理论并不关心。
就像一般微分方程的理论，它研究所有的微分方程， 而不在乎某个微分方程是否描述着现实世界中的某些实际现象。
对于命题的检查而言，我们需要构造一个特殊形式推演系统， 然后解释它是如何与，存在于我们思维中的，数学的对象与推理形式相对应的，
构造这样的系统，并且将它的形式组件， 与我们数学思维世界中的对象和行动对应起来， 这就是这个叫做「数学基础 / Foundations of Mathematics」的领域的主要任务。
这就是数学基础的主旨所在， 它旨在连接 我们的思想世界 与 形式系统中的对象， 而形式系统可以帮助我们灵巧地使用我们的思想。
一个形式推演系统，外加一个对应关系， 这个对应关系连接了 形式推演系统的形式组件 与 我们数学思维世界中的对象和行动， 借由这二者，我们可以形式化所有数学的领域， 这就可以称作是「为数学而做的基本系统 / Foundational system for mathematics」 或者「数学基础 / Foundations of Mathematics」。
当我还在莫斯科大学的时候，人们可不是这样描述「数学基础」的。 人们描述它的方式非常不同，如果当时就能这样描述它， 我肯定会认为它非常非常酷，可惜当时不是。
如果你有一个系统可以给你公式， 并且这些公式对应于你对数的思考， 那么这个系统就是数的系统。
最早的类似数学基础的东西，就是各种数的系统， 它们使得人们能够写下数， 而数正是人们数学思维世界中的简单对象。
人们将数写做符号，并且通过操纵符号来进行计算， 而所算的，正是实际生活中各式各样关于数的东西。
比如说，如何计算「为了造给定大小的墙，需要多少块砖」。
今日的数学基础，也当是数的系统的某种类比， 只是，我们现在所处理的，数学思维中的对象，更加抽象了。
古典纯数学的主流基础， 叫做「Zermelo-Fraenkel 集合论 / Zermelo-Fraenkel Set Theory」 外加「选择公理 / The Axiom of Choice」，简称 ZFC， 这命名来自它所使用的「谓词演算 / Predicate logic」的公理系统。
ZFC 算是一个形式推演系统， 其中，建立数学对象与我们的思想之间的联系的方式，称作集合论数学。
这是「布尔巴基小组 / Bourbaki group」在诸多数学领域耕耘了很多年的东西。
它是二十世纪开头几十年的造物，那时计算机还不存在， 那时形式化实际的复杂证明也还不是紧要的问题。
在计算机之前，没人真的想过要形式化复杂的证明， 因为没有计算机的帮助这太难了。
部分是因为 ZFC 是为前计算机时代的数学而设计的， 它没能很好地适应二十一世纪的数学； 它也没能很好地适应计算机检查证明这个任务。
为了像检查方程的解一样，检查我的证明，我需要新的数学基础。
我在 2006 年想出了「单值性基础 / Univalent Foundations」中的主要想法。 只有一个缺失的元素，而我花了三年的时间才找到它。
在 2009 年秋天，我就「单值性模型 / Univalent model」做了第一个公开演讲， -- 一个数学构造，以一种新的，出乎意料的方式，连接了 Martin-Löf 的类型系统 与 ZFC。
2010 年春天，我意识到我有了一个可以使用的新形式系统， 它基于一个新的基础系统，我称其为「单值性基础 / Univalent Foundations」。
在 2012 到 2013 学年，在我就职的普林斯顿高等研究院， Thierry Coquand、Steve Awodey 和我，组织了一个特别项目。
在这一学年间，项目的参与者们一起写了一本书叫「同伦类型论 / Homotopy Type Theory」。
在 Google 里搜一下这些关键词，你会找到一个网站， 在里面你可以了解到更多关于这个新项目的信息，也可以免费下载这本书。
这本书是真真切切的集体劳动成果，因此它没有一个作者。 为这本书的问世贡献最多，并且持续塑造着这本书的内容与风格的人， 是 Michael Schulman。
2014 年 6 月 21 日，「单值性基础 / Univalent Foundations」迎来了另外一个重要的里程碑。 Thierry Coquand 就 单值性基础 在巴黎的「布尔巴基讨论班 / Bourbaki Seminar」做了演讲。 被选中在这个讨论班上做演讲，是受到世界数学界认可的重要标志。
Thierry 和他的同事，同时也是 单值性基础 问世之后的最重要进展的作者， 他们构造了另一个模型，类似最初 2009 年的「单值性模型 / Univalent model」， 但是是基于「构造主义数学 / Constructive mathematics」的。
这个模型为更广泛的，古典和构造主义数学的「单值性综合 / Univalent Synthesis」开辟了道路⋯⋯
但是，小小的，无聊的，充满了错误的故事却随时发生着。
这些小小的错误浪费我们的时间，并且当我们发现它们时，它们让我们狼狈不堪。
随着我们变得年长，变得更有名望，对这些错误的恐惧也在增长。 我们花费越來越多的时间，去在一遍一遍地检查我们的工作成果，而一点一点失去了尝试新事物的勇气。
在我的数学生涯中，没有这样一个故事，在其中一个错误毁掉了我工作的重要部分。
而随着数学变得越来越复杂，错误的重担，与对出错的畏惧，正在更进一步蹒跚着数学发展的脚步。
提问者 问了关于使用「辅助证明系统 / Proof assistants」的问题。
Voevodsky: 辅助证明系统可以极为有用，就像乐器一样，在没有老师的情况下，你也可以用它来练习。
提问者 问关于如何提高「数学感 / Mathematical sense」的问题。
Voevodsky: 通过做大量大量大量的细节证明与计算，日复一日，月复一月，年复一年。 尝试考察不同领域的数学，然后它们都将以某种方式在你的脑子里联系起来， 并且你将能够以一种更一般的观点去理解它们。
用这种「数学感」来寻找新的证明， 年轻的时候，我会花很多很多个小时， 在纸上写东西，思考，然后再写，并且喝很多浓茶， 来回踱步，让这些东西在我脑子不断盘旋着。
当我变得更年长了，我不再经常这么做了，或者说至少我尝试着不再这么做了。
我现在通常就是，尝试非常精确地表达一个问题，以保证它只有一个意义， 然后把这个问题放到我脑子里，让它在那老老实实待一段时间， 然后我忘了它，去做别的事，我等待着答案出现。
V.V. 的这篇演讲，是鼓励我坚持着我的程序语言项目的重要动力之一。
抛开演讲中，给人很多灵感和启发的数学内容不谈， V.V. 的演讲，真诚清晰，风趣幽默，魅力十足，是不是？
创造一个软件，同时也是一个语言， 让所有数学家可以用它完成其工作，让我们的生活更加简单， 用软件逐步验证证明中的步骤，以排除我们工作中的不确定性。