据科技博客网站Gizmodo报道，早在1611年，德国数学家、天文学家开普勒曾提出一个猜想。他猜测，最有效率的堆放球形物体（例如市场里的橙子）的方式是金字塔形。遗憾的是，他没能证明这个命题。不过，现在一台计算机最终证明了这个猜想的正确性，解决了已经争论了四个世纪的问题。
事实上，美国匹兹堡大学的托马斯·哈尔斯在1998年就提出过解决这个问题的证明。不过由于长达300页，12名审阅者花了4年来寻找错误。即使这样，他们也只能99%确信这个证明的正确性。所以在2003年，哈尔斯开始了他的“蝇斑计划”，即用计算机工具来检查他给出的证明的正确性。
这项计划使用了名为“Isabelle”和“HOLlight”的两款形式化验证的校验软件。二者都基于小巧而易证的一系列逻辑语句。如同数学证明一样，只要给以足够的时间，软件能够检验任何其他逻辑语句。
上周日，哈尔斯和他的团队宣布，300页的证明已经经由两款软件检验完成。让他长舒一口气的是，证明完全正确。换句话说，计算机成功证明了开普勒400年前提出的猜想的正确性。“我觉得我一下年轻了10岁，”哈尔斯对《新科学家》杂志表示。
当然，这一好消息对别的科学家也有重大的意义。数学家们每年都会给出数百个异常复杂的数学证明，而这一消息证明除了人工检查之外，计算机也能对它们进行验证。这意味着，数学家们可以尝试用更新鲜的方法解决难题了。至于复杂繁琐的验证工作，让计算机完成就好。
来源：新华国际