摘要：在这样丰富多彩的数学世界中，有一种初看起来极为朴素的证明方法，承担着一些最复杂数学难题，这就是“穷举法（Proof by Exhaustion）”。

本文来源：遇见数学

当数学遇上“穷举”

在这样丰富多彩的数学世界中，有一种初看起来极为朴素的证明方法，承担着一些最复杂数学难题，这就是“穷举法（Proof by Exhaustion）”。

穷举法(Proof by exhaustion，又称为“暴力搜索法”、“枚举法”、“分类证明”)通过逐一检查所有可能情况来验证命题。

这名字听起来似乎颇有些“笨拙”，但它却在数学史上屡立奇功，甚至在现代计算机辅助下，仍然发挥着不可替代的作用。

穷举法的朴素起源

其实，我们在日常生活中都曾无意或有意中用过穷举法。想象一下，你再找一支不见了的钢笔，可能会逐一翻开桌上的文件、桌下、抽屉、…。这种“逐个排查”的方法，就是一种典型的穷举策略。

在数学领域，这种方法被形式化为“穷举证明”，即将一个复杂的问题拆分为有限个具体的情形，然后再逐个验证每种情形是否成立。只有当所有可能的情况都被逐一验证之后，数学家才敢宣告：“这个命题已经被证明。”

我们可以考虑一个有趣而简单的例子：

命题：任何整数的立方数要么是 9 的倍数，要么比 9 的倍数大 1 或小 1。

乍看起来，这个结论似乎并不明显，但穷举法可以轻松证明。

第一步：把所有情况列出来

任何整数 除以 3 的余数只能是 0、1 或 2。因此我们可以将所有整数分为三类：

这三类穷尽了所有可能性，接下来逐一验证。

第二步：逐个验证每种情况

情况一：

那么：显然是 9 的倍数。

情况二：

前三项都是 9 的倍数，加上 1，所以整个表达式是比 9 的倍数多 1。

情况三：

同样，前几项是 9 的倍数，最后减 1，所以整个结果是比 9 的倍数少 1。

所以这三种情况都符合我们的命题。

结论：命题成立。Q.E.D.

上面三个情况覆盖了所有整数的可能性，因此我们成功地用“穷举”验证了这个命题。

穷举法的威力与局限——从简单枚举到计算机辅助证明

虽然穷举法看上去朴素简单(甚至有些笨拙)，但随着问题的复杂程度增加，其所需验证的情况数量也会急剧增长，甚至达到天文数字。仅凭人工计算，变得不现实并且极易出错。

幸运的是，现代计算机的出现改变了这一点。计算机最擅长的，恰恰就是快速、精确、不知疲倦地处理大量重复性的任务。

1976 年，数学史上首个由计算机辅助完成的重要定理——四色定理（Four Color Theorem）的证明，就是采用了穷举法。当时，数学家们将所有可能出现的地图情况，归纳为 1936 个基本情形，然后逐一用计算机进行验证。这个过程虽然引起了数学界的争议——毕竟人类无法亲自审阅每一步运算——但却彻底改变了数学家对穷举法的态度，展现出其强大的潜力。

目前已知最短的四色定理证法仍需划分超过600类情形.

此后，诸如“有限单群的分类问题”、“布尔毕达哥拉斯三元组问题”（Boolean Pythagorean triples）和著名的“开普勒猜想”（Kepler conjecture）等著名难题，也纷纷借助计算机的强大处理能力，通过穷举法获得了突破性的进展甚至完全解决。

然而，穷举法缺陷也显而易见。首先，它只能处理有限种情况，而绝大多数数学问题涉及无限集合；其次，穷举法的“逐一排查”式证明，往往缺乏数学家眼中的“优雅性”和“深刻性”。

正因为如此，数学家们通常更倾向于寻找更加深刻、更加优雅的证明方法，比如数学归纳法、反证法、构造法等等，以期揭示问题背后的本质规律。然而，现实情况却是，并非所有问题都能如愿以偿地获得优雅解答。有些难题至今为止，除了穷举法以外尚未发现更好的证明方式。

例如，“有限单群分类问题”被誉为 20 世纪数学最伟大的成就之一，这个问题的证明跨越了数十年，涉及几百位数学家的共同努力，最终形成了成千上万页的证明文献。如此庞大的工作中，相当一部分正是依靠穷举法完成的。即使到了今天，这些问题也依旧让人怀疑：是否存在更加优雅、更具“深刻洞察”的证明方式？

数学的魅力或许正体现在这种样的矛盾与平衡之中：一方面，数学家不断追求简洁、深刻的优雅解法；另一方面，又不得不承认，有些时候只能暂时接受“穷举”的实用，等待更深邃的洞见(工具)出现。

来源：人工智能学家