我是如何开始关心数学基础的
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. 的演讲,真诚清晰,风趣幽默,魅力十足,是不是?
创造一个软件,同时也是一个语言, 让所有数学家可以用它完成其工作,让我们的生活更加简单, 用软件逐步验证证明中的步骤,以排除我们工作中的不确定性。