「人物志」计算机将重新定义数学的根基吗？-Voevodsky
原文链接：QuantaMagazine
作者：凯文·哈特内特 (Kevin Hartnett) 2015年5月19日
当一位传奇数学家发现自己工作中的一个错误时，他踏上了一场由计算机辅助的探索之旅，旨在消除人为错误。为了成功，他必须重写支撑整个数学的百年规则。
数学正在新的基础上重建。 汉内斯·胡梅尔 为 Quanta Magazine 供图
最近一次从里昂到巴黎的火车旅程中，弗拉基米尔·沃埃沃德斯基（Vladimir Voevodsky）坐在史蒂夫·阿沃迪（Steve Awodey）旁边，试图说服他改变做数学的方式。
沃埃沃德斯基，48岁，是新泽西州普林斯顿高等研究院（IAS）的终身教员。他出生于莫斯科，但英语近乎完美，并且带着一种无需向任何人证明自己的自信风度。2002年，他荣获了菲尔兹奖，这通常被认为是数学界最负盛名的奖项。
如今，当他们的火车接近城市时，沃埃沃德斯基拿出他的笔记本电脑，打开了一个名为Coq的程序——一个为数学家提供编写数学论证环境的证明助手。阿沃迪是宾夕法尼亚州匹兹堡卡内基梅隆大学的数学家和逻辑学家，他跟着沃埃沃德斯基，看他使用自己创建的一种称为“单值基础”（univalent foundations）的新形式体系来编写一个数学对象的定义。沃埃沃德斯基花了15分钟写完这个定义。
“我当时试图说服[阿沃迪]在Coq中进行[他的数学研究]，”沃埃沃德斯基在去年秋天的一次讲座中解释道。“我想让他相信这很容易做到。”
在像Coq这样的程序中进行数学研究的想法由来已久。其吸引力很简单：与其依赖容易出错的人类来检查证明，不如将这项工作交给计算机，计算机能够以完全的确定性判断一个证明是否正确。尽管有这个优势，计算机证明助手并未在主流数学界得到广泛采用。部分原因是将日常数学翻译成计算机能理解的术语既繁琐，而且在许多数学家看来，不值得付出这样的努力。
近十年来，沃埃沃德斯基一直在倡导计算机证明助手的优点，并发展单值基础，以便将数学语言和计算机编程语言更紧密地结合起来。在他看来，转向计算机形式化是必要的，因为某些数学分支已经变得过于抽象，以至于人类无法可靠地进行检查。
“数学世界正变得非常庞大，数学的复杂性正变得非常高，存在错误累积的风险，”沃埃沃德斯基说。证明依赖于其他证明；如果一个证明包含缺陷，所有依赖于它的其他证明都会带有这个错误。
这是沃埃沃德斯基通过个人经历学到的。1999年，他发现自己七年前写的一篇论文中存在一个错误。沃埃沃德斯基最终找到了挽救结果的方法，但在去年夏天IAS通讯的一篇文章中，他写道这次经历让他感到恐惧。他开始担心，除非他在计算机上形式化自己的工作，否则他无法完全确信它是正确的。
但要迈出这一步，需要他重新思考数学的基础。公认的数学基础是集合论。像任何基础系统一样，集合论提供了一系列基本概念和规则，可以用来构建数学的其余部分。集合论作为基础已经足够使用了一个多世纪，但它不能轻易地转换成计算机可用来检查证明的形式。因此，随着他决定开始在计算机上形式化数学，沃埃沃德斯基启动了一个发现过程，最终导致了一个更宏伟的目标：重塑数学的基础。
集合论与一个悖论
集合论源于一种将数学置于完全严格基础上的冲动——一个比数字本身更安全的逻辑基础。集合论始于包含“无”的集合——空集——它被用来定义数字零。然后可以通过定义一个包含一个元素（空集）的新集合来构建数字1。数字2是包含两个元素（空集(0)和包含空集的集合(1)）的集合。通过这种方式，每个整数都可以被定义为它之前所有集合的集合。
集合论通过从字面上的“无”（空集，定义为零）开始构建所有数学。包含单个元素（空集）的集合成为数字1，包含两个元素（空集和包含空集的集合）的集合成为数字2，依此类推。 奥莱娜·什马哈洛/Quanta Magazine 供图
一旦整数就位，分数可以定义为整数对，小数可以定义为数字序列，平面上的函数可以定义为有序对的集合，等等。“你最终会得到复杂的结构，它们是一些事物的集合，而这些事物又是一些事物的集合，再往下又是一些事物的集合，一直追溯到底层的空集，”圣地亚哥大学的数学家迈克尔·舒尔曼（Michael Shulman）说。
作为基础的集合论包括这些基本对象——集合——以及操作这些集合的逻辑规则，数学中的定理就是从中推导出来的。集合论作为基础系统的一个优点是它非常经济——数学家可能想要使用的每个对象最终都是由空集构建的。
另一方面，将复杂的数学对象编码为精心设计的集合层级可能很乏味。当数学家想要考虑在某种意义上等价或同构，但不一定在所有方面都相等的对象时，这个限制就成问题了。例如，分数½和十进制数0.5代表同一个实数，但在集合论术语中它们的编码方式却大相径庭。
“你必须构建一个特定的对象，然后就被它束缚住了，”阿沃迪说。“如果你想使用一个不同但同构的对象，你就必须重新构建那个对象。”
但集合论并不是做数学的唯一方法。例如，证明助手程序Coq和Agda是基于一种称为类型论的不同形式系统。
类型论起源于修复早期集合论版本中的一个关键缺陷的尝试，该缺陷由哲学家和逻辑学家伯特兰·罗素（Bertrand Russell）于1901年发现。罗素注意到有些集合包含自身作为成员。例如，考虑所有不是宇宙飞船的事物的集合。这个集合——非宇宙飞船的集合——本身就不是宇宙飞船，所以它是自身的成员。
罗素定义了一个新集合：所有不包含自身作为成员的集合的集合。他问这个集合是否包含自身，并证明回答这个问题会导致一个悖论：如果该集合包含自身，那么它就不包含自身（因为该集合中唯一的对象是不包含自身的集合）。但如果它不包含自身，那么它就包含自身（因为该集合包含了所有不包含自身的集合）。
罗素创建了类型论作为摆脱这个悖论的方法。罗素的系统使用更仔细定义的对象，称为“类型”，来代替集合论。罗素的类型论像集合论一样，从一个对象宇宙开始，这些对象可以被收集在一个称为SET的“类型”中。在类型论内部，SET类型被定义为只允许收集那些本身不是其他事物集合的对象。如果一个集合确实包含其他集合，它就不再被允许是一个SET，而是变成了可以被认为是MEGASET的东西——一种新类型的类型，专门定义为自身是对象集合的对象集合。
由此，整个系统以有序的方式产生。人们可以想象，比如说，一个叫做SUPERMEGASET的类型，它只收集那些是MEGASETS的对象。在这个严格的框架内，可以说，甚至提出这个引发悖论的问题——“所有不包含自身作为成员的集合的集合是否包含自身？”——也变得不合法了。在类型论中，SETS只包含那些不是其他对象集合的对象。
集合论和类型论之间的一个重要区别在于处理定理的方式。在集合论中，定理本身不是一个集合——它是关于集合的陈述。相比之下，在某些版本的类型论中，定理和SETS处于同等地位。它们都是“类型”——一种新的数学对象。一个定理是这样一个类型，其元素是该定理所有不同的证明方法。因此，例如，存在一个单一的类型，它收集了勾股定理的所有证明。
为了说明集合论和类型论之间的这种差异，考虑两个集合：集合A包含两个苹果，集合B包含两个橘子。数学家可能会认为这些集合是等价的，或同构的，因为它们包含相同数量的对象。形式上证明这两个集合等价的方法是将第一个集合的对象与第二个集合的对象配对。如果它们能均匀配对，两边都没有剩余的对象，那么它们就是等价的。
当你进行这种配对时，你很快会看到有两种方法可以证明等价性：苹果1可以与橘子1配对，苹果2与橘子2配对；或者苹果1可以与橘子2配对，苹果2与橘子1配对。另一种说法是，这两个集合以两种方式相互同构。
在定理“集合A ≅ 集合B”（其中符号≅表示“同构于”）的传统集合论证明中，数学家只关心是否存在这样一种配对。在类型论中，定理“集合A ≅ 集合B”可以被解释为一个集合，包含了所有证明同构的不同方式（在这种情况下是两种）。在数学中，通常有充分的理由去追踪两个对象（如此处的两个集合）等价的各种方式，而类型论通过将等价关系捆绑到一个单一类型中来自动完成此操作。
这在拓扑学中尤其有用，拓扑学是研究空间（如圆或甜甜圈表面）内在属性的数学分支。如果拓扑学家必须分别考虑具有相同内在属性的空间的所有可能变体，那么研究空间将是不切实际的。（例如，圆可以有任何大小，但每个圆都具有相同的基本性质。）一种解决方案是通过认为其中一些空间是等价的来减少不同空间的数量。拓扑学家这样做的一种方式是使用同伦（homotopy）的概念，它提供了一个有用的等价定义：如果粗略地说，一个空间可以通过收缩或加厚区域而不撕裂地变形为另一个空间，那么这两个空间就是同伦等价的。
点和线是同伦等价的，这也是说它们属于相同同伦类型的另一种方式。字母P与字母O属于相同的同伦类型（P的尾巴可以收缩到字母上部圆边界上的一个点），并且P和O都与字母表中包含一个孔的其他字母——A、D、Q和R——属于相同的同伦类型。
拓扑学家使用不同的方法来评估空间的性质并确定其同伦类型。一种方法是研究空间中不同点之间的路径集合，而类型论非常适合追踪这些路径。例如，拓扑学家可能会认为空间中的两个点只要有路径连接它们就是等价的。那么，点x和y之间的所有路径的集合本身可以被视为一个单一类型，它代表了定理x = y的所有证明。
同伦类型可以由点之间的路径构建，但一个有进取心的数学家也可以追踪路径之间的路径，以及路径之间的路径之间的路径，等等。这些路径之间的路径可以被认为是空间中点之间更高阶的关系。
从20世纪80年代中期在莫斯科国立大学读本科开始，沃埃沃德斯基断断续续尝试了20年，试图以一种能使这些更高阶关系——路径的路径的路径——易于处理的方式来形式化数学。像这一时期的许多其他人一样，他试图在一个称为范畴论（category theory）的形式系统框架内完成这项工作。虽然他在使用范畴论形式化数学的特定领域取得了一些有限的成功，但仍有一些数学领域是范畴论无法触及的。
在获得菲尔兹奖后的几年里，沃埃沃德斯基带着新的兴趣回到了研究更高阶关系的问题上。2005年底，他有了一次顿悟。他说，一旦他开始从称为无穷广群（infinity-groupoids）的对象的角度思考更高阶关系，“许多事情就开始豁然开朗了。”
无穷广群编码了一个空间中的所有路径，包括路径的路径，以及路径的路径的路径。它们在数学研究的其他前沿领域也作为编码类似更高阶关系的方式出现，但从集合论的角度来看，它们是笨拙的对象。正因为如此，它们被认为对于沃埃沃德斯基形式化数学的目标是无用的。
然而，沃埃沃德斯基成功地用无穷广群的语言创建了类型论的一种解释，这一进展使得数学家能够有效地推理无穷广群，而无需再从集合的角度去思考它们。这一进展最终导致了单值基础的发展。
沃埃沃德斯基对建立在广群上的形式系统的潜力感到兴奋，但也对实现这一想法所需的大量技术工作感到畏惧。他还担心他取得的任何进展都会过于复杂，以至于无法通过同行评审可靠地验证，沃埃沃德斯基说他当时正对同行评审“失去信心”。
迈向新的基础系统
有了广群，沃埃沃德斯基有了他的对象，这让他只需要一个形式框架来组织它们。2005年，他在一篇名为FOLDS的未发表论文中找到了它，这篇论文向沃埃沃德斯基介绍了一个与他想要实践的那种更高阶数学惊人地契合的形式系统。
1972年，瑞典逻辑学家佩尔·马丁-洛夫（Per Martin-Löf）受到Automath（一种用于在计算机上检查证明的形式语言）思想的启发，引入了他自己版本的类型论。马丁-洛夫类型论（MLTT）被计算机科学家们急切地采用，并将其用作证明助手程序的基础。
在20世纪90年代中期，当专门研究数理逻辑、于2010年从麦吉尔大学退休的迈克尔·马凯（Michael Makkai）意识到MLTT可能被用来形式化范畴论和高阶范畴论数学时，MLTT与纯数学产生了交集。沃埃沃德斯基说，当他第一次读到马凯在FOLDS中阐述的工作时，那种体验“几乎像是在和自己对话，是好的那种感觉。”
弗拉基米尔·沃埃沃德斯基的单值基础项目旨在以一种允许计算机检查所有数学证明的方式重建数学。 安德里亚·凯恩/普林斯顿高等研究院 供图
沃埃沃德斯基沿着马凯的路径前进，但使用了广群而不是范畴。这使他能够在同伦理论和类型论之间建立起深刻的联系。
“这是最神奇的事情之一，不知何故，这些程序员真的想要形式化[类型论]，”舒尔曼说，“结果他们最终形式化了同伦理论。”
沃埃沃德斯基同意这种联系是神奇的，尽管他看待其意义的方式略有不同。对他来说，由同伦理论启发的类型论的真正潜力在于，它作为一个新的数学基础，既特别适合计算机化验证，又特别适合研究更高阶关系。
沃埃沃德斯基在阅读马凯的论文时首次意识到这种联系，但他又花了四年时间才使其在数学上精确化。从2005年到2009年，沃埃沃德斯基开发了几套机制，使数学家能够“首次以一致且便捷的方式”在MLTT中处理集合，他说。这些机制包括一个被称为单值公理（univalence axiom）的新公理，以及用单纯集（simplicial sets）语言对MLTT的完整解释，单纯集（除了广群之外）是表示同伦类型的另一种方式。
伊利诺伊大学厄巴纳-香槟分校的数学荣休教授丹尼尔·格雷森（Daniel Grayson）说，这种一致性和便捷性反映了该项目更深层次的东西。单值基础的力量在于它触及了数学中一个先前隐藏的结构。
“关于[单值基础]吸引人且与众不同之处，特别是如果你开始将其视为取代集合论的话，”他说，“在于它似乎将拓扑学的思想引入了数学的最基础部分。”
从想法到行动
为数学建立一个新的基础是一回事。让人们使用它是另一回事。到2009年底，沃埃沃德斯基已经完善了单值基础的细节，并准备开始分享他的想法。他明白人们很可能会持怀疑态度。“声称我拥有某种或许应该取代集合论的东西，这是一件大事，”他说。
沃埃沃德斯基首次公开讨论单值基础是在2010年初在卡内基梅隆大学以及2011年在德国奥伯沃尔法赫数学研究所的讲座中。在卡内基梅隆的讲座上，他遇到了史蒂夫·阿沃迪，阿沃迪当时正与他的研究生迈克尔·沃伦（Michael Warren）和彼得·拉姆斯代恩（Peter Lumsdaine）一起研究同伦类型论。不久之后，沃埃沃德斯基决定召集研究人员进行一段时间的密集合作，以推动该领域的发展。
与瑞典哥德堡大学的计算机科学家蒂埃里·科康（Thierry Coquand）一起，沃埃沃德斯基和阿沃迪组织了一个特别研究年，于2012-2013学年在IAS举行。来自世界各地的三十多位计算机科学家、逻辑学家和数学家参与其中。沃埃沃德斯基说，他们讨论的想法是如此奇特，以至于一开始，“没有一个人对此感到完全自在。”
这些想法可能有些陌生，但它们也令人兴奋。舒尔曼推迟了一份新工作的开始时间，以便参与该项目。“我想我们很多人都觉得我们正处在一个重大事件的 cusp（尖端、开端）上，一件真正重要的事情，”他说，“为了参与它的起源，值得做出一些牺牲。”
特别研究年之后，活动分化为几个不同的方向。一个研究小组，包括舒尔曼，被称为HoTT社区（代表同伦类型论，homotopy type theory），开始探索在他们开发的框架内进行新发现的可能性。另一个小组，自称为UniMath，包括沃埃沃德斯基，开始用单值基础的语言重写数学。他们的目标是创建一个基础数学元素的库——引理、证明、命题——数学家可以用它来形式化自己在单值基础中的工作。
随着HoTT和UniMath社区的发展，它们背后的思想在数学家、逻辑学家和计算机科学家中变得更加引人注目。宾夕法尼亚大学的逻辑学家亨利·托斯纳（Henry Towsner）说，如今他参加的每一次会议上似乎至少有一个关于同伦类型论的报告，而且他越了解这种方法，就越觉得它有道理。“它曾经是个时髦词，”他说。“我花了一段时间才明白他们真正在做什么，以及为什么它既有趣又是个好主意，而不是一种花哨的东西。”
单值基础受到的许多关注归功于沃埃沃德斯基作为他那一代最伟大数学家之一的地位。哥伦比亚大学的数学家迈克尔·哈里斯（Michael Harris）在他的新书《无需道歉的数学》（Mathematics Without Apologies）中对单值基础进行了长篇讨论。他对围绕单值模型的数学印象深刻，但他对沃埃沃德斯基更宏大的愿景——一个所有数学家都用单值基础形式化他们的工作并在计算机上检查的世界——持更怀疑的态度。
“据我所知，推动证明和证明验证机械化的动力并没有强烈地激励大多数数学家，”他说。“我能理解为什么计算机科学家和逻辑学家会感到兴奋，但我认为数学家在寻找别的东西。”
沃埃沃德斯基意识到，为数学提供一个新的基础是一件难以推销的事情，他承认“目前确实是炒作和喧嚣多于该领域实际准备好的程度。”他目前正在使用单值基础的语言来形式化MLTT和同伦理论之间的关系，他认为这是该领域发展的必要下一步。沃埃沃德斯基还计划形式化他证明米尔诺猜想（Milnor conjecture）的过程，这是他获得菲尔兹奖的成就。他希望这样做可以成为“一个可用来在该领域创造动力的里程碑。”
沃埃沃德斯基最终希望使用单值基础来研究在集合论框架内无法触及的数学方面。但目前他正谨慎地推进单值基础的发展。集合论支撑数学已有一个多世纪，如果单值基础想要拥有类似的寿命，沃埃沃德斯基知道从一开始就把事情做对是很重要的。
本文转载于Wired.com。