V.Ladimir Voevodsky在闪闪发光的桌子上没有坐下来，为新泽西州普林斯顿的杰出高级学习研究所为一个晚宴，比他翻倒了他的空酒杯，翻转杆上，站在其边缘上的玻璃-a给服务员的信号，他不会被吸收。他并不总是如此积极，但2013年下降的voevodsky是在一些严肃的工作中。
该研究所成立于1930年，被称为“数学和理论物理的尘世殿堂”，是各种严谨的智力探索的中心。爱因斯坦的老房子就在拐角处。停车场里，一辆车的保险杠上写着“不要相信你想的一切”——这很可能是直接针对沃渥斯基的。因为在过去十年左右的职业自我反省过程中，他意识到一个数学家的工作是5%的创造性洞察力和95%的自我验证。而在晚宴前后，最近的一项发现进一步证实了这一点:他犯了一个大错误。
B.沃渥德斯基在很大程度上是自己对数学产生了兴趣——最初是因为他想了解物理，后来因为他出乎意料地爱上了抽象代数。他不喜欢学术界的繁文缛节，也不去上课，用他自己的话说，他是莫斯科国立大学的“乡巴族”。1989年共产主义垮台后，他从未完成本科数学学位也就无关紧要了。他与数学家尤里·沙巴特(Yuri Shabat)和米沙·卡普兰诺夫(Misha Kapranov)一起工作和出版，建立了自己的资历。他和Kapranov对发展新的高维物体和类别的数学有着共同的热情，他们在1990年发表了一项重要的结果。
在卡普拉诺夫的推荐下，沃渥德斯基甚至没有申请就被哈佛大学录取了。1992年，他的博士论文标志着代数几何学思路的开始，10年后，他获得了菲尔兹奖，也就是所谓的数学诺贝尔奖。而在此之前的一年，也就是2001年，年仅36岁的他就成为了该研究所的正教授(自1998年以来，他一直是该研究所的长期成员)，该研究所是最受尊敬的知识圣殿。
神经元与星系网络的奇异相似性
意识和人脑研究领域的领军人物克里斯多夫·科赫(Christof Koch)曾说过，大脑是“已知宇宙中最复杂的物体”。不难看出为什么这可能是真的。有一千亿个神经元和…阅读更多
但是，他在路上遇到了一条凹凸。1998年，美国数学家Carlos Simpson发布了一篇论文，表明Voevodsky和Kapranov的1990年结果可能存在错误。多年来，Voevodsky通过细节筛选而不进行很大进展。他仍然相信结果是对的。然后，在2013年秋天，随着叶子改变了色彩和夏天，给秋天走向秋天，他取得了突破。各种各样的。他确认了错误。重要结果不再是如此重要。
“这显然是错误的。主要定理是错误的，”他说。“这并不是说证据有什么漏洞。主要定理显然是错误的。”他解释说，错误在于没有对显而易见的问题提出质疑。“我们已经证明了一个断言在所有困难的情况下确实是正确的，但在简单的情况下却是错误的。我们都懒得去核实。”为了确认这个错误，他在他的官方出版物列表中添加了一个附录——“警告:这篇论文的主要定理被卡洛斯·辛普森证明是错误的。”
但即使是在澄清这件事并作出弥补时，更广泛的影响也让他感到不安。这一错误在发生25年后才被确认。这是他发表的工作中发现了第二次错误。纸纸中的另一个错误是广泛读取和讨论的，并在不断发展的领域中互相应用。幸运的是，它是一个较小的错误，很容易被路由。Voevodsky通过构建与所有相同的有趣和重要定理的不同路线来纠正它。1
对于大多数人来说，电脑只是一个工具，如真空吸尘器。对我来说，它就像一位同事。
页边距还不错，大约60篇论文中有两个错误。尽管如此，他还是觉得这很麻烦。这显然不是一个意外，就像Voevodsky自己很快指出的那样，在一场关于他在其间的几年里至少给过十几次的困境的谈话中，他决心传达他的担忧。这是一篇复杂的论文。这类报纸的读者基本上会变得懒惰。“由可信作者撰写的技术论证很难验证，而且看起来与已知正确的论证相似，很少会被详细验证。”
对大规模对数学的影响是什么？
“我很担心，”他说。担心，害怕。从同一时间同时确认了错误，他也在致力于新的和令人兴奋的东西 - 他称之为“2理论”，类似于他和Kapranov一直在探索的高度数学。它在技术上复杂和创新。但他对追求它的热情蒸发，因为没有办法知道他可能没有犯错误。而且，正如他刚才所学到的那样，没有人可能会检查任何勤奋。这些担忧杀死了他的创造力。“我停止了奇妙的驱动研究。因为我的好奇心导致我的领域，价值和兴趣和美丽的领域，我没有探索工具。“
无论如何，没有任何确定性。根据Voevodsky的洞察核实率，每小时他花了一个人的想法，他需要花19个小时确保它是正确的。或者更多。“越野的洞察力越名，”他说，“越一个人必须在自我核实中付款。”太陡了一个价格。
沃渥德斯基认为，他能继续下去的唯一办法就是雇佣一个“证明助手”——一种可以防止他在错误的道路上走得太远的计算机程序。自2003年以来，他一直在研究计算机辅助数学正式化的前景。他说，这个错误“对我来说就像一件小礼物，让我的论点更有力。”
正如他所描述的那样，与校对助手一起工作的经历有点像玩电子游戏。他在和电脑比武。他指示它尝试这个，尝试那个——他甚至可以指示它尝试已知错误的东西，只是为了看看会发生什么。他表示:“这是非常具有互动性的。”“这可能很有趣，令人兴奋，有点上瘾。”当他犯了错误时，他输入的所有断言，一行又一行，都在他眼前消失了(尽管他将工作保存在一个名为“leftovers”的文件中)。
这样一来，一旦沃渥斯基证明了某件事，他就肯定它是真的。他不怀疑争论中是否潜藏着错误，也不担心如何说服同事。鉴证助手提供一枚证明其真实性的印章。
V.Oevodsky被认为是这个领域的先驱，但证据助手的概念已经出现一段时间了。第一部作品《自动驾驶》(Automath)可追溯到1968年。随着时间的推移，一个庞大的证明助手生态系统进化了，有无数的设置，计算机被用作一种工具，模仿传统数学是如何完成的。计算机本质上是教人类如何做数学，用公理编程，并要求它使用逻辑定律来推导证明。
另一种方法是利用计算机来探索全新的数学、新方法和新程序。例如，罗格斯大学(Rutgers)的数学家多伦·泽尔伯格(Doron Zeilberger)引用了他的合著者沙洛什·b·埃克哈德(Shalosh B. Ekhad)的话，自20世纪80年代以来，他发表了多篇论文。“对大多数人来说，”Zeilberger说，“电脑只是一个工具，就像吸尘器一样。对我来说，它就像一个同事。”他希望此举将带来革命性的效果。他说:“传统数学是基于严格的形式证明的概念，我认为这将过时。”“我认为，由于计算机是如此强大，它们开辟了新的前景，而如此严格地证明一切的旧议程不再像以前那样令人兴奋。”
在实际发现的时刻，你实际上停止思考。像艺术家一样，你连接到远远超出逻辑，思考和计算的东西。
然后是纯粹主义者，老派。普林斯顿大学的数学家约翰·霍顿·康威说:“我对计算机证明不感兴趣。”“我更喜欢思考。”他指出，具有讽刺意味的是，他的官方头衔是由IBM赞助的应用和计算数学约翰·冯·诺伊曼教授——“我整天坐着计算，但我不用电脑来做这件事。”
康威以发现数学对称的康威群、超现实数字和细胞自动机的生命游戏而闻名。他对娱乐数学很感兴趣，对四色地图定理也很感兴趣。但是在1976年，在数学家肯尼斯·阿佩尔和沃尔夫冈·哈肯的要求下，四色地图定理成为计算机证明的第一个定理，于是他就加入了纽约时报作为“一个主要的知识分子壮举” - 他对结果并不感兴趣。他也喜欢滋补封面猜测关于三维空间中的打包球的最大密度，但是当使用线性规划在1998年通过线性规划解决时，康威不满意。对于康威，计算机杀死了嗡嗡声。虽然他不是一个判断。如果他人使用计算机，他不介意。“这不是我。”
历史上，纯粹主义者并不总是如此平静地看待这个问题。计算机对四色猜想的证明引起了争议，大多数数学家拒绝接受它:计算机+数学=禁止。正如伯克利大学的爱德华·弗兰克尔教授所说纽约时报在2013年的申请死亡时，“就像一个地标最高法院案件一样，证据的遗产仍然感受到并热烈辩论。”
广义地说，反对使用计算机的论点是对人类丧失直觉和理解力的哀叹。因为计算机的判断而承认某件事是正确的，这和知道是不一样的为什么这是真的。有人可能会认为，这类似于依赖互联网上关于威尼斯神秘之处的评论，而不是去那里，在水上出租车上挥霍一番，亲自体验魔法。但是，同样的难题出现在基于以前的结果而不是从头开始。
“计算机很好，而且通常比人类更好 - 在他们设计的内容中，”弗雷肯克尔说：爱和数学．“这就是计算……但我们必须认识到，数学研究不是关于数字或计算。它是关于寻找看似不相关的事物之间的联系，它是关于看到看不见的东西。可以不是仅通过计算就可以得到。作为一名职业数学家，我可以告诉你，数学的发现对我们来说是一种洞察力。在发现的那一刻，你实际上停止思考．像艺术家一样，你连接到远远超出逻辑，思考和计算的东西。这就是数学的美丽。“
Voevodsky自己小心区分各种方式应该或不应该使用的方式。“很多人都不理解使用计算机计算的计算机生成的证明和计算机辅助证明之间的差异，”他说。“计算机生成的证据是教导我们很少的证据。并且存在正确的看法，如果我们走向计算机生成的证据，那么我们就会失去所有数学 - 数学的好处，作为精神纪律，数学是有助于形成纯洁的思想。“
更广泛的错误发生的文化和实践是一个更大的障碍，威胁着数学的基础和未来。
但是，他说，非常逐渐，在数学中使用计算机即将被认为是不可避免的。关于计算和计算，特别是在上行世代，如果被确认，它已经完全普遍存在。Frenkel同意，称，使用计算机来验证证明是预期和欢迎趋势。由于高耸的数学企业达到了新的高度，具有更复杂和深受衰老的峰值，每个从业者都钻入细节，即使在同一领域也永远无法理解，即使在同一领域也是必要的，并验证完整性结构 - 结构如此复杂，如此庞大的规模，仅仅是人类裁判的裁决将不再可行。
Voevodsky甚至更进一步，认为证明助手的作用——以及计算机的普遍使用——超越了避免错误的孤立的实际实例。因为更广泛的错误发生的文化和实践是一个更大的障碍，威胁着数学的基础和未来。错误可能是对正确证明某件事真正涉及的东西的忽视的症状。错误，他说，可以激发“直接的不诚实，声称已经证明了某件事，但实际上并没有做到。”这是当今数学的一大力量。”
“没有人故意做一些比一个人更不可能，”他估计。但如果数学家必须在不经过证明的所有细微差别的情况下选择出版，或者稍后发布并允许竞争对手取得领先，则诱惑是向细节滑行并牺牲证明和现行的质量。“And then if you read somebody else’s paper and there are even fewer details, you think, ‘Well if that’s what’s normal today then I’ll just be normal and next time put even fewer details.’ [Then] your student looks at your proofs and learns that this is how things are done, and then the student goes around and thinks completely honestly that he is doing the right thing.” It’s a gradual slippage—a “dissolution of standards.” Proof assistants nudge mathematicians in the other direction.
此外，如果有的话，错误很少，如果有启发性。即使是康威，谁喜欢在这里炫耀奇怪的错误，允许其他人见证他的瑕疵，抗议他从未遇到过任何形状或形式的错误。voevodsky解雇了追踪错误的数学转弯的概念可能就像迷失在纽约市，绊倒在一个壮丽的隐藏花园里。“嗯，首先，你必须在曼哈顿，或者你可能会发现一些不可取的东西。”
所以这些天，沃渥德斯基在他的证明助手之间来回奔波，一边严谨地一行一行地列出定义和定理，另一边是他更传统的努力，用铅笔和纸绘制图表，勾画出想法。他说:“与校对助理一起工作让我想起了什么是真正的校对。”“这让我在手写数学时能够提供更详细的证明。”每当他想走捷径的时候，比如，这个的证明和那个的证明是相似的或这很简单……或这是显而易见的……-他不得不问自己，在我值得信赖的举证助手的陪伴下，我能通过这样不靠谱的推理逃脱惩罚吗?
“显然不是。”
Siobhan Roberts是一名基于多伦多的作家。她的新书，Genius在Play：John Horton Conway的好奇心，将于今年7月由布卢姆斯伯里出版社出版。
