@ 2014.08.15 , 00:13
44

计算机成功验证了400年前数学难题的解法

[-]

早在1611年的时候,约翰尼斯·开普勒就建议人们在堆放球形物体时——比如商店中待售的橙子,采用金字塔型堆放法是效率最高的。不幸的是他本人并不能证明这点,不过最近计算机终于验证了这条猜想的正确性,结束了这场跨越5个世纪,长达400多年的争论。

其实,早在1998年匹兹堡大学的Thomas Hales就想出了证明方法,只是Hales的论述太长——12名评审耗时4年时间对这份300页的文档进行查错,只能99%肯定方法的正确性。所以,不甘心的Hales在2003年又开始了“污点项目”——一套能够验证他的证明法的计算机工具。

污点使用了两个形式验证软件——名字还很好听,一个叫“Isabelle”一个叫“HOL Light”——两个软件都是通过判断短小且容易验证的一系列逻辑表述来进行验证。凭借这种技术,软件可以检验所有逻辑表述的正确性,只要时间充足,验证数学证明过程也是可以的。

上周日的时候,Hales和团队宣布这份300页的证明方法已经接受并通过了两套软件的联合详细验证,最后结果显示他的验证方法完全正确,这也让Hales感到欣慰。

也就是说,计算机成功验证了400年前开普勒所提出的方法的正确性。“我一下子觉得年轻了十岁。”Hales 兴奋地说。

计算机可以成功验证数学证明过程不仅仅对于Hales来说是好消息,要知道每年全世界会诞生数百份内容多到可怕的数学证明过程,通过这项工程,Hales证明了验证逻辑不再需要人脑进行,计算机就可以完成这个工作。数学家终于能够放手去进行创造性思考——至于烦人的验证过程,交给计算机就可以了。

本文译自 Gizmodo,由译者 王大发财 基于创作共用协议(BY-NC)发布。


给这篇稿打赏,让译者更有动力
支付宝打赏 [x]
您的大名: 打赏金额:

0.0
赞一个 (0)

TOTAL COMMENTS: 44+1

  1. 木头先生
    @3 years ago
    2511002

    能活着验证自己想法的数学家好幸福。。

    [278] XX [3] 回复 [0]
  2. Infire
    @3 years ago
    2511005

    离机器人统治地球又近了一步。

    [18] XX [13] 回复 [0]
  3. 2511006

    这套机械证明算法 似乎之前天朝数学家也耍过?

    [16] XX [4] 回复 [0]
  4. 大大
    @3 years ago
    2511014

    完了完了,感觉自己智商不够用了。我读过书,你们不要糊弄我。

  5. 2511019

    下一个问题。。如何证明计算机是对的

    [77] XX [34] 回复 [0]
  6. Jancy君
    @3 years ago
    2511021

    以后高考数学最后一道题能解?

    [36] XX [6] 回复 [0]
  7. 邦尼
    @3 years ago
    2511035

    以后买水果的时候告诉老板橙子要用金字塔型堆放

    [12] XX [0] 回复 [0]
  8. yumushen
    @3 years ago
    2511040

    比较好奇除了金字塔堆法还有哪些堆法。。。。

    [95] XX [4] 回复 [0]
  9. 中学生二年级
    @3 years ago
    2511044

    总之是42

  10. 2511050

    @zinc: 你该吃药了

    [10] XX [3] 回复 [0]
  11. 不染
    @3 years ago
    2511067

    几乎在煎蛋看到的文章 都会在网易新闻里看到 网易搬过去的?

    [28] XX [0] 回复 [0]
  12. 想不到昵称
    @3 years ago
    2511068

    哟 之前看到巴基斯坦的水果摊几乎都是这样放 以为只是美观 原来还伴随 如此艰深的数学难题 高考数学55的幸好没去思考这个问题

  13. 金三胖思密达
    @3 years ago
    2511073

    关键是要把橘子一个一个摆成整齐的金字塔也太无聊了吧,,,,,,,,,顾客一拿还全乱了

  14. 职业学生党
    @3 years ago
    2511076

    不好放还费时间

  15. 客卿
    @3 years ago
    2511078

    以后对别人说文化水平,都不敢说懂啥,只敢说了解了一点。。。

  16. 2511093

    关键橙子还要一样大

  17. 2511103

    橙子怎么个金字塔摆法。。。。

  18. 首先
    @3 years ago
    2511106

    我并没有为过数学争论过

  19. 2511107

    @不染: 写了出处了

  20. 天や罚
    @3 years ago
    2511109

    一拳超人啊

  21. 2511112

    不晓得,因为晶体中的原子最大密排也是金字塔形的啊。。

  22. 2511115

    他证明了自己证明400年前数学难题的证明是正确的。

    [13] XX [0] 回复 [0]
  23. blu10ph
    @3 years ago
    2511117

    拿走下面的一个会不会崩溃一层?~

  24. Naproxen
    @3 years ago
    2511127

    “老板,你知道吗,橘子用金字塔型摆放最有效率哦。这是17世纪的约翰…”“少废话你买不买,不买不要捏我的橘子”

    [80] XX [2] 回复 [0]
  25. 杍墨
    @3 years ago
    2511134

    “效率最高”到底是什么意思??????

  26. 池塘王子
    @3 years ago
    2511144

    “效率”最高是指什么效率?不理解啊

  27. dredow
    @3 years ago
    2511157

    人脑真可怕,四百年才能验证的东西,可以用直觉搞定。这是一种什么天赋?

  28. 道离
    @3 years ago
    2511166

    是指限定底面积摆放最多个数?

  29. 煎蛋
    @3 years ago
    2511216

    “效率最高”的效率是指空间使用效率。

  30. 大麻夹
    @3 years ago
    2511217

    金字塔的话底面应该是正方形吧
    直觉告诉我六边形效率最高呀……

  31. 煎蛋
    @3 years ago
    2511250

    @大麻夹: 金字塔式的堆放是指这样的堆放:底层三个橙子组成一个等边三角形,然后在这三个橙子的中间放第二层的橙子。还有其他的堆放方式,比如说体心立方结构,就是每个橙子在立方体的八个顶点上。

    这篇文章的意思就是说,现在已经证明金字塔式的堆放是所有堆放方式中空间使用效率最高的。

  32. brahmagupta
    @3 years ago
    2511264

    20种布拉伐格子。化学家和物理学家轻蔑的骂了一句:"sb"

  33. brahmagupta
    @3 years ago
    2511266

    14种。。

  34. 阿卡
    @3 years ago
    2511321

    @Naproxen:
    “老板,不是,您先别着急…您听我说,就稍微等一等,听我说,您看您这里这里,在这边边地方有个橘子是不是违反了金字塔原则?这个橘子是不是搭在了?您算算,总共减少了多少效率?本来您可以多搭多少橘子?多搭了橘子是不是就更吸引客人?多吸引客人是不是能够能让他们多买橘子?多买橘子是不是量就不够了?老板您仔细看看,还有这里这里。仔细看着这些橘子,好好算一下。您看看,那我免费帮你拿走这些破坏您效率的橘子,是不是您就挽回了您的效率?是不是您就能更容易地卖出橘子?效率就是摆放数目除以空间,空间可是您租的地方则是您的成本,橘子则是代表着您的利润。可不是小事。您得好好算一下。对了,为什么那个橘子会在那里呢?您这么聪明,摆橘子的时候一定不会违反金字塔原则。那是谁乱放的呢?那个放的人肯定不怀好意想坑您的效率,啊,我猜到了,是您的竞争对手吗?您看对面卖苹果的阿婆一脸鬼祟的样子,是吧?是不是有问题吧。仔细思考一下。诶等等,我接个电话….约翰啊,什么?!你等着!我马上来,五分钟!!!老板您就在这里好好思考一下,我急事先走了。”

    [15] XX [0] 回复 [0]
  35. 阿卡
    @3 years ago
    2511334

    @FFF: NLP………

  36. 阿卡
    @3 years ago
    2511350

    @FFF: 譬如这个例子,关于NLP的对象。如果语言不同,就说他的第二语言。譬如他会中文和英文,英文是他第二语言,你就用英文说。如果他只会一种语言如中文,就故意用口音很重的中文说话。这是让他接受你信息的时候,花更多时间在解读你的信息上,在他解读的时候,再轰炸他更多的信息并暗示你的意愿。不让他有回复的时间,把握节奏,每次再他想脱离你的思路的时候,强制他沿着你的思路思考和接受信息。直至最后让对方的精神进入被动接受信息的学习状态。这过程中语速要快,不断轰炸信息,在他进入思考的失神状态时重复暗示你的意愿,要用重音和指示性肢体语言,直至他完全进入被动学习状态之后,强调你想让他做的事情,意志不强的人就会很被动地让你直接让你做,一般人起码过上十几分钟才能反应过来。
    这种技巧用于小额推销、街头讲价和逃罚单。

  37. 小柴人
    @3 years ago
    2511416

    我不懂效率最高是什么意思

  38. 乱毛
    @3 years ago
    2511465

    老板,我要从底下数第三层,右边第五行,第6列的那只橙子。
    对对,就是那只。

  39. AaronXu
    @3 years ago
    2511529

    @yumushen: 8个放成立方体那样,但会比8个按照金字塔摆法那样废地方

  40. jiangtonyy
    @3 years ago
    2511677

    @Jancy君: 很可能不能解。。因为很多题都出错的,像它这么分析,很可能会出问题。

  41. 老肖
    @3 years ago
    2511815

    那我怎么挑橘子?

  42. 秦川梦_
    @3 years ago
    2512096

    @阿卡: 药不能停

  43. 2512406

    @小柴人: 就是占用空间的效率最高

发表评论


24H最赞