1. 计算机1.1. 对于计算机来说，它就很擅长处理这种重复而机械且计算量庞大的任务1.1.1. 在速度与准确性等方面，计算机是远超过手工计算的1.2. 计算机只能执行指令，并无自主创造力1.2.1. 想要证实程序中是否存在错误是很困难的1.2.2. 我们能在多大程度上相信计算机，这个问题一直困扰着人工智能领域的学者1.2.3. 当我们进入由算法主导的未来时，确保代码中没有未被检测出的错误，将成为一项艰巨的挑战1.3. 哲学家大卫·休谟（David Hume）指出的，大多数科学研究都建立在归纳法之上——通过观察特定的例子来推断出一个普遍的规律或原则1.3.1. 基于归纳法，曾产生了许多著名的科学理论，这反过来证实了归纳法确实是一种科学研究的好方法1.4. 人类大脑的物理局限性，审核人必须得充分相信计算机的能力，就好比我们第一次乘坐飞机一样，心中难免惴惴不安1.4.1. 许多问题的证明往往都存在不足或错误，人类犯错的可能性通常比计算机更大1.4.2. 错误可以被修正，但遗憾的是，在证明的验证和审核阶段它们并没有被找出来1.4.2.1. 证明的验证和审核非常重要，它是发现缺陷和漏洞的重要环节1.4.3. 以安德鲁·怀尔斯证明“费马大定理”为例，在其证明方法付梓之前，审验人员发现了一个小缺陷1.4.3.1. 怀尔斯和理查德·泰勒（Richard Taylor，曾是怀尔斯的学生）奇迹般地修正了这一缺陷1.5. 许多新的证明极其复杂，以至于数学家们很担心一些潜在的错误难以被发现1.5.1. “魔群”是最大的“散在单群”1.5.1.1. 需要196 883维线性空间才能表达的“魔群”1.5.1.2. “魔群”具有的元素个数超过了构成地球的原子个数1.5.2. “魔群定理”的证明散落在100多篇论文中，合计超过10 000页，涉及数百名数学家1.5.3. 真理的产生取决于你的证明方法1.6. 20世纪70年代，计算机对“四色定理”的证明轰动了全世界1.6.1. 四色定理指的是“任何一张地图只用四种颜色就能使具有共同边界的国家着上不同的颜色。”1.6.1.1. 在不引起混淆的情况下，一张地图至少需要四种颜色来标记1.6.2. 1976年，数学家凯尼斯·阿佩尔（Kenneth Appel）和沃尔夫冈·哈肯（Wolfgang Haken）在前人的基础上用计算机证明了四色定理1.6.2.1. 阿佩尔与哈肯把地图的无限种可能情况简化为1936种构型，但是要靠人工逐一验证如此之多的构型是不现实的，所以才需要借助计算机进行验证1.6.2.2. 整个证明过程的耗时超过了1000小时1.7. 1992年，牛津物理学家利用弦理论中的启发法对高维几何空间中可识别的代数结构数量进行了预测1.7.1. 事实证明，否定这个预测的错误证据正是由一个有缺陷的计算机程序生成的1.7.2. 错的是数学家，而不是物理学家1.7.2.1. 程序的错误把他们引入了歧途1.8. 2006年匹兹堡大学的托马斯·黑尔斯（Thomas Hales）教授在《数学年鉴》上发表了关于借助计算机证明著名的数学问题——“开普勒猜想”的论文1.8.1. 开普勒猜想就是对在空间中如何最密集地堆积圆球的解答1.8.2. 用了8年时间，数学家们证明了黑尔斯是正确的，但其确定性是99%1.8.2.1. 对于数学纯化论者来说，这1%也是不可容忍的1.8.2.2. 因为无法确定计算机程序是否存在潜在缺陷2. Coq证明助手2.1. 数学是最伟大的浪漫主义学科之一，即便是天才，也得掌握所有知识才能激发灵感，理解一切。2.1.1. 贡蒂尔2.2. 在过去，数学问题的证明和验证过程全凭人工完成2.2.1. 人类的大脑存在物理上的局限性2.3. 越来越多的证明开始借力于计算机，但因为验证的过程既烦冗又复杂，并且工作量巨大，人类大脑的局限性决定了无法采用人工验证的方式判断其对错2.3.1. 通过构建新的程序来验证计算机证明的正确性2.3.2. 所做的一切能够叩开人类与机器彼此信任、持续合作的新时代“大门”2.4. 人类手工证明与计算机证明不同，手工证明过程中会跳过一些烦琐或众人皆知的步骤，而计算机却依赖于明确、细化的步骤才能正确执行指令2.4.1. 类似于写小说和写保姆指导手册的区别2.4.2. 前者不需要对主人公的每一个动作都解释得一清二楚2.4.3. 后者则需要尽可能地明确和详尽，包括一天中婴儿的食谱，以及吃饭、睡觉、上厕所的每一个细节2.5. 20世纪80年代末，法国数学家皮埃尔·于埃（Pierre Huet）和蒂埃里·科昆德（Thierry Coquand）开始从事结构微积分（calculus of
constructions）项目
2.5.1. 该项目简称CoC，但很快又被称为Coq（法语里意为“公鸡”）2.5.2. 在法国一直有以动物命名开发工具的习惯2.5.3. Coq是其开发者之一科昆德姓氏的前三个字母2.5.4. Coq为验证数学证明而生，很快也成了验证计算机证明的重要程序2.6. 2000年，微软研究院首席研究员乔治·贡蒂尔（Georges Gonthier）及其同事使用Coq对阿佩尔与哈肯的四色定理的计算机证明进行了验证，因为这是史上第一个需要计算机才能完成的证明（假定Coq不存在任何缺陷）2.6.1. 计算机用了5年的时间进一步自动识别并验证人类证明的过程2.6.2. 这期间，人们惊讶地发现了在第一次证明中被忽略的数学知识2.7. 越来越多的计算机证明被Coq所验证，使我们更加确信Coq是可靠的2.7.1. 用一个计算机程序来验证多个计算机证明，比编制一个特定的证明程序或者进行人工证明更值得我们信任2.8. 为了充分理解数学理论的构建过程并使之与Coq充分融合3. 奇阶定理3.1. odd order theorem3.2. 奇阶定理是对称性研究最重要的指导定理之一，通常被认为是有限单群分类的基石3.3. 有限单群是构成数学有限群论“元素周期表”中的基本元素，所有的对象都由有限单群构成3.4. 具有素数边的正多边形（如正三角形、正五边形）是该周期表中的元素3.5. 该定理指出，任何奇阶对称结构的基本组成单元都是素数多边形，此外再无其他结构3.6. 如果把对称物体分为奇阶和偶阶两种，那么该定理就等于涵盖了其中的一半，意义重大3.7. 奇阶定理的原始论文有255页，占据了《太平洋数学期刊》的全部篇幅3.7.1. 在它出版之前，大多数证明最多只有几页，一天内即可掌握3.7.2. 这个冗长复杂的证明，对每一位数学家来说都是一个挑战3.7.3. 其中是否存在细微的缺陷或错误，始终无法考证
