弗拉基米尔·沃沃斯基（1966―2017），是推动代数几何与计算机检验革命性发展的数学家，以开拓了“主上同调理论”新领域而闻名。此外，他对计算机形式化检验以及数学知识库的建设也有重大影响。
弗拉基米尔·沃沃斯基Vladimir Voevodsky
1966 ―2017
代数几何是对多项式方程几何方面的研究，如x2?+?y2?=?1，在一个范围内，x和?y是真实的数字，当x和?y是更抽象的数字时具有拓扑性质。正因为对代数几何领域的革命性推动，沃沃斯基成为了和黎曼、格罗滕迪克一样伟大的科学家。2017年9月，他逝世于普林斯顿的家中，享年51岁。
1966年，沃沃斯基出生于莫斯科，其父亲是物理学家，母亲是化学家。一开始，他学的是化学，但要想理解化学就要掌握物理知识，所以他开始学物理。可同样，要学物理就要掌握数学知识，所以他又开始学数学。于是他上了莫斯科州立大学，但由于没去上课所以没拿到学位。不过，他在校期间出版的数学论文被业界认为很有前景，所以在他本人没有申请的情况下，哈佛大学向他发出了入学邀请。1992年，沃沃斯基拿到了该学校的博士学位。
之后10年，沃沃斯基在学术上有很大建树。他的研究来源于格罗滕迪克在60年代提出的“主对象”的理论研究。在沃沃斯基的主上同调理论中，经典常用的几何被主上同调理论代替，同调理论是拓扑学的一个分支，大致说的是两个对象间的连续变化，比如从一根线逐渐缩小直至一个点。格罗滕迪克认为几何物体之间的映射可以被局部地定义，但沃沃斯基否定了这个观点。
1996年，沃沃斯基拿到博士学位还不到4年，他就宣布自己证明了1970年的“约翰·米尔诺猜想”，成为了能证明该猜想的第一人。沃沃斯基也因此获得了数学领域的最高奖项――菲尔兹奖。除此以外，他还证明了其他3个非常重要的猜想。
2002年，他被普林斯顿高等研究院数学系聘为教授。他开始思考数学检验的计算机表示法。和之前很多数学家一样，沃沃斯基梦想能有一个数学陈述和证明的全球数据库，这样数学家就能取得更多的成就，并且还能分享他们的成果。
2006年，沃沃斯基选择“类型理论”作为该全球数据库的正式语言，因为它能将数学对象分成“类型”，如三角形或曲线。他认为，比起数学家常用的集合理论，类型理论更自然一些。他设想的概念是该理论可以把类型组成一个无限的等级，等级1为命题，等级2为一系列基本事物（如自然数字），等级3为结构分类（如三角形），以此类推。数学家用不同的方法研究一个潜在相同的概念时，通过一价机制就可以互相运用成果。
2010年，他在3周之内制造了一个代码图书馆，里面有成千上万的基本定义和理论，他称之为“一价基础库”。该基础库之后被收入进了一个更大的UniMath数据库。UniMath的目的是将数学这个庞大的知识系统正式化。沃沃斯基一生留下了8篇从不同角度证明这个新系统合理的论文。一价基础库提供了一个全球数学资料库的概念，首次将类型理论作为数学库的基础。
尽管沃沃斯基10年前就把研究重点转移到了其他方向，但是主上同调理论仍在不断发展。还有很多研究人员继续寻找新的方法，将他的基础库运用到代数、几何和拓扑学当中。一价基础库注定成为一个研究的热门。将沃沃斯基的主对象研究收入到基础库也是帮助他圆梦的一个好途径。
沃沃斯基是一位有远见、细心的数学家，他有一股永不屈服的精神，但和人相处时他又非常亲切、友好和真诚。尽管他一生大部分时间被抑郁困扰，但他依然取得了很多了不起的成就。
资料来源Nature
责任编辑田心