撰文 Borwein（纽卡斯尔大学数学教授）、Bailey（加州大学戴维斯分校研究员）

　　翻译 333 （哆嗒数学网翻译组成员，就读于中南大学数学专业）

　　电脑在帮助数学家解决问题时是很有用的工具，同时，它们也能够自己发现并证明一些数学定理。

　　或许由电脑做出的第一个重要结果要算是40多年前关于四色定理的证明，这个定理声称任何一张地图（有着确定的、合理的条件）只要用四种不同颜色就够了。

　　这张图中需要四种不同的颜色以确保任意两个相邻的区块颜色是不同的。

　　这个定理在1976年首先被电脑证明，尽管不久后就被发现有漏洞。而一个完全正确的证明直到1995年才被最终完成。

　　在2003年，匹兹堡大学的托马斯·海尔斯发表了一篇关于开普勒猜想的基于计算机的证明，这个猜想是说，与超市堆放橘子的方法类似，这也是摆放相同维数球体的最节省空间的方法。

　　尽管海尔斯在2003年发表了这一证明，许多数学家对此却并不满意。因为这个证明是伴随着2G字节的计算机输出(需要耗费大量的时间)，并且某些计算无法保证完全正确。

　　作为回应，在2014年海尔斯发表了一个已被计算机验证过的正式证明。

　　新手上路

　　沿着这条线的最新进展是最近《自然》上的一篇关于所谓的“布尔毕达哥拉斯三元数问题”计算机证明的声明。

　　这个断言是说，从1到7824的任何整数能够被染成红色或蓝色，使得满足 a2 + b2 = c2 （由毕达哥拉斯定理，a，b，c 正好是直角三角形的三条边）的三个整数 a，b，c 不全是同一种颜色；而对于从1到7825的整数，不存在满足条件的染色。

　　即使是对于比较小的整数也很难找到一个满足上述条件的染色方法。举个例子，如果5是红色的，那么12和13中至少得有一个是蓝色，因为；3和4中也必须至少有一个是蓝色，因为。每一种选择都将导致对于其他数产生不同的约束条件。

　　研究表明，给1到7825的整数进行染色，开奖，其所有可能的方法总数是一个天文数字——超过10的2300次方（1后面跟着2300个0）。这个数字比可观测到的宇宙中的基本粒子数10的85次方还要来得巨大的多！

　　不过通过利用各种各样的对称性和数论性质，研究人员能够把这个数字显著地减小到“仅仅”一万亿。德克萨斯州立大学有着800个处理器的超级计算机 Stampede 为了检查这一万亿种情形足足运行了两天。

　　尽管这一结果无法被直接应用，但是解决这样一个困难染色问题的能力势必会对密码学和安全领域产生一定影响。

　　在德州的这次计算，据估计执行了大约10的19次方次算术操作，却仍然不能称得上是最大型的计算。2013年对 π?2; 数字的计算，两名IBM的研究人员做了两倍于此的计算量。

　　梅森素数互联网大搜索（GIMPS），是一个寻找最大已知素数的全球性计算机互联网络，每秒可执行450万亿次计算，每六个小时就超过德州那次计算的数目。

　　在计算机输出中，德克萨斯的计算机在数学计算方面却是超人一筹——令人难以置信的200兆兆字节，换句话说2字节或者平均到地球上每个人30000字节。

　　谁能检查这种尺度的输出结果？幸运的是，这个布尔毕达哥拉斯三元数问题的解法能够被一个小得多的程序检查。

　　这跟用计算机分解一个很大的数c为两个较小因子 a 和 b，使得 c=a×b 很相似。通常寻找这两个因子 a 和 b 是极其困难的，但是一旦找到，把它们乘起来以确认结果就是很容易的事了。

　　数学家过时了吗？