英文原文：Proof confirmed of 400-year-old fruit-stacking problem
“如何在有限的空间堆放最多的球型物体？”德国天文学家克卜勒（Johannes Kepler）在 1611 年提出没有任何一种堆叠方式比面心立方与六方最密堆积还要来得紧密，这两种方式就如同现今市场中常见的堆水果法，上下层交错排列，最后会堆成一座金字塔。虽然克卜勒提出解答，却无法证明它，而他的答案也就成为后来有名的克卜勒猜想（Kepler conjecture），四百年来数学家前仆后继想要解开，如今藉由一台电脑的帮忙，这道百年猜想终于被证实是真的。
（图片来源：Wikipedia）
解开此猜想的数学家为匹兹堡大学的黑尔斯（Thomas Hales），曾在 1998 年以长达三百页的论文篇幅提出证明，为了审查论证是否无误，12 名审稿者花了四年的时间检查，但最终只能肯定 99％ 是正确的，为此黑尔斯开发了一套计算工具，称为“污点计划”（Flyspeck project），希望能将最后一哩路填补起来。
污点计划使用两种形式验证软件（formal verification software），Isabelle 和 HOL Light，能够以简单、小片段的方式验证一连串的逻辑语句，因此黑尔斯就可以藉由这两套软件，将所有论文中的逻辑语句完整地检查一遍。
就在上周日，污点计划的小组宣布那份长达三百页的论文已成功通过两个软件的审查，证实他之前所提出的论证为正确的，也就是说电脑证实四百年前克卜勒提出的猜想为真。黑尔斯在接受《新科学人》（New Scientist）的采访表示：“我摆脱了肩头上沉重的负担，突然之间我好像年经十岁。”
污点计划不仅为黑尔斯带来好消息，同时也可帮数学家省下许多麻烦，有了 Isabelle 和 HOL Light 从旁协助，每年由数学家推导出来的密密麻麻数学证明，不再需要人脑逐条审查，只需要电脑就可以确认，而数学家能将更多心力放在解决其他问题上。
（首图来源：Wikimedia Commons）
相关文章
