转载

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

　　Vladimir Voevodsky 于 1966 年 6 月 4 日出生在莫斯科，为了理解物理学他对数学产生了兴趣，随后他又一发不可收拾的爱上了抽象代数。虽然他没有读完数学的本科学业，但在 1989 年共产党倒台后这一切变得无关紧要，他用论文证明了自己。

　　他和 Misha Kapranov 发展了高维数学对象和类，在 1990 年发表了一个重要结果。他甚至没有申请就被哈佛接受读博，1992 年的博士论文标志着代数几何的一个新思想领域的开始。2002 年他获得菲尔茨奖，2001 年成为普林斯顿高等研究院的正教授。

　　但在 1998 年，美国数学家 Carlos Simpson 发表论文认为他 1990 年发表的那篇论文存在一个错误。Voevodsky 对此展开了仔细的分析，多年来都没有取得进展。他仍然认为自己的结果是正确的。在 2013 年，他取得了突破确认了自己的错误，而且是主要理论错误，重要的结果不再重要。原因是他们没有去检查简单情况，只证明了困难情况。他发表了 60 篇论文，只发现了两个错误，其中一个可以被修正，这个错误比例不算高。然而此事却令他万分沮丧。他注意到读者懒于去核查信任的作者的论文，而论文的复杂性使他们几乎不去检查细节。

　　他正在发展一个新理论，但热情很快消失的无影无踪，因为没有办法知道他是否犯下了另一个错误。验证一个观点是否正确比提出一个观点所花的时间要多得多。唯一的解决方法只能是使用计算机程序去帮助检查，计算机正在改变数学的证明。

正文到此结束