在最近一次从里昂前往巴黎的火车旅途中， 弗拉基米尔·沃沃德斯基 坐在 史蒂夫·奥沃迪 旁边，试图说服他改变做数学的方式。
48岁的沃沃德斯基是普林斯顿高等研究院（IAS）的常任教员。他出生于莫斯科，却能说近乎完美的英语；举止自信，仿佛无需向任何人证明自己。2002年，他获得了菲尔兹奖，这一奖项常被视为数学领域最负盛名的荣誉。
如今，火车驶近这座城市时，沃沃德斯基拿出笔记本电脑，打开了一个名为 Coq 的程序。这是一款证明助手，为数学家提供书写数学论证的环境。宾夕法尼亚州匹兹堡卡内基梅隆大学的数学家和逻辑学家奥沃迪跟着他一起看，沃沃德斯基用自己创立的一种新形式体系，为一个数学对象写下定义，名为 单值基础。沃沃德斯基花了15分钟写出这个定义。
“我当时试图说服[奥沃迪]用 Coq 做[他的数学研究]，”沃沃德斯基在去年秋天的一场讲座上解释说。“我想让他相信，这很容易做到。”
阅读本文其余内容，请访问 《Quanta Magazine》。刊载本文并不意味着世界经济论坛认同其中的观点。
如需关注议程动态， 请订阅我们的每周简报。
作者：凯文·哈特内特。凯文为《波士顿环球报》观点版撰写 Brainiac 专栏。
图片：画面中是一把电脑键盘上的“End”键。路透社/卡茨佩尔·彭佩尔。
