电脑能取代人类做数学？ _小知识

如你所知，电脑是数学家们的得力助手。不仅如此，电脑在帮助他们的同时也能够自己发现并证明一些数学定理。
【电脑能取代人类做数学？】四色定理的证明或许由电脑做出的第一个重要结果，这个定理声称任何一张地图（有着确定的、合理的条件）只要用四种不同颜色就够了。
这个定理在1976年首先被电脑证明，尽管不久后就被发现有漏洞。而一个完全正确的证明直到1995年才被最终完成。
起点
在2003年，匹兹堡大学的托马斯·海尔斯发表了一篇关于开普勒猜想的基于计算机的证明，这个猜想研究摆放相同维数球体的最节省空间的方法。
尽管海尔斯在2003年发表了这一证明，许多数学家对此却并不满意。作为回应，在2014年海尔斯发表了一个已被计算机验证过的正式证明。
发展
沿着这条线的最新进展是最近《自然》上的一篇关于所谓的“布尔毕达哥拉斯三元数问题”计算机证明的声明。
这个断言是说，从1到7824的任何整数能够被染成红色或蓝色，使得满足a2+b2=c2（由毕达哥拉斯定理，a，b，c正好是直角三角形的三条边）的三个整数a,b,c不全是同一种颜色；而对于从1到7825的整数，不存在满足条件的染色。
研究表明，给1到7825的整数进行染色，其所有可能的方法总数是一个天文数字——超过10的2300次方（1后面跟着2300个0）。这个数字比可观测到的宇宙中的基本粒子数10的85次方还要来得巨大的多！
在计算机输出中，德克萨斯的计算机在数学计算方面却是超人一筹——令人难以置信的200兆兆字节，换句话说2字节或者平均到地球上每个人30000字节。
谁能检查这种尺度的输出结果？幸运的是，这个布尔毕达哥拉斯三元数问题的解法能够被一个小得多的程序检查。
这跟用计算机分解一个很大的数c为两个较小因子a和b，使得c=a×b很相似。通常寻找这两个因子a和b是极其困难的，但是一旦找到，把它们乘起来以确认结果就是很容易的事了。
数学家过时了吗？
这些发展和进步意味着什么？是否数学研究者们很快就要沦落为
被快速发展的科技所威胁而面临淘汰的职业之列？
不完全是。数学家，就像许多其他领域的专业人士，已经很大程度上接受计算机作为一种新的数学研究工具，由此发展来的所谓的实验数学，已经产生了深远影响。
问
实验数学究竟是什么呢？
它被很好地定义为使用计算机作为“实验室”的一种研究方式。跟物理学家、化学家、生物学家或者工程师做实验一样，举个例子，它可以用来获得洞察力和直觉，检验和否证猜想，以及确认一些已经被传统方法证明了的结果。
数学家将来的命运如何？
各种迹象都表明在可预见的未来，数学研究者们将会和计算机互利共存，继续他们的工作。确实，随着这种共存关系和计算机技术的成熟，数学家们将会更愿意把证明的某些部分扔给计算机去做。