《一个定理的诞生》一书，关于沃沃斯基的部分

沃沃斯基没有努力给我讲解自己的工作，而是跟我谈了谈他的梦想。那是一个一直以来让他无比痴迷、不惜全力以赴的研究课题 —-专家系统（langages experts）和自动定理证明。

沃沃斯基认为，在不远的将来，计算机软件能够检查卷轶浩繁的数学证明的正确性。他说，其实在法国，人们已经开始利用软件对一些著名的数学结论进行检验了。一开始，我对他的话将信将疑。然而，我面前站着的毕竟不是一个失心疯患者，而是一位顶尖科学家，我应该将他的话当作一个严肃的论断接受下来。我从来没有接触过这类问题，而且基本上没有使用过算法。匹配算法（二分图匹配算法）、单纯形法和拍卖算法在最优输运问题的数值模拟中都扮演着重要角色，而我恰恰是最优输运领域的专家。但是，沃沃斯基跟我谈及的问题却属于一个迥然不同的思维范畴。这里面有如此之多的谜题等待研究，不禁让人兴趣盎然。花朵、语言、四色、融合 ……奇妙的元素构成一首美妙的歌曲。是否已有人谱写过这支歌？

现在，不知疲倦的贡捷有了更加雄心勃勃的计划：验证有限单群分类定理，这些定理的证明皆属于 20 世纪最长的证明。

NYT 这篇报道内容比较丰富：Vladimir Voevodsky, Revolutionary Mathematician, Dies at 51（中文来自于 Google 翻译）

He was “one of the giants of our time,” Thomas Hales, a mathematician at the University of Pittsburgh, said in an interview. Dr. Voevodsky, he said, transformed every field he touched. In his work using computers, for example, he upended mathematical thinking to such a degree that he changed the meaning of the equals sign.

他是"我们这个时代的巨人之一"，匹兹堡大学的数学家托马斯·黑尔斯在接受采访时说。他说，Voevodsky博士改变了他所触及的每一 个领域。例如，在他使用计算机的工作中，他颠覆了数学思维，以至于他改变了等号的含义。

“If you want to ask how profound his work is, that’s how profound it is,” Dr. Hales said. “It changes the very meaning of what the equals sign means in mathematics.”

He added: “His ideas gave a new way for all mathematicians to do what they do, a new foundation. The foundations of math are like a constitutional document that spells out the governing rules all mathematicians agree to play by. He has given us a new constitution.”

“如果你想问他的工作有多么深刻，那就是它的深刻程度，“Hales博士说。“它改变了等号在数学中的意义。”

他补充说：“他的想法为所有数学家提供了一种新的方式来做他们所做的事情，一个新的基础。数学的基础就像一个宪法文件，阐明了所有数学家同意遵守的管理规则。他给了我们一部新宪法。”

Dr. Voevodsky realized that human brains could not keep up with the ever-increasing complexity of mathematics. Computers were the only solution. So he embarked on an enormous project to create proof-checking software so powerful and convenient that mathematicians could someday use it as part of their ordinary work and create a library of rock-solid mathematical knowledge that anyone in the world could access.

他意识到，数学论证变得如此复杂，其他数学家很少详细检查它们。而他的出色声誉只会让问题变得更糟：每个人都认为他的证明必须是正确的。

Voevodsky博士意识到人类的大脑无法跟上数学不断增加的复杂性。计算机是唯一的解决方案。于是，他开始了一个巨大的项目，以创建证明检查软件如此强大和方便的数学家可能有一天会用它作为自己平凡的工作的一部分，并创建一个图书馆的坚如磐石的数学知识，任何人在世界上可以访问。

Computer scientists had worked on the problem for decades, but it was territory only a few mathematicians had ever ventured into. “Among mathematicians, computer proof verification was almost a forbidden subject,” Dr. Voevodsky wrote.

几十年来，计算机科学家一直致力于解决这个问题，但只有少数几位数学家才进入这个领域。“在数学家中，计算机证明验证几乎是一个被禁止的主题，“Voevodsky博士写道。

The problem was that these systems were extraordinarily cumbersome. Checking a single theorem could require a decade of work, because the computer essentially had to be taught all of the mathematics a proof was built on, in agonizing, inhuman detail. Ordinary mathematicians intent on expanding the borders of the field could not possibly devote that kind of effort to checking their proofs.

问题是这些系统非常麻烦。检查一个单一的定理可能需要十年的工作，因为计算机基本上必须被教授所有的数学证据，这些数据建立在令人痛苦的，不人道的细节之上。旨在扩大该领域边界的普通数学家不可能将这种努力用于检查他们的证据。

Somehow, computers and humans needed to be taught to think alike.

不知何故，需要教导计算机和人类进行相同的思考。

Dr. Voevodsky developed a stunningly bold plan for how to do so: He reformulated mathematics from its very foundation, giving it a new “constitution,” as Dr. Hales put it. Mathematics so reformulated would be far friendlier to computers and allow mathematicians to talk to computers in a language that was much closer to how mathematicians ordinarily think.

Voevodsky博士为如何这样做制定了一个非常大胆的计划：他从其基础开始重新配置数学，给它一个新的"宪法”，正如Hales博士所说的那样。如此改编的数学对于计算机来说会更加友好，并允许数学家用一种更接近数学家通常思考的语言与计算机交谈。

Today, Dr. Voevodsky declared in 2014, “computer verification of proofs, and of mathematical reasoning in general, looks completely practical.”

今天，Voevodsky博士在2014年宣称，“证据的计算机验证和一般的数学推理看起来非常实用。”

Further, Dr. Voevodsky integrated the computer into the process of doing his own research, describing it as a bit like a video game. “You tell the computer, ‘Try this,’ and it tries it, and it gives you back the result of its actions,” he said in an interview with Scientific American in 2013. “Sometimes it’s unexpected what comes out of it. It’s fun.”

此外，Voevodsky博士将计算机整合到自己研究的过程中，将其描述为有点像视频游戏。“你告诉电脑，‘尝试这个’，它会尝试它，它会让你回到它的行动结果，“他在2013年接受科学美国人的采访时说道。“有时出乎意料的是它是出乎意料的。好有趣。”

Dr. Voevodsky was at the center of an informal but enormous effort to fulfill his vision, having inspired dozens of researchers to join it. “He’s been our leader, even though he lets everybody do whatever they want,” said Robert Harper of Carnegie Mellon University in Pittsburgh. “He’s this inspirational and spiritual leader by example.”

Voevodsky博士是实现其愿景的非正式但巨大的努力的中心，激励了数十名研究人员加入其中。匹兹堡卡内基梅隆大学的罗伯特哈珀说：“他一直是我们的领导者，尽管他让每个人都做他们想做的事情。” “他就是这个鼓舞人心和精神领袖的榜样。”

Dr. Voevodsky was especially attentive to young mathematicians. “By being accommodating, encouraging, listening to people, he generated enormous interest,” Dr. Harper said in a telephone interview.

Voevodsky博士特别关注年轻的数学家。哈珀博士在接受电话采访时说：“通过接纳，鼓励，倾听人们，他产生了巨大的兴趣。”

更多参考信息链接：

记录于 2018 盛夏，发布于 2018 金秋