一些关于弗拉基米尔·沃沃斯基（Vladimir Voevodsky）的信息
《一个定理的诞生》一书，关于沃沃斯基的部分沃沃斯基没有努力给我讲解自己的工作，而是跟我谈了谈他的梦想。那是一个一直以来让他无比痴迷、不惜全力以赴的研究课题 —-专家系统（langages experts）和自动定理证明。沃沃斯基认为，在不远的将来，计算机软件能够检查卷轶浩繁的数学证明的正确性。他说，其实在法国，人们已经开始利用软件对一些著名的数学结论进行检验了。一开始，我对他的话将信将疑。然而，我面前站着的毕竟不是一个失心疯患者，而是一位顶尖科学家，我应该将他的话当作一个严肃的论断接受下来。我从来没有接触过这类问题，而且基本上没有使用过算法。匹配算法（二分图匹配算法）、单纯形法和拍卖算法在最优输运问题的数值模拟中都扮演着重要角色，而我恰恰是最优输运领域的专家。但是，沃沃斯基跟我谈及的问题却属于一个迥然不同的思维范畴。这里面有如此之多的谜题等待研究，不禁让人兴趣盎然。花朵、语言、四色、融合 ……奇妙的元素构成一首美妙的歌曲。是否已有人谱写过这支歌？现在，不知疲倦的贡捷有了更加雄心勃勃的计划：验证有限单群分类定理，这些定理的证明皆属于 20 世纪最长的证明。 ...
