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

一直以来，学计算机的总是要先学数学与算法，计算机科学家好像比数学家低人一等。现在计算机科学家Lamport认为传统xy数学公式有漏洞，采取对象结构证明方法更好，你是不是扬眉吐气了呢？

赢得2013计算机图灵奖的Leslie Lamport发表了一篇编写21世纪证明文章，文章分析传统数学公式缺点，指出为什么我们还使用17世纪的数学方式？提出了使用软件编程中对象结构化层次方式编写数据证明的观点。

Lamport认为：传统数学家编写证明的方式易于阅读，不容易出错，确实比使用文字的散文方式证明要严谨得多，"当你编写证明时，你试图做两件事，一方面你要显示一些事情是美丽的，但是另外一方面你要证明它是真的，真的东西也许美丽，是一种美丽的真实，但是你无法证明这两个方式是相同的"

Evelyn Lamb在A Computer Scientist Tells Mathematicians How To W一文对此进行了分析：

无论相信与否，我有朋友自称不喜欢数学，在Facebook也有一些这样观点的人，撒旦说：将字母放入数学，虽然每个人有自己的不同成长背景，但是文字总是共同经历的，是相同的，但是还是有一些人因为数学课上的抽象符号而停止学习兴趣。

Lamport的新式数学证明方法是一种层次结构方式，似乎与大多数在中学或高中几何课上学习的两行式 two-column 证明证明没有什么不同，但他指出，在处理复杂问题时，两行(栏)格式是笨拙的，每行编号，每个断言都是使用指向前面行或断言的数字证明。

Lamport援引Michael Spivak的微积分课文：”精密和严谨既不能妨碍直觉，本身也不是目的(只是手段)，公式是自然的媒介，我们使用它思考数学问题“，Lamport然后指出教材中值定理的推论证明不够准确或严格，他使用自己的技术重写了证明。

Lamport说他的技术不仅对阅读证明的人有利，而且是一种在自己工作中更好的发现错误的方法，从而阻止这些错误公开发表。他说在一些小型调查研究中发现，大概有三分之一的出版数学论文中包含假定理，这些定理是假的因为推导这个定理的证明是错误的，还有的假定理是因为依赖错误的证明，无论什么原因，假定理就不应该让它出版(banq注：这大概是传统数学使用xy之类公式证明碰到的尴尬)。Lamport的证明结构能阻止草率思想侵入我们的写作。(共同为Heidelberg Laureate Forum编写博文的Marcus Pössel也写了一篇文章拓展Lamport的思想)

Lamport建议如果出版杂志只是以17世纪证明格式，那么数学家应该以一种方式来确保他们的证明是滴水不漏的，一个作者可以使用超文本发表其结构性证明，这样能让读者自己来隐藏或显露每步细节，包括证明每一步中的主要思想总结。

Lamport还指出他的结构证明方法容易改变，你可以稍微改变一个假设前提，或聚焦不同性质的解决方案，你很容易能告诉大家证明的哪部分还是和以前一样，而哪部分需要改变。

[该贴被banq于2015-01-30 10:26修改过]
[该贴被banq于2015-01-30 10:26修改过]