计算机科学家告诉数学家如何编写证明!
一直以来,学计算机的总是要先学数学与算法,计算机科学家好像比数学家低人一等。现在计算机科学家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修改过]