计算机正在改变数学证明的验证

Vladimir Voevodsky于 1966年6月4日出生在莫斯科，为了理解物理学他对数学产生了兴趣，随后他又一发不可收拾的爱上了抽象代数。虽然他没有读完数学的本科学业，但在 1989年共产党倒台后这一切变得无关紧要，他用论文证明了自己。他和Misha Kapranov发展了高维数学对象和类，在1990年发表了一个重要结果。他甚至没有申请就被哈佛接受读博，1992年的博士论文标志着代数几何的一个新思想领域的开始。2002年他获得菲尔茨奖，2001年成为普林斯顿高等研究院的正教授。但在1998年，美国数学家 Carlos Simpson发表论文认为他1990年发表的那篇论文存在一个错误。Voevodsky对此展开了仔细的分析，多年来都没有取得进展。他仍然认为自己的结果是正确的。在2013年，他取得了突破确认了自己的错误，而且是主要理论错误，重要的结果不再重要。原因是他们没有去检查简单情况，只证明了困难情况。他发表了60篇论文，只发现了两个错误，其中一个可以被修正，这个错误比例不算高。然而此事却令他万分沮丧。他注意到读者懒于去核查信任的作者的论文，而论文的复杂性使他们几乎不去检查细节。他正在发展一个新理论，但热情很快消失的无影无踪，因为没有办法知道他是否犯下了另一个错误。验证一个观点是否正确比提出一个观点所花的时间要多得多。唯一的解决方法只能是使用计算机程序去帮助检查，计算机正在改变数学的证明。