#Voevodsky | 单一基础的源起——为避免数学错误而发展计算机验证证明的个人使命

##meta

公众号 和乐数学

作者 Vladimir Voevodsky
译者 邓文超，中国科学院大学基础数学硕士研究生。

Vladimir Voevodsky 在 2002 年作为教授加入 IAS 数学系，他因在概型的同伦理论，代数 K 理论和代数几何与代数拓扑交叉部分的工作而知名。他对代数簇发展了新的上同调理论，这是过去几十年来代数几何最突出的进展。他的工作直接导致了 Milnor 猜想和 Bloch-Kato 猜想的解决。

##exceprts

现有的基础系统主要有两个导致其不合乎需要的问题。第一，现有的数学基础是基于谓词逻辑的语言，但是这种类型的语言限制性太大。第二，现有的基础不能被用来直接表达有些对象，比如我在 2-理论工作中的某些对象。

单一基础是一个完备的基础系统，相比范畴论，它更像 ZFC，但它和 ZFC 是非常不同的。为了作比较，我假设任何既适合人类推理又适合计算机验证的的数学基础应该包含下面这三个部分。
第一部分是形式推导系统：包括一种语言和用这种语言操作纯粹形式化语句的规则，使得这些操作可以被计算机程序检验。第二部分是一个结构，这个结构要能对这种语言中的语句给出人类头脑可直觉感知的对象。第三部分是另一个结构，这个结构帮助人们理解直接与这种语言相联系的数学想法

##content

Alexander Grothendieck 在 1984 年 1 月向法国国家科学研究中心提交了他的项目申请书“Esquisse d’un Programme”。这份文稿很快就在数学圈里传阅。几个月后，我的第一位学术研究导师 George Shabat 也给了我一份，当时我是莫斯科大学的一年级本科生。为了读它，我专门学了一些法语，之后我开始阅读并努力理解其中的想法。

我在1988 或1989 年遇到了 Michael Kapranov, 他也对发展数学中新的“高维”对象的想法极感兴趣，这些想法来自范畴和 2-范畴理论的启发。我们合作发表的第一篇论文是《无穷广群是同伦范畴的一个模型》（ -Groupoids as a Model for a Homotopy Category）。在文中，我们想要提供一个严格的数学形式化和对 Grothendieck 的某个想法的证明，Grothendieck 的这个想法意图联系 -广群和同伦型这两类数学对象。

接着，我们想可以将相似的想法应用到另一个那时的顶尖数学难题：构造 motivic 上同调，Alexander Beilinson, Robert MacPherson(现在是IAS的数学系教授) 和 Vadim Schechtman 在 1987 年合作的一篇论文中猜想这个数学对象是存在的。

Kapranov 在 1990 年夏天安排我免申请进入哈佛大学研究生院。几个月之后，他在康奈尔，我在哈佛，我们的数学道路有了分歧。我集中精力于 motivic 上同调和后来的 motivic 同伦论。1991 年 3 月 29 日我的笔记开头是一个问题：“什么是代数簇或概型的同伦论？”

motivic 上同调在那时被认为仅仅是个猜测，还缺乏坚实的基础。Spencer Bloch 在 1986 年的突破性论文《代数循环和高阶 K 理论》（Algebraic Cycles and Higher K-theory）也很快被 Andrei Suslin 发现在引理 1.1 的证明中包含一个错误。这个证明无法被修复，于是论文中的几乎所有论断都无法被证明。

一个新的证明直到 1993 年才公布，这个新证明用 30 页的复杂讨论替换原来论文中的一段。有趣的是，这个新的证明是基于 Mark Spivakovsky 的一个旧有的结果。Mark Spivakovshy 在那时也宣布了奇点消解猜想的证明。不过，Spivakovshy 的证明在多年后被发现包含一个错误，所以奇点消解猜想现在仍是公开问题。

我、Andrei Suslin 和 Eric Friedlander 发展的通往 motivic 上同调的路径通过我的论文《带有转移的预层的上同调理论》“Cohomological Theory of Presheaves with Transfers”回避了 Bloch 的那个引理，这篇论文是我作为IAS成员时在 1992-1993 年完成的。1999-2000 年，同样是在 IAS，我给了一个系列讲座，Pierre Deligne（IAS数学系教授）当时在做笔记并检查我的每一个步骤。正是这样，我发现论文中的一个关键引理的证明包含一个错误，并且这个错误无法修补。幸运的是，我后来证明了一个稍弱但更复杂的引理，这个引理对论文中的应用是充分的。于是，在 2006 年，正确的论证发表了出来。

这段故事让我觉得后怕。从 1993 年开始，很多数学家群体在讨论班上研究了我的论文，并将其应用到他们的工作之中，但是没有人注意到这个错误。这当然不是一个容易避免的事情。因为这个由一位被信任的作者给出的技术性讨论本身就感觉像是正确的而不容易被很细心地检查出来。

但是这并不是数学文本中的错误一直存在的唯一问题。1998 年 10 月，Carlos Simpson 向 arXiv 预印本文库提交了一篇论文——《严格3-广群的同伦型》（Homotopy Types of Strict 3-groupoids）。这篇论文中的论证表明 Kapranov 和我在 1989 年发表的那篇关于“-广群”的论文中的主要结果是不正确的。然而，Kapranov 和我也曾想过类似的批评，并且相信这样的批评不成立。一直到 2013 年的秋天，我才确定我们俩是正确的。

我发现导致这种反常情况出现的两个因素：Simpson 声称构造出了一个反例，但是他没有找出我们论文中的错误。故而，我们并不清楚到底是我们论文中有错误还是他在构造反例的时候出了错。现在的数学研究依赖一个基于数学声誉的复杂互信系统。Simpson 的论文出现的那时，Kapranov 和我都有很好的数学声誉。Simpson 的论文对我们的结果产生了怀疑，这导致它不被其他研究者使用，但是没有人继续前进并向我们在这个问题上提出异议。

在我发现我的 motivic 上同调论文中的错误时，我正在发展新的理论，我称之为 2-理论。在我考虑这些想法的时候，我越来越不确定应该怎么推进。2-理论的数学正是 Kapranov 和我在 1989 年梦想的那种高维数学。我非常享受发现了并不是低维结构直接推广的新的高维结构。

但是想要达到我觉得必要的那种严格和精确程度需要花费大量的精力，并且会产生一篇很难阅读的论文。谁能保证我不会忘掉什么或者犯个什么错误呢，甚至某个很简单的论证中的错误都有可能在多年后才被发现。我想正是在这个时候，我停止了去做那种“好奇心驱动型研究”，转而开始严肃地考虑未来。我并没有能探索好奇心带领到达的有价值的、有趣的并且很优美地方的工具。

所以，我开始考虑我能不能造出这样的工具。很快我就明白解决的途径就是用计算机去验证我的那些抽象的、逻辑的和数学的构造。这样的软件从六十年代起就在发展。但当我在 2000 年左右寻找这样一个实用的证明辅助软件时，我并没有找到。有好几个课题组在做这样的软件，但没有一个符合我那种数学的需求。

当我第一次开始探索这种可能性的时候，机器验证证明还几乎是一个在数学家群体里被禁止的主题。对机器验证证明的讨论无疑会导向 Gödel 不完备性定理（这个定理对实际问题没有任何用处）或者有一两个例子对已有的证明进行了验证，这只能表明机器验证证明这个想法的不实用性。

Tom Hales 和 Carlos Simpson 是那时坚持尝试发展数学中的机器验证的少数数学家。几年后的现在，证明和数学推理的机器验证对许多工作在单一基础（univalent foundations）和同伦型理论(homotopy type theory)领域的数学家来说，基本上看起来完全可行了。

最核心的待解决的挑战是现有的数学基础达不到做这件事的要求。用一种足够精确使得计算机可以理解的语言形成数学推理意味着不仅将使用数学的基础系统作为建立一些基本定理的一致性准则，还将其作为一个可以被使用到日常数学工作中的工具。现有的基础系统主要有两个导致其不合乎需要的问题。第一，现有的数学基础是基于谓词逻辑的语言，但是这种类型的语言限制性太大。第二，现有的基础不能被用来直接表达有些对象，比如我在 2-理论工作中的某些对象。

不过，要接受数学需要一个全新的基础这一观点仍然是十分困难的。即使很多直接接触同伦型理论的人也不容易接受这个想法。一个原因是：现有的数学基础——ZFC 和范畴论——已经十分成功。我很倾向于用范畴论作为新的数学基础。

故事从 ZFC 开始：Zermelo-Fraenkel 理论和选择公理。从二十世纪的前半叶开始，数学就成为一个基于 ZFC 的科学，ZFC 是作为谓词逻辑中的一个特殊理论引进的。所以，想要接触数学底层的人有一条简单的路——学习什么是谓词逻辑，然后学习一种叫做 ZFC 的特殊理论，然后学习如何将涉及一些基本数学概念的命题翻译成 ZFC 中的公式，然后通过例子学习去相信其余的数学都可以化约到这些基本的概念。

这种情形对数学是十分有益的，正是它促成了二十世纪抽象数学的成功。历史上，ZFC 的第一个问题从早期布尔巴基宏伟事业的衰落中就可以看到，这个衰落是由于二十世纪后半叶的中心方法是范畴论，但是范畴论在 ZFC 框架里不太好表达。范畴论的成功使得人们觉得范畴是“下一个维度中的集合”，数学的基础应该是范畴论或者它的高维类似物。

对我来说最大的路障就是这个“范畴是下一个维度中的集合”。我清楚地记得我明白这个观点是错误的的时候的感觉。范畴不是“下一个维度中的集合”，他们是“下一个维度中的偏序集”，而“下一个维度中的集合”是广群。

这种“广群”和“范畴”的新看法对我来说需要一些调整，我记得教我数学的人们强调过一件事: Grothendieck 处理代数几何的方法会如此成功的一个原因就是他和旧有的做法决裂了，他坚持认为考虑所有的态射而不仅仅是同构是重要的。（广群经常是由集合级别的对象和它们之间的同构造出来的，而范畴常是由集合级别的对象和所有的态射造出来的。）

单一基础是一个完备的基础系统，相比范畴论，它更像 ZFC，但它和 ZFC 是非常不同的。为了作比较，我假设任何既适合人类推理又适合计算机验证的的数学基础应该包含下面这三个部分。

第一部分是形式推导系统：包括一种语言和用这种语言操作纯粹形式化语句的规则，使得这些操作可以被计算机程序检验。第二部分是一个结构，这个结构要能对这种语言中的语句给出人类头脑可直觉感知的对象。第三部分是另一个结构，这个结构帮助人们理解直接与这种语言相联系的数学想法。

在基于 ZFC 的数学基础中，第一组成部分有两“层”。第一层是建立推理系统的通用机制，叫做谓词逻辑；第二层是叫做 ZFC 的具体的推理系统，这是通过将通用机制应用到一些操作和公理上得到的。ZFC 的第二组成部分是基于人类自然感知层次体系的能力。实际上，ZFC 公理可以看作是所有层次体系满足的性质，再加上无穷公理，而无穷公理就是假定无穷层次体系是存在的。第三组成部分是根据层次体系翻译数学概念，这些层次体系开始于集合的数学性质的编制规则。这就是 ZFC 经常被称为集合论的原因。

单一基础最初的形式演绎系统叫做归纳构造演算，即 CIC(calculus of inductive construction)。这是 Thierry Coquand 和 Christine Pauline 在大约 1988 年发展的，是基于计算机语言理论和实践里的想法以及构造数学里的想法。这些想法的主要贡献者有 Nicolaas Govert de Bruijn, Per Martin-Löf 和 Jean-Yves Girard。证明辅助形式演绎系统 Coq 就是 CIC 的一个直接产物。

单一基础的第二组成部分，给 CIC 的语句提供直接含义的结构是基于单一模型的。直接与 CIC 的语句相联系的对象被称之为同伦型。同伦型的世界是被我们称之为 h-级的东西分层的，1 h-级的型对应命题，2 h-级的型对应集合。我们关于高阶级的直觉大部分来自它们和高维形状的关系，这些是基于 ZFC 的数学考虑了几十年的事情。

单一基础的第三组成部分，用同伦型翻译一般数学概念的途径，是基于 Grothendieck 在 70 年代后期的想法的反向考虑，这在我们的“-广群”论文中进行过讨论。不论从数学上还是哲学上来讲，这块都是该理论最深和最少被理解的部分。

我从 2005 年开始到现在就一直在考虑这些引导发现单一模型的想法，并且于 2009 年 11 月在 Ludwig-Maximilians-Universität München 做了关于此主题的第一个公开报告。当我独立构建模型的时候，这个方向的一些进展从 1995 年就开始了，主要是 Martin Hofmann, Thomas Streicher, Steve Awodey, 和 Michael Warren 在做。

我在 2010 年春天向 IAS 数学系建议在 2012-2013 年组织一个关于新的数学基础的特殊项目，尽管在那时仍然不清楚这个领域是否准备好这样一次研讨。

现在我已经可以在我的证明辅助的帮助下做数学了。虽然这个证明辅助还有待完善，但至少我现在不用担心所做数学工作中会包含错误了。现在做数学时，我能知道我真的做了什么，不用反复检查，也不用担心我的讨论是否太过复杂，也不用担心如何说服别人相信我的论证是正确的。我只需要相信计算机就好。现在有很多计算机科学的人在参与我们的项目，但是大部分数学家仍然不相信这是一个好想法，我觉得这是很不正确的。

感谢所有尝试去理解单一基础，发展这些想法和与别人交流这些想法的人们。

推荐参考：Vladimir Voevodsky 于 2012-2013 年在研究院组织的关于单一基础的特殊项目里二十多位数学家一起在六个月内写了一本六百多页的参考书。这本书可从 http://suo.im/5ikLSg 免费获取。这篇文章来自 Voevodsky 在三月份的一个报告，当时的录像可在 http://suo.im/4GJfAm 查看。