1700517433
1700517434
然而，离开DeepMind时我的心情有些失落，因为此行并没有得到预想的收获。我本该为数学能取得如此巨大的进步而高兴，但实际上，机器只是盲目地生成了一些粗制滥造的“数学音乐”，而不是我所期望的“天籁之音”。没有人评判这些新发现的价值，也没有人对其中是否有令人惊讶的启示而感兴趣——它们只是新的而已。
1700517435
1700517436
1700517437
1700517438
1700517439
天才与算法：人脑与AI的数学思维 [:1700514930]
1700517440
天才与算法：人脑与AI的数学思维 数学图灵测试
1700517441
1700517442
这就是真正的未来吗？我从Mizar的数据库中精心挑选了一部分定理的证明，想要更深入地了解一下。为了能通过一个真命题推导出另一个命题，证明用计算机形式语言描述。但我却发现自己几乎无法驾驭这种晦涩难懂的形式语言，我体会到了大多数人打开我的论文看到一堆看起来毫无意义的符号时的那种感受。这不是人类表达和交流数学思想的方式。例如，关于“素数有无穷多个”[1] 这一定理，Mizar的证明过程如下：
1700517443
1700517444
reserve n,p for Nat;theorem Euclid: ex p st p is prime & p > n proof set k = n! + 1;n! > 0 by NEWTON:23;then n! >= 0 + 1 by NAT1:38; then k >= 1 + 1 by REAL1:55; then consider p such thatA1: p is prime & p divides k by INT2:48; A2: p <> 0 & p > 1 by A1,INT2:def 5; take p;thus p is prime by A1; assume p <= n;then p divides n! by A2,NATLAT:16; then p divides 1 by A1,NAT1:57; hence contradiction by A2,NAT1:54;end;theorem p: p is prime is infinite from Unbounded(Euclid);
1700517445
1700517446
即便是我这样的数学家、专门人士也觉得一头雾水！这不符合人类的叙事方式，甚至可以夸张一点说是语言障碍。
1700517447
1700517448
既然通过算法可将西班牙语翻译成英语，那么能不能将这种计算机证明语言翻译成易于与人交流的方式呢？剑桥大学的两位数学家蒂莫西·高尔斯（Timothy Gowers）和莫汉·加内萨林加姆（Mohan Ganesalingam）开展了此项研究。1998年，高尔斯成为菲尔茨奖获得者并登上新闻头条，同年被聘为劳斯·鲍尔（Rouse Ball）讲席教授。
1700517449
1700517450
另一位数学家加内萨林加姆的经历也极富传奇色彩。起初，他按部就班地在剑桥大学三一学院学习数学，以第一名的成绩拿到剑桥大学的数学专业学位，并获得资深兰格勒头衔（Senior Wrangler），这是剑桥数学学子的最高荣誉。后来，加内萨林加姆改行学英语，又以剑桥大学英语学院最佳成绩毕业，获得了盎格鲁–撒克逊英语（Anglo-Saxon English）硕士学位，令所有人大吃一惊。紧接着，他继续攻读计算机科学博士学位，从形式语言学角度对数学语言进行分析。他的数学和语言学的背景很快就派上了用场——高尔斯和加内萨林加姆在三一学院相遇，并惊奇地发现他们对揭开计算机语言难以理解的奥秘有共同的爱好。他们决定一起组建团队，创建一个能够生成人类直接能读得懂的计算机证明。
1700517451
1700517452
为测试算法，他们在高尔斯的博客上发布了一个调查问卷。该问卷挑选了本科一年级《度量空间》课程里面的5个定理，每个定理包括3个不同的证明，分别由博士生、本科生和计算机算法完成。为了保证调查的真实性和有效性，博客读者事先未被告知任何关于证明的来源信息。高尔斯仅仅要求他们根据自己的判断为这15个证明的优劣打分，其目的是想了解在没有任何提示的情况下，是否有人会怀疑这些证明不全是由人类完成的。紧接着，他们在第二篇博客文章里向读者透露了每个定理对应的3个证明中有一个是由计算机算法生成的，请读者投票加以辨别。
1700517453
1700517454
通过对投票结果的统计分析，大约有50%的读者识别出了由计算机算法生成的证明，但其中只有半数人确信自己的判断是正确的。此外，那些确信不是计算机证明而实际是计算机证明的投票占比也不容忽视。那些来自本科生的证明往往被误认为是计算机的证明。
1700517455
1700517456
那么，高尔斯这位菲尔兹奖的获得者是如何看待人工智能“入侵”数学领域对他构成的威胁呢？高尔斯在他的博客中这样写道：
1700517457
1700517458
在计算机最终取代人类工作这一历史发展进程中我看不到任何实质性的障碍，这可能会让人感到难过。但实现这一目标的过程却让人憧憬和兴奋。计算机在处理证明中那些烦冗、琐碎环节时的能力越来越强，人机互动越来越少，这留给我们更多的时间和精力去自由地思考更“有趣”的环节。
1700517459
1700517460
在Mizar项目中，除了语言问题之外，DeepMind和谷歌研究团队费了九牛二虎之力提高的3%中，有没有出乎意外的“惊喜”呢？我觉得整个项目似乎并没有抓住研究重点。我为什么这样说？
1700517461
1700517462
[1] “素数有无穷多个”定理的证明之一：假设素数只有有限的n个，其中最大的素数是p。设q为所有素数之积加上1，即q=（2×3×5×…×p）+1，则q不为素数。那么，q就可以被2、3、…p中的某一个数整除。而根据公式，q被2、3、…p中任意一个数整除后又会余1，与前结论相互矛盾。所以，由此可证明，素数个数是无限的。——译者注
1700517463
1700517464
1700517465
1700517466
1700517467
天才与算法：人脑与AI的数学思维 [:1700514931]
1700517468
天才与算法：人脑与AI的数学思维 巴别数学图书馆
1700517469
1700517470
我最喜爱的短篇小说之一，阿根廷作家豪尔赫·路易斯·博尔赫斯（Jorge Luis Borges）创作的《巴别图书馆》可以解释上述的问题。该小说讲述的是一名图书管理员“探索”自己图书馆的故事。小说开头他这样描述自己的工作场所：“宇宙（别人管它叫图书馆）由许多六角形的回廊组成，其数目不能确定，也许是无限的……任何一个六角形回廊的上层和下层看起来都是永无止境的。”除图书馆之外，这里别无他物。它是我们自己的图书馆（我们称之为宇宙）的隐喻。这个像巨大蜂巢一样的图书馆里堆满了大小一致的书籍：每本书有410页，每页有40行，每行由80个书写符号（书写符号共25种，包括空格、句号、逗号以及22个字母）组成。
1700517471
1700517472
当图书管理员翻看这些书籍时，他发现除了偶尔地会看到一些有趣的文字之外，几乎所有书籍的内容都是无序、混乱的：有一本书从头至尾全部都在重复MCV三个字母；另一本书则纯粹是完全看不懂的“字母迷宫”，唯有倒数第二页上出现一行字——“啊！时间，你的金字塔！”
1700517473
1700517474
图书管理员给自己设定的目标是确定图书馆是否真的是无限大，如果不是，那么它到底是什么形状？随着故事的发展，一个假设被提出：“这个图书馆是‘完全的’……图书馆的书架上收藏着由25个书写符号构成的全部可能的组合（其数目尽管很大，但却是有限的）。换言之，就是能够用所有的语言表达出来的一切。”这个图书馆收藏着有可能被写出来的每一本书籍：托尔斯泰的《战争与和平》随处可见；达尔文的《物种起源》、托尔金的《指环王》，以及这些作品所有语言的译本；甚至本书也被放置在图书馆某个角落的书架上。（到目前为止，我的这本书才写了这么多，我多么希望能够找到它，这样就省得自己苦思冥想剩下的部分了！）
1700517475
1700517476
由于所有书的页数、行数、每行的字数这些指标都是固定的，我们可以估算出图书馆的藏书总数。已知构成书籍内容的书写符号共有25种，那么第一页第一行第一个字符就有25种选择，第二个字符也有25种选择，所以前两个字符总共可构成25×25=252 种选择。依此类推，每行有80个字符，就有2580 种可能的组合方式。
1700517477
1700517478
我们把问题进一步扩展，计算一下第一页可能有多少种不同的组合方式。因为每页有40行，所以就有（2580 ）40 =2580×40 种可能的组合方式。每本书有410页，进而可得（2580×40 ）410 =2580×40×410 种可能的组合方式，这就意味着图书馆的藏书总数达到了2540×80×410 本。这个数目非常巨大。给定宇宙可观测范围内的原子总数为1080 ，那么用一个原子代表一本书，即使把所有的原子都用光，也远远达不到巴别图书馆里的藏书总数。但即便如此，它依然是一个有限的数字。根据这个原理，我们可以很容易地编写出程序，让计算机在有限的时间内系统地生成所有书籍。当然，宇宙逐渐衰变成永恒的、冰冷的黑暗要经过多长的时间尚未得知，这里仅仅是从理论上加以讨论。
1700517479
1700517480
当人们听说图书馆收集了所有能被写出来的书籍时，首先得到的是一种奇特的幸福感，但随之而来的是巨大的失望，因为人们意识到这个似乎包罗万象的图书馆里实际上什么都没有。托尔斯泰、达尔文、托尔金甚至我的书在出版以后会被牛津大学图书馆收藏，是因为它们被人（许多人）认为是文学世界的瑰宝，它们值得在那里被收藏。这也是巴别图书馆与牛津大学图书馆最大的不同之处。
1700517481
1700517482
