能用数学归纳法做证明题的 Wolfram|Alpha

世界第一个不受语法束缚的基于数学归纳法的Proof Generator于2016年在 Wolfram|Alpha上闪亮登场，它的设计和创建离不开创意、行动力和优秀资源的整合。

创作动机

Wolfram | Alpha是学生们尤其是大一学生学习数学课程常用的工具。 事实上，当我向学生们解释我在Wolfram | Alpha的工作时，从他们那里得到的最常见的一个回答就是："OMG，这个网站是我学习微积分的救命稻草。"他们通常是在说微分方程求解器，或Wolfram | Alpha的导数和积分功能。

高中和大学一年级所学的大部分数学知识以计算为基础，题型与上面提到的这些功能类似。试题经常以下列形式出现：

• 求 x
• 求 f(x)的导数
• 求下列方程的根

计算型问题通常涉及一系列计算 （即步骤） 以获得最终结果。可以通过计算解决的问题使用的方法往往是重复的。一旦学生掌握了与这类问题相关的步骤和规则，基本就能够解决作业或考试中出现的与这类问题相关的任何问题。这是因为基于计算的问题有一套循规蹈矩的方法。与学习函数的导数类似，一旦学生掌握了"求导规则"，解决这些问题不过就是反复应用这些规则而已。

那么，问题来了，对于那些与计算无关的数学问题呢？ 更具体地说，对于没有什么规则或方法的数学问题，学生该如何学习和练习？当我还是一个学习离散数学的一年级学生时，我遇到了这个问题。 学习的是数学归纳原理的证明，我将在后面简要介绍一下背景。 这个内容与我以前在数学课上学到的任何知识都不同，原因有两个：

• 证明不是计算。 一套规则不能适用于所有问题。
• 证明没有一个唯一正确的最终答案。

数学问题没有一个简单、明确的答案是很奇怪的想法。 如果一个学生在测试中解方程，他们可能会写上五行步骤，然后最后写上最终答案，比方说以"x = 21"的形式。 然而，数学证明并不是那样的。 事实上，步骤本身就是"答案"。 证明的目的是逻辑地说明为什么某些论断是真的。

假设你正在玩谋杀悬疑图版游戏Clue（或Cluedo，中文名称"妙探寻凶"）。游戏的目标是确定凶手是谁，使用的武器以及犯罪地点。如果谁说出这样一句话："Mustard上校拿左轮手枪在餐厅。"他就赢了。现在想象一下，不是试图找出这些信息，而是在游戏开始时就告诉你凶手是谁，使用什么武器，以及犯罪地点。现在的目标不是确定结论（因为你已经被告知），而是搞清楚为什么这是真的。根据你自己的卡片和游戏过程中暴露的信息，最终应该能够使用逻辑证明为什么在游戏开始时被告知的信息一定是真实的。这样，你可以通过陈述某些内容来在游戏中获胜，"因为我手里有除了左轮手枪之外所有的凶器卡，而且Joe有除了餐厅之外所有的位置卡，而且根据你们出过的牌，我知道你们手上都没有那张Mustard上校，所以我证明了所指控的凶手是真的。"

我并不想说明上面这个Clue游戏的变形有多好玩，实际上正好相反，它变得一点意思都没有了。我讲它的目的是想说明证明所表示的问/答格式。下面是一道一年级学生可能会在考试中遇到的归纳法证明题：

用数学归纳法证明：对于 n > 0，8^n - 3^n均能被5整除。

当n > 0时，8^n - 3^n能被5整除这个推断是完全成立的（假定n为整数）。但这里是让学生从逻辑上证明这个结论成立。就像上例中对游戏Clue的变形一样，信息在游戏开始就告诉了你， 然后要证明它是真的。对大多数学生来说, 写出这些证明并不简单，而且往往是最难掌握的数学概念之一。

鉴于这些问题的复杂性，学生们常常求助于互联网资源（如Wolfram|Alpha）。如果学生需要求解一道微分方程，并希望验证答案，他可以将问题交给Wolfram|Alpha，Wolfram|Alpha不仅会给出最终答案，还会给出求解过程。这同样适用于求导、积分、化简表达式等等。但证明题呢？

我们已经确定，证明题不同于计算题。据我所知, 至今没有任何计算器或在线工具能够为证明问题提供解决方案。

我清楚地记得一年级的时候, 我想检验作业题中一道证明题的解。我已经写出了自认为正确的解。但怎么检验我的答案是否正确？令人惊讶的是, 只有两种方法可以验证我的证明的正确性:

• 找到与在线示例完全相同的证明(非常罕见)
• 与班上其他同学的答案比较，假定如果我们的答案相同，则我们一定都正确 (错误假设)

那么为什么在线"导数计算器"很容易找到，而"证明计算器"却如此困难呢？

主要是由于这一事实——证明通常被视为是不可计算的。由于同一组规则不能用于覆盖100% 的证明，计算机难以创建证明所组成的逻辑步骤。我解决这个问题的方法是，建立一个与模式匹配的证据库 (如下所述)。这种方法证明了计算在构造证明中起着作用, 一个可行的 "证明生成器" 应运而生。

原型

在一个夏天, 我开始建立一个应用程序原型, 它能够使用数学归纳原理 (PMI)执行有限数量的证明。PMI 是证明一个命题是否成立的常用方法，把这个方法想成一列很长的的多米诺骨牌也许更容易理解一些。首先, 你要证明, 第一个多米诺骨牌会倒。第二, 你要证明，只要任意一张骨牌倒了，那么与其相邻的下一张骨牌也会倒。通过证明这两个事实, 你就可以证明, 如果第一个被推倒, 所有的多米诺骨牌都会倒下。

多米诺骨牌的例子很好地说明了归纳证明背后的逻辑，有两步组成：

• 起始步骤（第一张多米诺） ：验证命题在起始时成立（n取最小值），也就是说，如果要证明某个命题在n >= 1时成立，起始步骤就要证明命题在n = 1时成立。
• 归纳步骤（后续的多米诺）：这是更具挑战性的一步。在归纳步骤中, 假设命题对于某个值 (即 k) 成立，然后尝试证明对于 k + 1 亦成立。

如果这两个步骤都正确完成, 则证明完成。

在开发这个应用程序之前，我曾与我本科时的一位大学 (阿尔戈马大学) 教授探讨。他将这一具有挑战性的想法比作制作一本包含世界上所有食谱的食谱书。你可以不断添加尽可能多的食谱，但它基本上不可能包括曾经出现过的所有食谱。同样, 我可以不断提高证明题的覆盖率，但我永远不能将每个用户将要求的证明囊括。

虽然有相当明显的局限性, 但我换了一个考虑问题的角度。我想，如果一个烹饪新手想要一本食谱, 它可能会是一个相当厚的食谱。他们可能想尝试各种各样的食谱。同时, 他们不太可能想把Gordon Ramsay的名菜Beef Wellington列入食谱。准备那道菜的难度对于一个烹饪新手来说可能太高了。同样道理，对于学习证明 (大学一年级) 的新生来说, 他们很可能不需要访问太过高深的证明资源。只要他们的资源可以应付一年级的证明题, 那么在他们看来资源就足够充分了。这是我在研发规划阶段作出的重要区分。

在原型开发过程中, 我很快就遇到一个迫在眉睫的挑战。我理想的应用程序能够对付的许多证明都涉及到简化表达式, 这本身就是一个非常复杂的程序。这时，我第一次发现了Wolfram|Alpha的API。使用其 API，我可以简单地直接调用Wolfram |Alpha (即化简表达式), 并将结果返回到我的应用程序。我使用 API时遇到几个具体的问题, 所以我决定直接联系Wolfram|Alpha。

电话那头的工作人员很快回答了我的问题，然后话题转到了我没想到的方向。在我解释了正在构建的小应用项目之后, 他让我把这个应用向Wolfram|Alpha的另外几位成员演示（当然事先签署了保密协议）。当时，这个应用程序能够处理的证明还相当有限，但作为一个原型或概念的证明表现还是相当不错的。演示进行得很顺利, 但再一次，谈话的方向让我始料不及。几个星期后，我收到了Wolfram|Alpha的职位聘书，作为数学内容开发人员，我接受了。

工作原理

我在第二个夏天，搬到了伊利诺伊州香槟，Wolfram|Alpha的总部。在这里, 我参与了在网站上添加数学功能的几个项目。但我的主要精力还是重新实现我的归纳证明计划，使其成为Wolfram|Alpha的一部分。

这个项目的目标是解决学生在一年级课程中遇到的任何归纳证明问题。为了使这成为现实, 我搜遍了互联网和教科书, 寻找所有的归纳证明问题。

需要解释一下的是，这个项目并不是我能找到的所有归纳问题的数据库。为了使程序能够适用于所有证明 （甚至是它以前没有见过的），我首先需要归纳学生正在学习的归纳证明题型。早期的决定是, 该程序将处理三种主要类型的证明：

• 求和/乘积等式，如：证明 1 + 2 + 3 +\[Ellipsis] + n = n(n + 1)/2, 其中 n > 0
• 表达式整除性，如：证明8^n \[Dash] 3^n能被5整除，其中 n > 0
• 表达式不等式，如：证明 2^n > n^3，其中 n > 9

通过使用这三种主要的证明类型，我进一步将查询类型分解为更具体的证明子集。下面用一个例子予以介绍。

比方说我们想要证明以下命题：

证明8^n - 3^n能被5整除，其中 n > 0

不是把证明的全部过程生硬地编成代码，我想让它尽可能具有一般性，以便能适用于更多的证明。因此，我没有在应用程序中添加非常具体的证明, 而是添加模式匹配的证明。

表达式8^n - 3^n中，我对8和3并不太关心，因为即便这些数字变了，证明的逻辑结构仍不会改变。也就是说，如果用户要证明的是10^n - 3^n能被7整除，步骤不会有任何变化，变的只是数值。为了利用这一点，我将为这种类型写了一个证明解决方案:

证明a^n - b^n能被d整除，其中 n > x。

将用户的输入进行模式匹配, 如果检测到用户的查询以此形式 (即遵循此模式), 则将根据此结构输出证明。然后提取变量(a, b, n, d, x), 以便为生成的证明提供值。

这个概念在许多不同结构的证明查询中得以应用。模式匹配方法似乎效率很高，基本涵盖了我在网上和教科书中遇到的大多数证明题型。任何查询， 即使先前并没有遇到过，只要它与应用所知道的一个结构模式相匹配，即可生成证明。

但是, 特定模式匹配实际上仅用于表达式整除性和表达式不等式查询类型。对于求和/乘积等式, 可以遵循特定的数学方法，应用程序理论上能够100%处理，而无论等式的右手表达式或求和/乘积的内容如何。此方法适用于求和等式的证明和反证。这是一个很好的功能, 因为它确保了此查询类型的归纳证明的完整覆盖率, 前提是Wolfram|Alpha不会由于输入过大而超时。

对于表达式的整除性, 生成的大多数证明仅基于与输入匹配的模式。然而，对于给定表达式没有成功匹配模式的情况，还有个适用于一般情况的算法可以作为最后一搏。该算法对表达式执行某种操作, 试图将表达式放入一个特定形式中。这种形式不过是两项的加和，其中一项是归纳假设, 另一个包含具有给定除数作为因子的系数。如果此操作成功, 则可以生成证明。否则将失败。

对于表达式不等式，所有生成的证明都是模式匹配的, 因为我还未发现有什么一般算法能应用于表达式不等式证明。对两个表达式之间的差异进行模式匹配则更有意义。这不仅有利于不等式运算, 也是消项的一个关键步骤。例如, 下面是一个可能的查询:

证明2n + 7 + sin(n) < (n +7)^2 + sin(n)，其中n > 0。

理想情况下，生成的证明与以下内容的模式匹配：

证明 a n + c < (n + b)^d，其中 n > g

问题是模式匹配表达式在不等式两边都不包括sin(n)。但是，如果取表达式两侧的差值（例如左侧 - 右侧），则新查询将是2n + 7 - （n + 7）^ 2，这与 a n + c - (n+b)^d 的模式匹配。

同样重要的是要注意，这些变量中有些有时是可选的（即等于0或1），例如是常数、系数和指数。

一开始测试该应用程序时，我注意到有两种类型的查询一直生成错误的证明。 虽然目标是尽可能多地包含各种证明，但是生成一个数学上不正确的证明，其后果远比根本不生成证明严重得多。 一旦应用程序开始生成无效内容，应用程序的质量和可靠性就会大打折扣。

生成无效证明的第一种查询类型可以通过下例说明：

证明 4n + 7 > 2^n，其中 n >= 0

在此示例中，初始情况（n = 0）正确通过（因为7> 1）。 然而，由于实际的命题是错误的（即当n = 5时，27 >32不成立），归纳步骤失败。 但无论出于何种原因，该应用程序试图生成一个归纳步骤，以使证明有效。 这导致了错误，需要被淘汰。 归纳法对于验证命题成立非常有用，但对于否定命题则并不理想。 因此，对于表达式不等式的查询，如果初始情况成立但给定查询为假，则不生成证明（或"反证"）。

生成无效证明的其他查询类型，可以通过下面这个例子说明：

对于n >= 0，求证 4n < 2^n

这个例子其实相当棘手。左右两侧表达式的大小可以通过下图直观地说明：

本例的初始情况是当n = 0时，原式即 4(0) < 2(0)，化简后得到0 < 1，显然成立。由于初始情况成立，可以进行接下来的归纳步骤。和前面的例子一样，这个查询也生成了无效的归纳步骤。问题是归纳步骤的许多计算需要假定 k 在一定范围内。例如，在上面的证明中，其中一步依赖于k >= 2时，3 < 2^k这个事实。然而，当k值的范围在0和k >= 2之间时，其中n = k，并没有证实"4n < 2^n"这个命题成立。因此，初始情况必须也要把 n = 1 和 n = 2包括进来。注意"修正后的证明"需要n > 4，因为 n = 4 的情况对于 4n < 2^n 不成立。

如果在归纳步骤中进行的运算要求n> = 2，而初始情况是n = 0，那么我们并未证明查询对于n = 1或n = 2成立。这与悖论"所有的马都是同一种颜色" 非常类似。解决这个问题的方法并不是将证明完全删除。相反，如果在归纳步骤中做出任何假设，则初始步骤将测试n的多个值。 因此，查询4n <2 ^ n在初始情况下即失败，因为对于n = 1，它不成立。

该个课题的最后一项挑战涉及自然语言处理（NLP）。 允许用户用英语提问，并让Wolfram|Alpha理解他们的问题。虽然我之前没有任何NLP的实战经验，但Wolfram | Alpha现有的解析/扫描架构使NLP与应用程序的集成变得相当容易。主要挑战是确定用户在就一道归纳法证明题向Wolfram | Alpha提问时的所有可能方式。这将是一个持续的开发过程，因为不同的查询语句仍在不断地添加进来。

应用程序的使用

这是该应用程序在 Wolfram|Alpha上的截屏：

如果您是Wolfram | Alpha Pro用户，可以通过单击"Step-by-step solution"（分步求解）按钮看到生成的证明。 而上述内容所有用户都能看到。 附加信息已添加到应用程序中，以便向用户提供重要的详细信息。 一项功能添加了此结果页面，即在证明无效时建议使用不同除数。

以下是"修正除数"后生成的证明的截屏：

对于所讨论的具有多个初始情况的例子，生成两个证明：一个显示初始证明（无效），然后是第二个证明，推荐不同的初始情况以使证明有效：

最后一个很酷的功能是，如果一个求和/乘积等式证明无效，将用推荐的新表达式进行修正：

结语

2015年10月15日，也就是我开始设计原型程序大约十五个月后，该应用程序在Wolfram | Alpha上正式发布了，这一天令我终生难忘。六天之后，在我的二十一岁生日当天，我在Wolfram技术大会上介绍了这个应用程序。这个项目获得的成功和热烈的反响远远超出了我的想象。通过一个想法和一点主动性，我来到了世界上最大的计算知识引擎所在的团队，成为了其中一员，并且已经工作了一年多。该项目的目标是产生归纳式证明，而这个项目的整个开发过程也是想象力、原创性和努力工作能带来高回报的完美证明。