不会用狗，硬伤啊。难怪您的科学素养只能让人客气呢。
[评论]为什么越出国越爱国？听听海外党们自己的故事
- 主题发起人 小晴猫
- 发布时间 2016-01-27
看一篇两位搞数学的人写的文章，张景中好像很有名，注意到了下面这一段，
我们知道吴的领域是几何定理机器证明，是机器证明里的一小块，说是机器证明的奠基人，就比较可笑了。
现在已经实现的几何定理可用机器求解，所生成的解答其推理过程的简洁优美可以与人工解答媲美。虽然解决的只是一小类数学问题，远没有达到解决四色定理、哥德巴赫猜想一类难题的水平，但至少说明了机器证明和人工证明之间并没有不可逾越的鸿沟。人类的创造力再一次得到展现。
----------------------
机器证明可靠吗
作者：彭翕成, 张景中
用机器证明的数学定理中，最为人津津乐道的当属四色定理。100多年以来，数学家们为证明这条定理绞尽脑 汁，所引进的概念与方法刺激了拓扑学与图论的发展，但一直没有得出证明。1976年,美国数学家阿佩尔与哈肯借助电子计算机,用了1200个小时，作了上 百亿次判断，终于完成了四色定理的证明，轰动全世界。美国邮局为此在一些明信片上加盖邮戳：“四色足够了！”
当一些数学家为一个高难度的定 理得到解决而庆祝时，更多的数学家却对计算机给出的证明表示质疑。质疑的理由有二。一是对于相当多的定理证明，特别是那些被称为“下金蛋”的数学问题，最 重要的意义不在于论证最终的真假，而是在求证过程中不断发现的新方法。二是计算机凭借高速计算能力作出的所谓证明,数学家无法人工检验,谁知道中间会不会 出错呢?
计算机得出的结果，有些是容易检验、容易相信的。例如，把某一个很大的整数分解为两个大于1的整数的乘积，这是破解一类密码的关键任务。大型高速计算机工作几个月才分解了一个整数，人只要几分钟就能检验结果是否正确。
类似地，计算机算出来的方程解是否正确也不难检验，但定理证明是另一回事。在例证法中，面对计算机用10万个例子证明了的一条几何定理，我们会有什么想法？与此类似，用代数方法经过成百上千项的多项式计算而证明的几何定理，我们会有什么想法？
我们可以相信某一条被计算机宣布成立的定理前提，认为计算机的硬件是可靠的，计算机的操作系统是可靠的，机器证明软件的程序是可靠的，程序依据的算法和理论是可靠的。
算 法和理论的可靠性，通过学习和讨论，不难确认。其他几种可靠性，可以经过大量实践验证。譬如让另外一批人，用另外的算法编程，用另外的机器运行，假如推导 出来的结论与之一致，那么可靠性得到了增强。因为一个定理，反映一个客观事实。这个事实不会因发现的人的不同而改变，同样也不会因为证明程序的不同而改 变。这样做，从哲学上看，是不是改变了数学真理的性质呢？
另一种方法，是计算机给出人工能够检验的证明。1976年，中国科学院的吴文俊院 士发表了检验几何命题的有效的机械化方法。吴法的成功激起了几何定理机器证明的研究热潮。到1992年，基于几何不变量的消点方法出现，实现了几何定理可 读证明在计算机上的自动生成。这一工作被国际同行誉为计算机处理几何问题的里程碑。
伴随着计算机技术的进步，直到1996年出现了基于前推模式的 “几何信息搜索系统”，成功地证明了上百个非平凡的几何命题，收到了良好的效果。
人们对机器证明的反对，多半集中于它的繁琐和不可检验。
在 计算机还没发明的时候，就有数学家提出机器证明（设计一种机器代替人推理）的设想，遭到了很多数学家的反对。数学大师庞加莱认为：“你可以将牲畜赶到机器 的前端，机器将其宰杀后储存成罐头输出。难道你可以把定理的条件送到机器的前端，机器自动输出结论吗？这实在是不可思议！”
在四色定理被机 器证明之后，反对声仍然强烈。有评论认为：“机器证明破坏了数学的优美。一个好的数学证明应当像一首诗—而这纯粹是一本电话簿！”普林斯顿大学数学教授约 翰·康威更是在接受《纽约时报》采访时说:“我不喜欢它们（计算机证明），因为你感觉不知道究竟发生了什么。你不能从中获得任何新的见地。”持这种观点的 数学家不是个别的，他们认为如果一个难题被一种新方法解决了，这是一件了不起的事情。但是如果解决的方案只是现存方法的反复使用，那只能证明解决者的聪明 而已。这不利于数学的发展。
还有人指出，传统数学研究四色定理，虽未获得最终成功，但促进了某些数学分支的发展(主要是图论、拓扑学等)， 而机器证明四色定理结论是对的，又能怎样呢?只得到没有灵魂的空壳而已，因为四色定理本身的意义并不大。现在数学界普遍承认五色定理了，但世界上绝大多数 的地图颜色都超过5种。因为除了考虑颜色种类最少，现实生活中还有其他考虑。
一位反对机器证明的数学家说，数学的光荣，便在于它现有的一切证明方法，都是脉络绵密，层次分明，就像天衣无缝，出不了差错的。而使用计算机则有可能出现人无法检验出来的差错，而这差错可能是致命的。
现在已经实现的几何定理可用机器求解，所生成的解答其推理过程的简洁优美可以与人工解答媲美。虽然解决的只是一小类数学问题，远没有达到解决四色定理、哥德巴赫猜想一类难题的水平，但至少说明了机器证明和人工证明之间并没有不可逾越的鸿沟。人类的创造力再一次得到展现。
国外还出现了一些人机交互的计算机推理系统，如Coq、Otter、Roo等。借助这些系统，能够用来进行不同的数学领域的推理，所生成的证明类似于数学家的工作。
其实对于人类面临的很多难题，既然单个群体无法解决，那我们齐心协力一起解决不是很好么？数学家提供理论基础，计算机科学家设计算法并编程实现，而物理学家和工程师们则要保证计算机本身的稳定性。
我们相信，机器证明不但不会像有些数学家担心的那样“使数学走向衰败”，还将使数学家摆脱大量的繁琐的机械计算和推理，把节省下来的时间和精力用于更加富有创造性的工作中去。
1852年德·摩根写给哈密尔顿的信，信中首次提到四色猜想并做了初步探讨
nvod11111111
职业5分调戏家
给未尝老师的回答在哪儿？麻烦你给个链接。楼里面找
没有观点的网友是谁？是您自己吗？你这是想再次承认自己互博吗
俺承认，您没有用过“伟大”这个词儿来描述吴文俊，您只是说他是机器证明的奠基人。
机器证明这个学科有重要性吗？对你不重要其奠基性的内容，大学里会不教？这又是自搏的第一招吗？
您已经语无伦次，没有逻辑了。阅毕！
不谢。现在查文献的最好方法不是谷歌吗？现在正经搞科研工作的人离得开谷歌吗？难道靠百度吗？
告诉您吧，未尝老师引用Automated Theorem Proving, after 25 years在谷歌上查得到。第一篇文章回顾了自动定理证明这个领域里的发展，洋洋洒洒31页的文字里，对吴文俊的贡献，两三句话就带过去了。
nvod11111111
职业5分调戏家
这篇文章，你读了吗？
你确定你读懂了吗？
你确定你读懂了吗？
看一篇两位搞数学的人写的文章，张景中好像很有名，注意到了下面这一段，
我们知道吴的领域是几何定理机器证明，是机器证明里的一小块，说是机器证明的奠基人，就比较可笑了。
现在已经实现的几何定理可用机器求解，所生成的解答其推理过程的简洁优美可以与人工解答媲美。虽然解决的只是一小类数学问题，远没有达到解决四色定理、哥德巴赫猜想一类难题的水平，但至少说明了机器证明和人工证明之间并没有不可逾越的鸿沟。人类的创造力再一次得到展现。
----------------------
机器证明可靠吗
作者：彭翕成, 张景中
用机器证明的数学定理中，最为人津津乐道的当属四色定理。100多年以来，数学家们为证明这条定理绞尽脑 汁，所引进的概念与方法刺激了拓扑学与图论的发展，但一直没有得出证明。1976年,美国数学家阿佩尔与哈肯借助电子计算机,用了1200个小时，作了上 百亿次判断，终于完成了四色定理的证明，轰动全世界。美国邮局为此在一些明信片上加盖邮戳：“四色足够了！”
当一些数学家为一个高难度的定 理得到解决而庆祝时，更多的数学家却对计算机给出的证明表示质疑。质疑的理由有二。一是对于相当多的定理证明，特别是那些被称为“下金蛋”的数学问题，最 重要的意义不在于论证最终的真假，而是在求证过程中不断发现的新方法。二是计算机凭借高速计算能力作出的所谓证明,数学家无法人工检验,谁知道中间会不会 出错呢?
计算机得出的结果，有些是容易检验、容易相信的。例如，把某一个很大的整数分解为两个大于1的整数的乘积，这是破解一类密码的关键任务。大型高速计算机工作几个月才分解了一个整数，人只要几分钟就能检验结果是否正确。
类似地，计算机算出来的方程解是否正确也不难检验，但定理证明是另一回事。在例证法中，面对计算机用10万个例子证明了的一条几何定理，我们会有什么想法？与此类似，用代数方法经过成百上千项的多项式计算而证明的几何定理，我们会有什么想法？
我们可以相信某一条被计算机宣布成立的定理前提，认为计算机的硬件是可靠的，计算机的操作系统是可靠的，机器证明软件的程序是可靠的，程序依据的算法和理论是可靠的。
算 法和理论的可靠性，通过学习和讨论，不难确认。其他几种可靠性，可以经过大量实践验证。譬如让另外一批人，用另外的算法编程，用另外的机器运行，假如推导 出来的结论与之一致，那么可靠性得到了增强。因为一个定理，反映一个客观事实。这个事实不会因发现的人的不同而改变，同样也不会因为证明程序的不同而改 变。这样做，从哲学上看，是不是改变了数学真理的性质呢？
另一种方法，是计算机给出人工能够检验的证明。1976年，中国科学院的吴文俊院 士发表了检验几何命题的有效的机械化方法。吴法的成功激起了几何定理机器证明的研究热潮。到1992年，基于几何不变量的消点方法出现，实现了几何定理可 读证明在计算机上的自动生成。这一工作被国际同行誉为计算机处理几何问题的里程碑。
伴随着计算机技术的进步，直到1996年出现了基于前推模式的 “几何信息搜索系统”，成功地证明了上百个非平凡的几何命题，收到了良好的效果。
人们对机器证明的反对，多半集中于它的繁琐和不可检验。
在 计算机还没发明的时候，就有数学家提出机器证明（设计一种机器代替人推理）的设想，遭到了很多数学家的反对。数学大师庞加莱认为：“你可以将牲畜赶到机器 的前端，机器将其宰杀后储存成罐头输出。难道你可以把定理的条件送到机器的前端，机器自动输出结论吗？这实在是不可思议！”
在四色定理被机 器证明之后，反对声仍然强烈。有评论认为：“机器证明破坏了数学的优美。一个好的数学证明应当像一首诗—而这纯粹是一本电话簿！”普林斯顿大学数学教授约 翰·康威更是在接受《纽约时报》采访时说:“我不喜欢它们（计算机证明），因为你感觉不知道究竟发生了什么。你不能从中获得任何新的见地。”持这种观点的 数学家不是个别的，他们认为如果一个难题被一种新方法解决了，这是一件了不起的事情。但是如果解决的方案只是现存方法的反复使用，那只能证明解决者的聪明 而已。这不利于数学的发展。
还有人指出，传统数学研究四色定理，虽未获得最终成功，但促进了某些数学分支的发展(主要是图论、拓扑学等)， 而机器证明四色定理结论是对的，又能怎样呢?只得到没有灵魂的空壳而已，因为四色定理本身的意义并不大。现在数学界普遍承认五色定理了，但世界上绝大多数 的地图颜色都超过5种。因为除了考虑颜色种类最少，现实生活中还有其他考虑。
一位反对机器证明的数学家说，数学的光荣，便在于它现有的一切证明方法，都是脉络绵密，层次分明，就像天衣无缝，出不了差错的。而使用计算机则有可能出现人无法检验出来的差错，而这差错可能是致命的。
现在已经实现的几何定理可用机器求解，所生成的解答其推理过程的简洁优美可以与人工解答媲美。虽然解决的只是一小类数学问题，远没有达到解决四色定理、哥德巴赫猜想一类难题的水平，但至少说明了机器证明和人工证明之间并没有不可逾越的鸿沟。人类的创造力再一次得到展现。
国外还出现了一些人机交互的计算机推理系统，如Coq、Otter、Roo等。借助这些系统，能够用来进行不同的数学领域的推理，所生成的证明类似于数学家的工作。
其实对于人类面临的很多难题，既然单个群体无法解决，那我们齐心协力一起解决不是很好么？数学家提供理论基础，计算机科学家设计算法并编程实现，而物理学家和工程师们则要保证计算机本身的稳定性。
我们相信，机器证明不但不会像有些数学家担心的那样“使数学走向衰败”，还将使数学家摆脱大量的繁琐的机械计算和推理，把节省下来的时间和精力用于更加富有创造性的工作中去。
1852年德·摩根写给哈密尔顿的信，信中首次提到四色猜想并做了初步探讨
nvod11111111
职业5分调戏家
您的数据库咋就教会您虚张声势的咋呼啊？
呵呵，还是当年七一那一套，对了现在变成八一了。
nvod11111111
职业5分调戏家
你这是谷歌到的结论吗？您的数据库咋就教会您虚张声势的咋呼啊？
nvod11111111
职业5分调戏家
你想说啥，我看不明白？
不用。就看您在本楼的表演，就能得出结论啦。
nvod11111111
职业5分调戏家
你确定这结论对吗？不用。就看您在本楼的表演，就能得出结论啦。
坦白讲俺不能百分之百地确定哟。
不出国听到公知口中大象的腿，
出国旅游看到的是大象的身子，
国外定居就能摸到大象的尾巴。
出国旅游看到的是大象的身子，
国外定居就能摸到大象的尾巴。
看来先出国旅游后再出国定居的老师们对大象有比脚完整的鸟解了。当然没出国时，如果他们没听公知的话，也会吃一些亏。
看来先出国旅游后再出国定居的老师们对大象有比脚完整的鸟解了。当然没出国时，如果他们没听公知的话，也会吃一些亏。
从不回国，只看《大鸡元》的移民看到的是中国大象的jj
不经常回国的移民，看到的是中国大象的身体或者大腿，
天天待在中国，看到的是中国大象的尾巴。
这应当是10多年前的国内情况。
我98年在上海上大学的时候，学生宿舍是7人间，有8个床，但有一个床专门放7个人的行李箱之类的东西。那时候宿舍楼每层有两个公共洗衣房，没有热水，没有洗衣机和干衣机，只能手洗衣服。洗澡得去公共澡堂。 过了两年后，学校新修了学生宿舍楼，因赶上扩招，我们没有机会享受新宿舍，新生全部搬进了新宿舍，我记得那时候已经是4人间了。毕业工作后，遇到实习生，他们说他们的宿舍也是4人间，上床下桌，带有独立卫浴，有小阳台可供晾晒。
来加拿大之前，我记得上海某些高中的学生宿舍都配上单独的空调了。
国内的学生宿舍的配置情况应当说还是进步挺大的。
你的还不算便宜，我同事的车险一年960$。
但这样比较没有意义，首先你这个车险应当有很多条件才能拿到的
1，有一定的驾龄，起码4，5年要吧。我同事的驾龄在多伦多有16年。
2，车型安全性好。
3，没有事故记录。
加拿大的车险不一定是最贵的，但一般的车险确实是非常贵的，300多刀一个月都很常见，如果保的全面，甚至上500多刀。
注册或登录来发表评论
您必须是注册会员才可以发表评论
注册帐号
注册帐号. 太容易了!
登录
已有帐号? 在这里登录.
Similar threads
2024-07-05有新回复
全楼:0.02
Saint.Saens
