Solidot | 数学证明因为太长而无法被人类验证

数学证明因为太长而无法被人类验证

科学 数学
WinterIsComing (31822)发表于 2014年02月19日 18时13分 星期三 新浪微博分享 腾讯分享 豆瓣分享 人人分享 网易分享
来自AI数学家部门
如果人类无法检验一个定理的证明,这个证明还能被当成数学吗?这是计算机辅助证明的流行而引发的一个疑问。利物浦大学的 Alexei Lisitsa和同事Boris Konev使用计算机生成了一个13GB大小的证明,这可能是有史以来最长的证明了,它的大小使得人类不可能去检查证明是否无误。他们的证明与匈牙利犹太数学家Paul Erdős在1930年代提出的一个猜想有关。Erdős提出,一个只含有+1s和-1s的随机无穷序列(例如对于序列(x1, x2, x3, ...),其中xi = (−1)i+1)是否包含内在模式, 一种测量方法是将无穷序列在特定点切割,创造出了一个有限的子序列。Erdős的猜想是:对于任意整数C,存在整数K和d,使得。Lisitsa和Konev用计算机证明,一个无穷序列总有一个大于2的差。论文预印本发表在arXiv.org上。

回复

数学证明因为太长而无法被人类验证 | 6条评论
显示选项 阈值选择:    样式:
声明: 下面的评论属于其发表者所有,不代表本站的观点和立场,我们不负责他们说什么。
  • Leap of Faith(得分:1 )

    biergaizi(30884) Neutral 发表于2014年02月19日 18时40分 星期三
    这个程序从本质上来说是一个信仰问题,即哲学上说的 Leap of Faith,是跨越本质界和现象界的鸿沟的唯一途径。比如,你可以去一行一行审查这个证明程序的代码,但你无法审查 libc、外部程序库、操作系统内核、编译器、内存、CPU。我们只能被迫相信它们,完成信仰的飞跃。克尔凯郭尔会怀疑 GCC 吗?
    [ 回复本条 ]
    • re:Leap of Faith 匿名用户 (得分:0) 2014年02月19日 20时41分 星期三

      • re:Leap of Faith 匿名用户 (得分:0) 2014年02月19日 23时57分 星期三

    • 机器证明本来就和编译器理论相关 匿名用户 (得分:0) 2014年02月20日 00时47分 星期四

    • 没有人验证证明 匿名用户 (得分:0) 2014年02月20日 06时39分 星期四

  • Ising模型 匿名用户 (得分:0) 2014年02月20日 03时12分 星期四

随意打赏

提交建议
微信扫一扫,分享给好友吧。