计算机科学家马伦・豪勒(Marijn Heule)始终在数学领域内寻求挑战。豪勒是卡内基梅隆大学的一名副教授，他因善于使用计算工具解决数学难题而声名卓著。

2016 年他对 “布尔毕氏三元组问题” 的解答，因其巨大的证明量而成为了头条新闻：“200TB 的数学证明前所未有。” 如今，他正在运用自动化的方式向及其简明的考拉兹猜想发起攻坚战。

(来源：MS TECH | SUPERREMBO VIA CODINGTRAIN)

根据某些说法，考拉兹猜想于二十世纪 30 年代由德国数学家罗特哈尔・考拉兹(Lothar Collatz)首次提出，这一数论问题提出了一个生成数列的方法，或者叫算法：数列的首项是任一正整数；如果该数为偶数，则将其除以 2；如果该数为奇数，则将其乘以 3 再加 1；然后不断重复这一规则。该猜想称，这一数列最终一定会得到 1(之后继续以 4，2，1 的顺序循环)。

例如，以 5 作为数列首项，会产生 6 个数：5, 16, 8, 4, 2, 1。

以 27 为首项会生成一个 111 项的数列，在到达 1 之前上下波动，最大值达到 9232。

把首项增大到 40，得到的数列就又短了回去：40, 20, 10, 5, 16, 8, 4, 2, 1。如今，从 1 到接近 300000000000000000000 为止的正整数都已被计算机验证符合考拉兹猜想。

大多数研究者都相信考拉兹猜想是正确的。它吸引了许多数学圈子内外的人士为之前赴后继，但尚未有人能为它提供证明。二十世纪 80 年代初，匈牙利数学家保罗・厄德斯(Paul Erdős)曾称：“数学还没准备好解决这样的问题。”

“他可能是正确的，” 豪勒说。对于豪勒而言，考拉兹猜想的诱惑力与其说是实现突破的可能性，不如说是它能促进自动推理技术的进步。

最近，与考拉兹猜想缠斗了 5 年之久的豪勒和他的合作伙伴 —— 斯科特・阿隆森(Scott Aaronson)和埃姆雷・约尔库(Emre Yolcu)—— 在预印本平台 arXiv 上发布了一篇论文。他们在论文中写道：“尽管我们没能成功证明考拉兹猜想，但我们认为，本文的观点提供了一种十分有趣的新方法。”

“这是次宝贵的失败，” 阿隆森如此评价到。他是一名计算机科学家，任职于德克萨斯大学奥斯汀分校。说它失败，是因为他们没能成功证明考拉兹猜想。说它宝贵，是因为他们在另一种意义上实现了进步：豪勒认为，从此开始，我们将能够确认究竟是人类还是计算机更善于证明此类问题。

对于许多数学问题而言，计算机是指望不上的，因为后者接触不到历史上积累的大量数学作品。但电脑也有行的时候。把问题答案可能长什么样告诉电脑 —— 给它定个目标并规定好搜索域 —— 电脑可能就会靠强力找到答案，尽管电脑计算的结果能否算得上对数学经典的有意义的补充尚且存在争议。

传统观点认为，只有人类通过概念和观念发挥的创造力和直觉才能扩展数学的范围，相比之下，通过计算实现的进步往往被鄙称为工程学。

在某种程度上，计算机和考拉兹猜想可谓天作之合。一方面，正如卡内基梅隆大学的逻辑学家和哲学教授杰瑞米・阿维加德(Jeremy Avigad)所言，迭代算法的概念是计算机科学的基础，而通过特定规则一步步演算出来的考拉兹数列正是迭代算法的绝佳示例。

同时，进程终止的表达也是计算机科学中的一个常见问题。阿维加德说：“计算机科学家都想知道他们的算法于何处终止，所谓终止就是说它会重复得到同一个答案。” 豪勒和他的同僚在处理考拉兹猜想(其实就是个终止问题)时就运用了这一技术。

豪勒的专长是使用一种叫做 “SAT 求解器”(或 “可满足性” 求解器)的计算工具，这一程序可用于确定某一公式或问题在给定约束条件的情况下是否存在解决方案。

然而关键在于，在用 SAT 求解器解决数学问题时，需要先把问题转译或表示为计算机能够理解的形式。并且，就像豪勒的博士生约尔库所说的：“这一步很重要，非常非常重要。”

当豪勒最初提出要用 SAT 求解器对付考拉兹猜想时，阿隆森心想：“这打死都行不通。” 但他很快就被劝服了，认为这值得一试，因为豪勒发现了一种很巧妙的方式，能把这个古老的问题转化为可以用计算工具处理的形式。豪勒注意到，有一群计算机科学家成功地运用 SAT 求解器为一种称为 “重写系统” 的抽象计算表达找到了终止性证明。

虽然目标距离有点远，但他还是向阿隆森提议道，如果把考拉兹猜想转化为一种重写系统，或许就能得到它的终止性证明(阿隆森曾用小型图灵机对黎曼假说进行编码，帮助将其转化为计算系统)。当晚，阿隆森就把系统设计出来了。对此，他表示 “就像做作业、解趣味题似的”。

阿隆森的系统把考拉兹问题还原为 11 条规则。如果研究人员能为一个以任意顺序应用这 11 条规则的模拟系统找到终止性证明的话，也就能够证实考拉兹猜想了。

豪勒用最顶尖的重写系统终止性证明工具进行了尝试，但没能成功 —— 虽然这是意料之中的事情，但也令人失望。

豪勒表示：“这些工具是为了那些能在分秒之内解决的问题而优化的，但解决考拉兹问题需要数日以至于数年的连续计算。” 这次失败激励豪勒他们队进一步打磨计算方法，并运用他们自己的工具来把考拉兹猜想转换为 SAT 问题。

图 | 考拉兹猜想的 11 条规则重写系统示例(来源：马伦・豪勒)

阿隆森发现，如果放弃11条规则中的一条，问题解决起来会容易得多——这样的结果是一个“类考拉兹系统”，是达成更大目标的试金石。他发起了一项人类对抗电脑的挑战：最先运用10条规则解决所有子系统者胜。

阿隆森徒手上阵，豪勒则腰佩SAT求解器之利剑：他不仅把系统编码成一个可满足性问题——他还巧妙地运用了另一个表示层，把系统转化为以0和1表达的计算机语言——然后让他的SAT求解器在内核上运行，寻找终止性的证据。

(来源：马伦·豪勒)

此处的系统遵循以 27 位首项的考拉兹数列 ——27 在对角阵的左上角，1 在右下角。中间有 71 而非 111 步，因为研究者用了一种稍有不同但本质上等同的考拉兹算法：如果数字是偶数就除以 2，否则就乘以 3 再加 1，再把结果除以 2。

他俩都成功证明该系统按照 10 条规则的可变集具有终止性。有时，对于人类和程序而言，这都是一项微不足道的任务。豪勒的自动化方法最多只用了 24 小时。阿隆森的纯人工方式需要大量脑力劳动，耗时在数小时到一整日之间 —— 他没能证明这 10 条规则的其中一种组合方式，但他坚信只要再努力努力也就能解出来了。阿隆森说：“在最严格的字面意义上，我的对手是终结者 —— 或者至少是个终止性定理的证明者。”

与此同时，约尔库对 SAT 求解器进行了调校，将其校准以更好地适应考拉兹问题。这些手段让情况大大改观，10 规则子系统的求解速度大大加快了，运行时间缩短到了秒级。

阿隆森表示：“剩下的最主要的问题是，11 条规则的完整集怎么处理？如果试着用这个系统跑 11 条规则，那它会无休止地跑下去。我们或许不该对此表示震惊，毕竟这是考拉兹问题。”

在豪勒看来，自动推理领域内的大部分研究都回避了需要大量计算的问题。但基于他此前的突破，他相信这些问题并非无解。有些研究者已经把考拉兹问题转化成了重写系统，但是，只有配合极强的算力大规模运用经过微调的 SAT 求解器才有可能求得证明。

到目前为止，豪勒都是用 5000 个核心(为电脑提供算力的处理单元；消费级电脑通常是 4 核心或 8 核心)来处理考拉兹问题的。作为亚马逊学者，亚马逊网络服务对他发出了公开邀请，允许他使用 “实际上毫无限制” 的资源，也就是多大一百万个核心。但豪勒不太愿意用过多的核心。

他说：“我想或多或少地表现出这是个很实际的尝试。” 不这样做的话，豪勒觉得他就会浪费资源，辜负信任。“我不需要百分百的信心，但我真的想证明这件事有成功的可能。”

“这一自动技术的优美之处在于，你只需要打开电脑，然后等着就行了，” 密歇根大学的数学家杰弗里・拉加利亚斯(Jeffrey Lagarias)如是说。他已经和考拉兹猜想缠斗了差不多 50 年，俨然是其相关知识的守门人，著作等身，还编辑了一本关于考拉兹猜想的题为《终极挑战》的书。

对于拉加利亚斯而言，这个自动化方法让他想起了普林斯顿的数学家约翰・霍尔顿・康威(John Horton Conway)于 2013 年发表的一篇论文，后者在文中称，考拉兹问题可能属于一类难以捉摸的问题，它们是真实的，且具有 “不可判定性”—— 但又不能证明其不可判定。

正如康威所言：“…… 甚至对于它不可证明的断言都是不可证明的，然后，对于其不可证明的断言是不可证明的这一断言，亦无法证明，以此循环往复。”

拉加利亚斯表示：“如果康威是对的，那不管用自动化的方法还是靠手解，考拉兹猜想都是无法证明的，并且我们永远不会知道确切的答案。”

目前，可以说是最接近证明考拉兹猜想的人类是 UCLA 的数学家陶哲轩(Terence Tao)。陶在 2019 年证明考拉兹猜想对于 “几乎” 所有数都 “几乎” 正确(他的 “几乎” 基于两条技术性定义，但也符合英语的日常语义)。

陶相信，对该猜想的人工证明 —— 了解其个中缘由 —— 比计算机证明在数学的层面上更有意义。他同时表示：“但是，自动化证明工具如果能解决重大的未解难题的话，就会极大地推动数学家在工作中运用计算机的方式发生革命性的转变。对于考拉兹猜想这个级别的难题，我们会接纳任何洞见。”

然而，通过在考拉兹问题上运用自动化方法，豪勒及其同僚真正追寻的是这样一种场景：电脑在特定问题上战胜了人类，或者人类反过来战胜电脑。“在当前的时间节点上，我们无从知晓究竟是这些技术比人类靠双手所能做到的事情更强大，还是人类能做到电脑无法完成之事，” 豪勒说，“我们想知道，究竟是人类还是计算机更善于解决此类问题。”

为了得到答案，咱们就拭目以待，看看谁能先证明考拉兹猜想吧。

-End-

原文：

https://www.technologyreview.com/2021/07/02/1027475/computers-ready-solve-this-notorious-math-problem/