1700517417
1700517418
该系统允许任何人提交用这种形式语言编写的数学证明。因此，到2013年特里布里克去世时，Mizar已成为世界上最大的计算机数学证明数据库：其中一部分是将人类证明过程转化为计算机语言，另一部分则由计算机直接生成。该系统目前由波兰比亚威斯托克大学、加拿大阿尔伯塔大学、日本信州大学的研究小组负责开发和维护。近年来，人们对该系统的关注程度有所下降，数据库的发展不是很快。DeepMind和谷歌研究团队将其目标锁定在Mizar的数据库上，这一点超出了绝大多数人的预料。
1700517419
1700517420
经过数十年的积累，人们已经用形式语言这种计算机更容易理解的语言在Mizar的数据库中创建了5万多个定理。Mizar项目的参与人从中挑选出许多人类数学家们钟爱的定理，比如代数基本定理：复数域上的n次多项式有且仅有n个根。
1700517421
1700517422
这个定理非常具有代表意义，其证明可谓一波三折。从17世纪初到现在，人类对它的证明中曾出现过多次失误，其中不乏最伟大的数学家，诸如欧拉、高斯、拉普拉斯等人。直到1806年，让·罗伯特·阿甘（Jean Robert Argan）才提出第一个被公认为完整无误的证明。以往证明中的错误都藏得很深，没有足够的时间检验，是极不容易被发现的。倘若计算机能够发现人类证明中隐藏的错误，那么它在证明定理方面的正确性和有效性就会被刮目相看了。
1700517423
1700517424
计算机在Mizar数据库中生成证明的流程是这样的：首先，整理出数学、几何学的基本公理列表；其次，制定推理规则；最后，用一系列相互关联的推理规则构建出某一定理的证明过程。这与下围棋有异曲同工之处：一开始棋盘上空空如也，推理规则就相当于黑白棋手交替行棋所遵循的游戏规则，定理就相当于最终形成的某种特定的棋局。
1700517425
1700517426
DeepMind团队意识到，证明定理和下围棋在本质上是相互关联的：两者都是在可能的输出结果树中寻找特定的节点。而每个节点又具有不同分支，且到达某一特定终点（叶子节点）的分支长度有可能非常长。问题的关键就在于如何选择分支以获得最期待的输出结果：赢得一场比赛或证明一个定理。
1700517427
1700517428
利用计算机来生成数学定理已是司空见惯、不足为奇的事情了，甚至略微夸张一点说，计算机只要启动，就可以证明定理。但“条条大路通罗马”，一个定理的不同证明中往往会出现重叠。可这并不是研究人员们的兴趣点，他们真正要解决问题是，在被给定一个命题（特定的终点）时，计算机是否能够找到通往该终点的路径，即命题的证明。如果不能，那能说明这个命题是假命题吗？
1700517429
1700517430
通过对Mizar相关数据的研究，DeepMind和谷歌研究团队发现其约有56%的定理证明没有人类参与的痕迹。他们将目标锁定在创建一个新的定理证明算法以提高这一比例：用计算机成功生成的证明来训练该机器学习算法，通过对Mizar数据库中已有数据的学习获得探索证明树的好方法。温雅尔斯拿着手中的研究论文无比自豪地对我说，他们的算法已将Mizar数据库中机器证明的比例提高到了59%。这个看似微不足道的“一小步”，代表的却是新技术应用的“一大步”。它不仅仅是多证明一个定理或者多赢一场比赛，而是计算机可以完成的证明量增加了3%。
1700517431
1700517432
在某种程度上，我可以理解温雅尔斯的激动之情。这就像学习演奏爵士乐的算法，决定它前景的是一个合乎音乐继续发展的逻辑，而不是接下来到底演奏哪个音。该算法在很大程度上扩展了计算机的应用范围，打开了计算机产生定理的新篇章。
1700517433
1700517434
然而，离开DeepMind时我的心情有些失落，因为此行并没有得到预想的收获。我本该为数学能取得如此巨大的进步而高兴，但实际上，机器只是盲目地生成了一些粗制滥造的“数学音乐”，而不是我所期望的“天籁之音”。没有人评判这些新发现的价值，也没有人对其中是否有令人惊讶的启示而感兴趣——它们只是新的而已。
1700517435
1700517436
1700517437
1700517438
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
[
上一页 ]
[ :1.700517417e+09 ]
[
下一页 ]