早在1611年的时候，约翰尼斯·开普勒就建议人们在堆放球形物体时——比如商店中待售的橙子，采用金字塔型堆放法是效率最高的。不幸的是他本人并不能证明这点，不过最近计算机终于验证了这条猜想的正确性，结束了这场跨越5个世纪，长达400多年的争论。

其实，早在1998年匹兹堡大学的Thomas Hales就想出了证明方法，只是Hales的论述太长——12名评审耗时4年时间对这份300页的文档进行查错，只能99%肯定方法的正确性。所以，不甘心的Hales在2003年又开始了“污点项目”——一套能够验证他的证明法的计算机工具。

污点使用了两个形式验证软件——名字还很好听，一个叫“Isabelle”一个叫“HOL Light”——两个软件都是通过判断短小且容易验证的一系列逻辑表述来进行验证。凭借这种技术，软件可以检验所有逻辑表述的正确性，只要时间充足，验证数学证明过程也是可以的。

上周日的时候，Hales和团队宣布这份300页的证明方法已经接受并通过了两套软件的联合详细验证，最后结果显示他的验证方法完全正确，这也让Hales感到欣慰。

也就是说，计算机成功验证了400年前开普勒所提出的方法的正确性。“我一下子觉得年轻了十岁。”Hales 兴奋地说。

计算机可以成功验证数学证明过程不仅仅对于Hales来说是好消息，要知道每年全世界会诞生数百份内容多到可怕的数学证明过程，通过这项工程，Hales证明了验证逻辑不再需要人脑进行，计算机就可以完成这个工作。数学家终于能够放手去进行创造性思考——至于烦人的验证过程，交给计算机就可以了。