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

15-01-30 banq
                   

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

                   

4
ericyang
2015-02-04 10:54

2015-01-30 10:18 "@banq"的内容
精密和严谨既不能妨碍直觉,本身也不是目的 ...

看起来好像搞计算机的要革数学的命,说白了就像写小说的要造文字的反一样,呵呵,没有必要。

其实,他就是想说计算机证明数学题更好,这个有先例啊,比如希尔伯特第8问题,好像就是计算机解决的吧。不过,这位老兄显然对数学了解甚少,就像人脑怎么思考的,再给计算机几千年的发展,也是模拟和替代不了的,就是'复杂性'。

再者,这位作者开始批评数学的证明方式,其实也有点荒谬了,数学证明步骤也仅仅是手段,你想怎么证明都行,只要保证你的每一步都是正确的(所以那个1/3都是假定理,不知道哪里做的所谓小型调查,决不可信。banq,你批注这是尴尬,这种调查本身就不严谨你还信,呵呵)

通篇看完,我只能说,数学,仍然只能是天才的乐园,用模式/结构的方法来替代过程解决数学题?就像我们想用设计模式来解决需求问题一样,本末倒置。。。

ericyang
2015-02-04 13:11

2015-02-04 10:54 "@ericyang"的内容
老兄显然对数学了解甚少 ...

好吧,我有些武断了,此君居然大名鼎鼎,LaTex -- 曾经多么熟悉而使用过的东西,居然是他的!!!看他经历,和我居然有交集,失敬,呵呵。

ok,回正题,看了他的文章,简单说就是一段话'假设一个区间有2点a和b,a<b',很熟悉的证明开始吧,但作者说no,这个开始本来就没有被证明,谁证明区间一定能找到2个这样的点?于是有了所谓的1/3的假定理。意思是,至少,你在论题上就得指出,这是个前提假设,在此基础上才能证明,所以证明过程中的每一句描述性文字,都必须纳入假设,,,于是乎,有了他的结构 -- 严谨而合理。

不过多体会和理解,仅此。