1. 深度数学

1.1. 组合与选择，是发明新事物的两个不可或缺的条件

1.1.1. 保尔·瓦雷里（Paul Valéry）

1.2. 利用以往的数学定理证明过程训练算法，以发现新的定理

1.3. 谷歌设在伦敦的总部整体有一种现代牛津大学的感觉，提供了有助于员工们集中注意力、进行深度思考的最佳设施及环境

1.3.1. 24小时免费食物供应，配有专门的咖啡师随时为激活员工大脑活力而服务

1.3.2. 90米长的跑道，提供免费按摩服务

1.3.3. 可以上厨师丹·巴滕（Dan Batten，曾与英国厨神杰米·奥利弗共事）的烹饪课

1.3.4. 当大脑处于超负荷时，员工还能去遍布于大楼各处的“睡眠仓”里美美地睡上一觉

1.3.5. 员工在工作间歇可以尽情娱乐放松，如果愿意的话还可以在那里编写代码

1.3.6. 随性自然不仅指着装，更主要是人与人之间可以坦诚相见、畅所欲言

1.3.7. 所有的会议室都是以阿达·洛夫莱斯等科学先驱的名字命名的

1.4. 不会休息，就不会工作

1.4.1. 谷歌办公场所的“豪华”正是机器学习蓬勃发展的明显象征

1.4.2. 机器学习正用于帮助人们探索量子物理这个难以捉摸的随机世界，同时，其也通过各种各样的项目逐渐渗透到生物学和化学领域

2. 巴别数学图书馆

2.1. 阿根廷作家豪尔赫·路易斯·博尔赫斯（Jorge Luis Borges）创作的《巴别图书馆》

2.2. 这个图书馆收藏着有可能被写出来的每一本书籍

2.2.1. 托尔斯泰的《战争与和平》随处可见

2.2.2. 达尔文的《物种起源》

2.2.3. 托尔金的《指环王》

2.2.4. 这些作品所有语言的译本

2.2.5. 本书也被放置在图书馆某个角落的书架上

2.2.6. 托尔斯泰、达尔文、托尔金甚至本书在出版以后会被牛津大学图书馆收藏，是因为它们被人（许多人）认为是文学世界的瑰宝，它们值得在那里被收藏

2.3. 因为每页有40行，所以就有（25^80）40=25(80×40)种可能的组合方式。每本书有410页，进而可得（25^(80×40)）410=25^{(80×40×410)种可能的组合方式，这就意味着图书馆的藏书总数达到了25}(40×80×410)本

2.3.1. 给定宇宙可观测范围内的原子总数为10^80，那么用一个原子代表一本书，即使把所有的原子都用光，也远远达不到巴别图书馆里的藏书总数

2.4. 人们意识到这个似乎包罗万象的图书馆里实际上什么都没有

2.4.1. 它是我们自己的图书馆（我们称之为宇宙）的隐喻

2.5. 数学不仅仅是由一组我们所能发现的关于数字的真命题构成的

2.5.1. 这可能会让大多数非数学专业人士感到震惊

2.5.2. 证明定理的过程就是在叙述故事和塑造角色

2.5.3. 他们判断和选择故事是基于对故事情节产生的情绪反应

2.6. 创造，意味着不制造无用的组合，而仅制造那些少量且有用的

2.6.1. 不是人人都能创造出像贝多芬的《大调赋格》（Grosse Fuge）或者艾略特的《荒原》（The Waste Land）那样的伟大作品

2.6.2. 创造即甄别，即选择

2.6.2.1. 数学是被创造的，归根结底是鉴别和选择

2.6.2.2. 数学是一门关于鉴别和选择的学问

2.6.2.2.1. 庞加莱

2.7. 数学不仅是一门有用的科学，而更像是一门创造性的艺术

2.7.1. 定理证明的叙述，是决定这个定理能否在数学的万神殿中占据一席之地的重要因素

2.7.2. 一个好的证明就像一个动人的故事，抑或是一首美妙的乐曲，可以启发或引导“听众”踏上转变之旅

3. Mizar的数学

3.1. 一个20世纪70年代在波兰启动的名为Mizar的项目

3.1.1. 波兰数学家安杰伊·特里布里克（Andrzej Trybulec）率先启动了该项目的研究

3.1.2. Mizar的名字源于大熊座中的一颗恒星——开阳星

3.1.2.1. 这个名字是由特里布里克的妻子取的

3.1.3. 该项目旨在构建用一种容易被计算机理解和检验的形式语言描述的数学证明数据库系统

3.1.4. 该系统目前由波兰比亚威斯托克大学、加拿大阿尔伯塔大学、日本信州大学的研究小组负责开发和维护

3.1.5. 近年来，人们对该系统的关注程度有所下降，数据库的发展不是很快

3.1.5.1. DeepMind和谷歌研究团队将其目标锁定在Mizar的数据库上，这一点超出了绝大多数人的预料

3.2. 到2013年特里布里克去世时，Mizar已成为世界上最大的计算机数学证明数据库

3.2.1. 一部分是将人类证明过程转化为计算机语言

3.2.2. 另一部分则由计算机直接生成

3.2.3. 经过数十年的积累，人们已经用形式语言这种计算机更容易理解的语言在Mizar的数据库中创建了5万多个定理

3.2.3.1. 比如代数基本定理：复数域上的n次多项式有且仅有n个根

3.3. 利用计算机来生成数学定理已是司空见惯、不足为奇的事情了，甚至略微夸张一点说，计算机只要启动，就可以证明定理

3.3.1. 一个定理的不同证明中往往会出现重叠

3.3.2. 真正要解决问题是，在被给定一个命题（特定的终点）时，计算机是否能够找到通往该终点的路径，即命题的证明

3.3.3. 如果不能，那能说明这个命题是假命题吗？

3.4. 计算机在Mizar数据库中生成证明的流程

3.4.1. 整理出数学、几何学的基本公理列表

3.4.2. 制定推理规则

3.4.3. 用一系列相互关联的推理规则构建出某一定理的证明过程

3.5. 证明定理和下围棋在本质上是相互关联的

3.5.1. 两者都是在可能的输出结果树中寻找特定的节点

3.5.2. 每个节点又具有不同分支，且到达某一特定终点（叶子节点）的分支长度有可能非常长

3.5.3. 问题的关键就在于如何选择分支以获得最期待的输出结果

3.5.3.1. 赢得一场比赛或证明一个定理

3.6. 通过对Mizar相关数据的研究，DeepMind和谷歌研究团队发现其约有56%的定理证明没有人类参与的痕迹

3.6.1. 用计算机成功生成的证明来训练该机器学习算法，通过对Mizar数据库中已有数据的学习获得探索证明树的好方法

3.6.2. 已将Mizar数据库中机器证明的比例提高到了59%

3.6.3. 这个看似微不足道的“一小步”，代表的却是新技术应用的“一大步”

3.6.4. 它不仅仅是多证明一个定理或者多赢一场比赛，而是计算机可以完成的证明量增加了3%

3.7. 该算法在很大程度上扩展了计算机的应用范围，打开了计算机产生定理的新篇章

3.7.1. 就像学习演奏爵士乐的算法，决定它前景的是一个合乎音乐继续发展的逻辑，而不是接下来到底演奏哪个音

3.7.2. 实际上，机器只是盲目地生成了一些粗制滥造的“数学音乐”，而不是我所期望的“天籁之音”

3.7.3. 没有人评判这些新发现的价值，也没有人对其中是否有令人惊讶的启示而感兴趣

3.7.3.1. 它们只是新的而已

3.8. 首先创建一个数学命题列表，然后用公理去证明这些命题以验证其真假

3.8.1. 对命题的证明就是进入Mizar数据库的必要条件

3.8.2. 对于命题的实质是什么，是否有人会觉得它足够有趣，是否可以与其他数学家分享等，Mizar并不关心

3.8.3. 它所做的是，只要是对命题的证明，就在没经过筛选的情况下收录到数据库中

3.8.4. 换言之，它只是一个包含可以证明的一切的“巴别图书馆”

3.9. 很少有专业的数学家听说过Mizar项目，因为它的目的就不是让人真正感兴趣

3.9.1. Mizar构建的是看似包罗万象实则一无所有的“巴别图书馆”

4. 代数基本定理

4.1. 复数域上的n次多项式有且仅有n个根

4.2. 从17世纪初到现在，人类对它的证明中曾出现过多次失误，其中不乏最伟大的数学家，诸如欧拉、高斯、拉普拉斯等人

4.3. 直到1806年，让·罗伯特·阿甘（Jean Robert Argan）才提出第一个被公认为完整无误的证明

4.4. 以往证明中的错误都藏得很深，没有足够的时间检验，是极不容易被发现的

4.5. 倘若计算机能够发现人类证明中隐藏的错误，那么它在证明定理方面的正确性和有效性就会被刮目相看了