已有90年的历史数学难题——凯勒猜想
“凯勒猜想”（Keller’s conjecture）是关于特定形状如何平铺覆盖空间的问题，于1930年由Ott-Heinrich Keller提出。该推测认为，如果一个N维空间被N维相同的超立方体所覆盖，则至少两个超立方体必须共享一个面。例如，如果尝试用匹配的方砖完全覆盖一个立方体，则应始终至少存在一对完全面贴面的砖。该猜想对每个维度的空间做出相同的预测。
数学家探索该猜想已有90年了。一维到六维已被证明是正确的，八维及以上维度证明是错误的。最后一个谜是，第七维空间是否正确。
在2019年秋季，热衷于用constraint satisfaction technique（约束满足技术）解决组合问题、专门研究计算和信息科学的RIT博士研究生David Narváez受邀加入了一个包括来自斯坦福大学和卡内基梅隆大学的研究人员组成的小组，协助证明这个持续将近一个世纪的猜想。
该小组最近发表了一篇关于其工作的论文，宣布证明了这个猜想在第七维空间中是正确的。
要证明这个猜想，得利用高性能计算机系统地检查所有可能性，但是有难点，也是该猜想迟迟未能被证明的原因。“这类数学对象的问题在于它们的结构高度复杂，又具有许多相似之处，”Narváez说，“如果可以意识到计算中的对称性，可以避免很多无用计算。但是计算机逻辑并不知道这一点，因此它会重复很多工作。”
卡内基梅隆大学副教授Heule说：“不打破对称性，自动化方法就无法解决这个猜想。实施对称性打破非常困难，我们必须确保没有犯任何错误。”
最终，Narváez利用他在对称性破坏方面的专业知识来帮助一个计算机集群在30分钟内解决了问题。他引入了使证明可验证的技术，让数学计算机程序可以确认答案是正确的。
David Narváez，来自巴拿马，RIT计算机与信息科学博士研究生
Narváez打破对称性论点的一个重要部分是，他的技术还把它变成了机器可检查的证明（计算机产生的答案通常太复杂，以至于人类无法理解，因此需要通过数学计算机程序进行验证），让研究人员对实现的正确性充满信心；该技术最终产生了大约200 GB的巨大证据。
Heule总结到：“解决凯勒的猜想表明，自动推理能够解决数十年来一直面临的数学难题。拥有能够解决人类难以解决的问题的技术非常重要。相同的技术用于显示高度复杂的系统的正确性，这样的系统无处不在，从金融到医疗保健再到航空。”
“我喜欢使用计算机科学来帮助解决数学家所遇到的问题。” 对于自己的成就，Narváez如是说。也许兴趣加上环境，就是成就伟大科学家的最主要条件。
*本文翻译编辑自罗切斯特媒体《Democrat and Chronicle》的报道。
同学们如果在申请入读RIT的过程中遇到问题，可以随时私信小编编写“姓名+意向专业+微信ID”加入RIT微信咨询群，和RIT的招生官，还有学长学姐们一起交流。
