计算机科学家告诉数学家如何撰写证明

本文发表于《大众科学》的前博客网络，反映了作者的观点，不一定反映《大众科学》的观点

信不信由你，我确实有一些朋友会说他们不喜欢数学，他们时不时地会在 Facebook 上分享这个梗图：然后撒旦说：“把字母表放进数学里。” 每次这个梗图出现时，背景图片都不同，但文字总是相同的。有些人觉得抽象符号是数学课开始让他们感到困惑的地方。

但是如果我们没有那种符号呢？在本学期我的数学史课上，我们了解了在我们（撒旦？）将字母表放入数学之前，数学是什么样的。具体来说，我们和花拉子米一起完成了配方法，这位波斯数学家撰写了关于求解线性和二次方程的教科书，这本书给了我们“代数”这个词。他没有使用符号来表示未知量，所以他的书中包含这样的说明

“一个平方和 10 个根等于 39 个单位。因此，这类方程中的问题如下：哪个平方与它的十个根组合起来会得到总和 39？解决这类方程的方法是取刚才提到的根的一半。现在我们面前的问题中的根是 10。因此取 5，它自身相乘得到 25，将这个量加到 39 得到 64。然后取它的平方根，即 8，从中减去根的一半，5 剩下 3。因此，数字三代表这个平方的一个根，它本身当然是 9。因此，九给出了平方。”

关于支持科学新闻

如果您喜欢这篇文章，请考虑通过以下方式支持我们屡获殊荣的新闻事业 订阅。通过购买订阅，您正在帮助确保有关塑造我们当今世界的发现和想法的具有影响力的故事的未来。

今天，我们会将该段落翻译成这样

x²+10x=39。求 x²。

x²+10x+5²=39+5²

(x+5)²=64

x+5=8

x=3

x²=9

我认为我们大多数人，包括我那些对数学有恐惧症的 Facebook 朋友，都会发现第二个版本更容易理解和遵循。正如我对我的班级所说，唯一比在数学中使用字母表更糟糕的事情是在数学中不使用字母表。

本周，我正在参加海德堡桂冠论坛，这是一个类似于林道诺贝尔奖获得者论坛的数学和计算机科学论坛，并且为论坛博客撰写文章。周二，莱斯利·兰波特，他在 2013 年获得了计算机科学领域的图灵奖，做了一个题为“如何撰写 21 世纪的证明”的演讲，演讲的开头与我的历史课和我所做的观察相同：公式比散文方程更容易阅读和解析，所以当我们在撰写关于数学的文章时，我们已经超越了散文方程。那么，为什么数学家坚持用散文来撰写证明，就像 17 世纪的数学家那样？

莱斯利·兰波特身穿一件写着“你想要证明？我会给你证明！”的 T 恤衫在海德堡桂冠论坛上做了演讲。图片来源：HLFF/Kreutzer。

当我看到演讲的标题时，我以为兰波特会谈论计算机证明检查程序，甚至是像蒂莫西·高尔斯所研究和撰写的那样的证明创建程序。但兰波特的建议要实际得多。他实际上是在描述一种让数学家撰写更容易阅读且更难出错的证明的方法，这种方法可以替代冗长的散文证明。“当你撰写证明时，你试图做两件事，”兰波特在稍后与媒体的会议上说。“一方面，你想展示某些东西是美丽的，但另一方面，你试图证明它是真实的。真理可能是美，美可能是真理，但你不能用同样的方式来证明它们。”

他的方法，您可以在他的网站上阅读更多详细信息 (pdf)，是一种分层结构，它看起来与我们大多数人在初中或高中几何课上学到的双栏证明并没有完全不同，尽管他指出它可以处理在这种双栏格式中会显得笨拙的复杂问题。每行都编号，并且每个断言都用引用前几行和断言的数字来证明。

兰波特引用了迈克尔·斯皮瓦克的微积分教科书：“……精确性和严谨性既不是对直觉的阻碍，也不是目的本身，而是构建和思考数学问题的自然媒介。” 然后，他带领我们浏览了该教科书中值定理的推论的证明，指出了他认为不够精确或严谨的陈述，并使用他的技术重写了证明。

兰波特说，他的技术的好处不仅在于，甚至主要不在于它对读者的价值。它也是一种更好的方法，可以找到自己工作中的错误，并防止它们进入已发表的作品。尽管他承认确切的总体数字尚不清楚，但他表示，在一项小型研究中，1/3 已发表的、经过同行评审的数学论文包含错误的定理。其中一些是错误的，因为证明是错误的，而另一些是错误的，因为它们依赖于错误的证明。无论原因如何，错误的定理都不应该发表，兰波特说他的证明结构使我们不会让草率的思维侵入我们的写作。（海德堡桂冠论坛的联合博主马库斯·珀塞尔也撰写了关于兰波特演讲的文章，并扩展了他关于清晰写作的一些想法。）

兰波特建议，如果期刊坚持只发表“17 世纪”的证明，数学家也应该无论如何都写出来，以此来确保证明是万无一失的。作者可以将分层证明发布在其网站上，或许可以使用超文本来允许读者隐藏或显示每个步骤中的详细信息，或者在证明的每个步骤中包含主要思想的摘要。

在与媒体的会议上，兰波特谈到了这项技术的另一个好处，他在演讲中没有时间谈到。他说，一旦你有了分层证明，你就可以很容易地在新证明中使用它的片段。例如，如果你想稍微改变一个假设或专注于具有不同属性的解决方案，你将能够很容易地分辨出证明的哪些部分可以保持不变，哪些部分需要改变。

这次演讲引发了很多问题，我听到与会者整天都在讨论它。并非所有在场的数学家都对一位计算机科学家（即使是一位拥有数学博士学位和图灵奖的计算机科学家）告诉他们如何撰写证明感到兴奋。他们中的一些人强烈地认为，分层证明会损害他们作品的美感。有些人认为，这种技术可能适用于教学环境中的简单证明，但不可能适用于研究环境中的更复杂证明。我认为兰波特会争辩说，如果你认为你不能以这种形式撰写你的证明，那么你对证明的理解还不够。

就我个人而言，我发现兰波特的论点很有说服力。用文字解释的代数方程和用符号解释的代数方程在清晰度上的差异就像白天和黑夜一样，如果兰波特是对的，那么切换到这种证明技术会引起类似的清晰度飞跃。改变是困难的，但我对它对我教学、思考和沟通的潜在好处很感兴趣。

这篇博文源自第二届海德堡桂冠论坛 (HLF) 的官方博客，该论坛于 2013 年 9 月 21 日至 26 日在德国海德堡举行。24 位阿贝尔奖、菲尔兹奖和图灵奖得主将齐聚一堂，会见 200 位年轻研究人员的精选小组。