打字猴:1.700516772e+09
1700516772 天才与算法:人脑与AI的数学思维 [:1700514914]
1700516773 天才与算法:人脑与AI的数学思维 Coq证明助手
1700516774
1700516775 在过去,数学问题的证明和验证过程全凭人工完成。而现在,越来越多的证明开始借力于计算机,但因为验证的过程既烦冗又复杂,并且工作量巨大,人类大脑的局限性决定了无法采用人工验证的方式判断其对错。因此,我们迫切需要一种解决方案,即通过构建新的程序来验证计算机证明的正确性。
1700516776
1700516777 20世纪80年代末,法国数学家皮埃尔·于埃(Pierre Huet)和蒂埃里·科昆德(Thierry Coquand)开始从事结构微积分(calculus of constructions)项目。该项目简称CoC,但很快又被称为Coq(法语里意为“公鸡”)。这个改动一方面是为方便记忆,因为在法国一直有以动物命名开发工具的习惯;另一方面是因为Coq是其开发者之一科昆德姓氏的前三个字母。Coq为验证数学证明而生,很快也成了验证计算机证明的重要程序,备受青睐。
1700516778
1700516779 2000年,微软研究院首席研究员乔治·贡蒂尔(Georges Gonthier)及其同事使用Coq对阿佩尔与哈肯的四色定理的计算机证明进行了验证,因为这是史上第一个需要计算机才能完成的证明(假定Coq不存在任何缺陷)。然后,他们也使用Coq去验证了阿佩尔和哈肯自己所写的证明部分。
1700516780
1700516781 人类手工证明与计算机证明不同,手工证明过程中会跳过一些烦琐或众人皆知的步骤,而计算机却依赖于明确、细化的步骤才能正确执行指令。这类似于写小说和写保姆指导手册的区别。前者不需要对主人公的每一个动作都解释得一清二楚,而后者则需要尽可能地明确和详尽,包括一天中婴儿的食谱,以及吃饭、睡觉、上厕所的每一个细节。
1700516782
1700516783 计算机用了5年的时间进一步自动识别并验证人类证明的过程。这期间,人们惊讶地发现了在第一次证明中被忽略的数学知识。
1700516784
1700516785 Coq与原始的计算机证明相比,更应该信任谁呢?当然是前者。越来越多的计算机证明被Coq所验证,使我们更加确信Coq是可靠的。这就像我们通过归纳法验证数学中的基本公理一样。这就像任取两个数A和B,如果A+B都等于B+A,那么A+B=B+A就是正确的。用一个计算机程序来验证多个计算机证明,比编制一个特定的证明程序或者进行人工证明更值得我们信任。
1700516786
1700516787 贡蒂尔团队验证完四色定理后,紧接着开始了对奇阶定理(odd order theorem)的验证工作。奇阶定理是对称性研究最重要的指导定理之一,通常被认为是有限单群分类的基石。像化学里的元素周期表一样,有限单群是构成数学有限群论“元素周期表”中的基本元素,所有的对象都由有限单群构成。具有素数边的正多边形(如正三角形、正五边形)是该周期表中的元素。此外,该周期表中还有一些复杂且独特的对称元素,如旋转了60次的正二十面体、需要196 883维线性空间才能表达的“魔群”等。“魔群”具有的元素个数超过了构成地球的原子个数。
1700516788
1700516789 该定理指出,任何奇阶对称结构的基本组成单元都是素数多边形,此外再无其他结构。如果把对称物体分为奇阶和偶阶两种,那么该定理就等于涵盖了其中的一半,意义重大。
1700516790
1700516791 奇阶定理的原始论文有255页,占据了《太平洋数学期刊》的全部篇幅。在它出版之前,大多数证明最多只有几页,一天内即可掌握。这个冗长复杂的证明,对每一位数学家来说都是一个挑战。因此,其中是否存在细微的缺陷或错误,始终无法考证。
1700516792
1700516793 Coq对复杂数学定理的证明过程,一方面可以检验Coq的能力,另一方面能帮我们树立足够的信心。但将人工证明转换成可验证的计算机代码这一过程并不容易。
1700516794
1700516795 贡蒂尔略带腼腆地回忆道:
1700516796
1700516797 第一次开会讨论时,我向团队里其他成员宣布了我的宏伟计划,他们流露出不可思议的表情,就像是我得了妄想症。奇阶定理的证明过程太过复杂,验证它最初被认为是不可能的。做这个项目的真正原因,是为了充分理解数学理论的构建过程并使之与Coq充分融合。
1700516798
1700516799 会议结束后,团队里的一名程序员查看了原始证明,随后向贡蒂尔发来一封邮件:“17万行代码,1.5万个变量,4300个函数。好玩,太棒了!”微软剑桥研究院团队用了6年的时间完成了证明。当项目即将结束时,贡蒂尔兴奋地说,经过无数个不眠之夜,他终于可以放松一下了。
1700516800
1700516801 贡蒂尔说:“数学是最伟大的浪漫主义学科之一,即便是天才,也得掌握所有知识才能激发灵感,理解一切。”但是,人类的大脑存在物理上的局限性。他希望他们所做的一切能够叩开人类与机器彼此信任、持续合作的新时代“大门”。
1700516802
1700516803
1700516804
1700516805
1700516806 天才与算法:人脑与AI的数学思维 [:1700514915]
1700516807 天才与算法:人脑与AI的数学思维 人脑的极限
1700516808
1700516809 年轻的数学家们开始意识到,数学研究变得更为艰难了:学科分支越发密集,问题越发复杂。攻读博士学位的3年时间,只够去理解导师所给题目的含义。随后,再花费数年时间去研究、探索,运气不错的话,会得到一些研究成果。然而,你发表的论文却面临着没人能审核它。
1700516810
1700516811 审核别人发表的论文是得不到太多报酬的,但期刊论文的审核必须经过同行的评审。职称评定也以公开发表在《数学年鉴》或《l’IHES数学期刊》这类文献中的论文积分为基准。因此,有一个像Coq证明助手这样的系统就非常重要了。
1700516812
1700516813 一些数学家认为我们目前正处在一个新旧时代的交替期——数学的发展虽然受到人类大脑局限性的制约,但借助于计算机,我们对数学的探索已远远超出了人脑的思维范畴。
1700516814
1700516815 伟大的数学家们能够用他们睿智的头脑,借助于纸和笔这些极其简单的工具,构造出像“魔群”这样具有196 883维的对称体,这是人类的奇迹。但数学家们终将会老去,就像中世纪的泥瓦匠,其精湛的技艺将伴随身体的死亡而从人世间消失。如果很难找到通往“新奇迹”的方向,人们终将失去创造的原动力。
1700516816
1700516817 费马大定理的证明长达数百页,跨越3个世纪,这说明人类拥有足够的耐心。当你努力去证明一个极其复杂的猜想时,隐约会有一种突破人类大脑物理极限的感觉。数学是无限的,而人的能力是有限的。但即便如此,我们常会为自己所做的努力感到吃惊,因为我们用数学的方式证明了“数学海洋的广阔无边”。
1700516818
1700516819 有一个问题几乎困扰了我15年之久。每次推演时,总是在即将得到解决方案的关键时刻,我的大脑容量就不够用了,它给我“即将宕机!”的警告。距离成功仅一步之遥,却难以取得突破。就像现象与本质之间隔着一张“渔网”,它制约着我们,让我们难以冲出迷雾,得到光明。当几代数学家致力于黎曼假设的证明而不得其解时,人们开始怀疑,是否这样的证明已超越人脑的极限。
1700516820
1700516821 著名数学家哈代多年来一直试图证明黎曼假设,后来他自嘲道:“每个傻瓜都能提出有关质数的问题,而最聪明的人却无法解答。”奥地利数学家、逻辑学家库尔特·哥德尔(Kurt Gödel)有过论证:数学中包含了许多没有经过证明的真理。能否用新的公理去证明那些未被证明的真理呢?哥德尔早在1951年就发出了警示,他认为我们可能会越来越难以掌控现代数学的发展方向:
[ 上一页 ]  [ :1.700516772e+09 ]  [ 下一页 ]