许多新的证明极其复杂,以至于数学家们很担心一些潜在的错误难以被发现。以有限单群分类定理(classification of finite simple groups)为例,单群在有限群论中的地位,与素数在数论中的地位、原子在化学中的地位一样,它们都是构建各自所在世界的“砖块”。对于任意的有限群,我们可以将其分解为一系列单群,且分解方法是唯一的。通过研究这些“砖块”,我们可以进一步发现由它们所组成的物质的结构和性质。与当年化学家寻找新元素一样,数学家也开始了对于单群的寻找—列出一个单群的“元素周期表”,并证明这个“周期表”中包含了所有的单群。其中,“魔群”是最大的“散在单群”。“魔群定理”的证明散落在100多篇论文中,合计超过10000页,涉及数百名数学家。单群的“元素周期表”中含有26个散在单群,对于是否存在第27个散在单群,人们总是持怀疑态度。对于这种类型的复杂证明,进行人力审核几乎是不可能的,那么,是否可以通过计算机程序来检验数学定理的证明呢?
20世纪80年代末,法国数学家皮埃尔·于埃(Pierre Huet)和蒂埃里·科昆德(Thierry Coquand)开始从事结构微积分(calculus of constructions)项目。该项目简称CoC,但很快又被称为Coq(法语里意为“公鸡”)。这个改动一方面是为方便记忆,因为在法国一直有以动物命名开发工具的习惯;另一方面是因为Coq是其开发者之一科昆德姓氏的前三个字母。Coq为验证数学证明而生,很快也成了验证计算机证明的重要程序,备受青睐。
贡蒂尔团队验证完四色定理后,紧接着开始了对奇阶定理(odd order theorem)的验证工作。奇阶定理是对称性研究最重要的指导定理之一,通常被认为是有限单群分类的基石。像化学里的元素周期表一样,有限单群是构成数学有限群论“元素周期表”中的基本元素,所有的对象都由有限单群构成。具有素数边的正多边形(如正三角形、正五边形)是该周期表中的元素。此外,该周期表中还有一些复杂且独特的对称元素,如旋转了60次的正二十面体、需要196883维线性空间才能表达的“魔群”等。“魔群”具有的元素个数超过了构成地球的原子个数。
以色列数学家多伦·泽尔伯格(Doron Zeilberger)认为:数学家只用铅笔和纸张工作的日子即将结束。20世纪80年代以来,他一直使用计算机撰写论文。他将自己的由AT&T(美国电话电报公司)生产的计算机命名为“Shalosh B. Ekhad”(希伯来语中3B1的意思),并坚持将这位机器伙伴作为论文的联合作者。泽尔伯格认为,人们之所以不愿倚重人机合作的方式,是因为“狭隘的人本主义”在作祟,这种偏执与其他形式的偏执一样,阻碍了人类发展的脚步。
马库斯·杜·桑托伊(Marcus du Sautoy),英国皇家学会院士,美国数学学会院士,牛津大学西蒙尼公众理解科学教授,大英帝国勋章获得者,英国皇家学会迈克尔·法拉第奖获得者,伦敦数学协会贝维克奖获得者。桑托伊被誉为科学王国的大使,他创造了“流行数学”的概念,将复杂的数字和数学概念用形象生动、通俗易懂的语言表达出来。他常为《泰晤士报》和《卫报》写文章,也为电台和电视台作评论,同时与英国BBC广播公司保持长期合作。2001年,他赢得了伦敦数学会的贝维克奖(Berwick Prize)。2004年,他被英国《周日独立报》评为英国最杰出的科学家之一。