1. 数学研究

1.1. 数学研究变得更为艰难了

1.1.1. 学科分支越发密集，问题越发复杂

1.1.2. 攻读博士学位的3年时间，只够去理解导师所给题目的含义

1.1.3. 随后，再花费数年时间去研究、探索，运气不错的话，会得到一些研究成果

1.1.4. 然而，你发表的论文却面临着没人能审核它

1.2. 审核别人发表的论文是得不到太多报酬的，但期刊论文的审核必须经过同行的评审

1.2.1. 有一个像Coq证明助手这样的系统就非常重要了

1.3. 数学的发展虽然受到人类大脑局限性的制约，但借助于计算机，我们对数学的探索已远远超出了人脑的思维范畴

1.3.1. 如果很难找到通往“新奇迹”的方向，人们终将失去创造的原动力

1.4. 费马大定理的证明长达数百页，跨越3个世纪，这说明人类拥有足够的耐心

1.4.1. 当你努力去证明一个极其复杂的猜想时，隐约会有一种突破人类大脑物理极限的感觉

1.4.2. 数学是无限的，而人的能力是有限的

1.4.3. 我们常会为自己所做的努力感到吃惊，因为我们用数学的方式证明了“数学海洋的广阔无边”

1.4.4. 鉴于我们可能即将触及人类自身能力的极限，一些数学家已意识到，如果希望人类文明持续进步，我们将需要更多的机器辅助

1.5. 奥地利数学家、逻辑学家库尔特·哥德尔（Kurt Gödel）有过论证：数学中包含了许多没有经过证明的真理

1.5.1. 人们创造出了一套庞杂且仍在扩展的公理系统，但人们研究它的目的越来越说不清楚

1.5.2. 数学家是将咖啡转化为定理的机器。

1.5.2.1. 著名的匈牙利数学家保罗·厄多斯

1.6. 数学家只用铅笔和纸张工作的日子即将结束

1.6.1. 以色列数学家多伦·泽尔伯格（Doron Zeilberger）

1.6.2. 人们之所以不愿倚重人机合作的方式，是因为“狭隘的人本主义”在作祟，这种偏执与其他形式的偏执一样，阻碍了人类发展的脚步

1.6.3. 人类再也不可能仅使用笔和纸来探求数学的奥义了

1.7. 不仅希望能得到真理，并且希望探求真理背后更多的内涵

1.7.1. 如果计算机在无法真正理解数学的情况下就能验证数学真理，他们会觉得非常荒谬

1.7.2. 我们的理想是探究数学真谛，而不是利用机械执行指令的计算机推演论证

1.7.2.1. 菲尔兹奖的数学家迈克尔·阿蒂亚（Michael Atiyah）

1.8. 在数学领域里，利用计算机完成很多工作已经变成现实

1.8.1. 现在，人类很多刚发表的论文就已过时了，其实完全可以用算法来替代人类完成这些工作

1.8.2. 现如今我们遇到的很多问题已经变得毫无意义，但是我们还是继续在做，仅仅因为这是人类可以做的事情

1.8.3. 为了做某事而做某事所带来的意想不到的成果已经多次证明，无目标驱动的研究有时是收集真正的新见解的最佳方式

1.9. 我们非常擅长搞定计算机无法做到的事情

1.9.1. 如果目前所知道的一切定理都可以通过计算机得到证明，那我们就可以去探索计算机无法解决的其他问题，这有可能成为未来的“数学”

1.9.2. 人类的许多研究成果不是向前而是横向平行延伸的

1.9.3. 在某些领域我们确实达到了临界点，想要超越珠穆朗玛峰的高度就必须借助一台机器

2. 弗拉基米尔·沃沃斯基

2.1. Vladimir Voevodsky

2.1.1. 明星数学家，他仅用传统的纸笔工具就在数学研究领域成绩斐然，但后来他开始倡导数学家使用计算机技术辅助研究工作

2.2. 沃沃斯基认为安非他命能使他产生大量幻觉，可以使他激发出极大的灵感

2.2.1. 正常蜘蛛可以迅速织出形状规则的网，而摄入咖啡因的蜘蛛织的网就像一团乱麻

2.3. 两个危机

2.3.1. 涉及“理论数学”和“应用数学”的分离

2.3.1.1. 沃沃斯基极其重视向外界阐述他所从事的研究工作将来会对社会产生的深远影响

2.3.2. 另一个危机更像是一场生存危机，它与数学研究变得日益复杂有关

2.3.2.1. 即使数学家们能够精通各自研究的细分领域，但对他人的研究过程和成果缺乏足够的了解

2.3.2.2. 沃沃斯基认为，如果人类无法检验彼此的证明成果，那么我们可能需要寻求机器的帮助

2.3.2.3. 大多数数学家继续坚信，在自身敏锐直觉的引导下，人类思维才是促进方程和几何研究发展并可获得解决方法的核心力量

2.3.2.3.1. 谈论使用计算机辅助研究似乎就是误入歧途

2.4. 同时化解两个危机的方法

2.4.1. 他发现看似呆板机械的数学范式竟然完美地构建了计算机世界

2.4.2. 他可以利用这种“新语言”来创建一套全新的研究数学领域的基础方法，计算机将在其中发挥核心作用

2.5. 学术期刊的论文迟早会由于过于复杂而无法得到详细的论证，而这将导致期刊文献中出现未检测到的错误

2.5.1. 数学是一门深度学科（具有复杂的层阶结构），一篇论文通常将之前许多篇论文的结论作为依据，这种错误的叠加效应将会得到非常危险的结果

2.5.2. 他发现唯一可行的计算机系统是法国的Coq系统，它能够引导证明

2.6. 他致力于研究数学如何避免发生潜在灾难的问题

2.6.1. 运用数学方法来解决其他领域的问题

2.6.2. 他发现自己并没有深入探究生物学问题的工具和技能

2.7. 如果你想要深入了解某些知识和概念，就试着备课并教会别人

2.7.1. 计算机学者所使用的程序设计语言，起初看似难懂，实则是他早些年作为数学家时运用过的一种抽象世界的范式

2.8. 那些仍用纸笔计算的学者（可能现在也使用计算机来检验常规计算结论）和那些想用计算机来证明新定理的学者之间仍然存在较大分歧

2.8.1. 虽然使用计算机检查证明结论的方法正在被更多人接受，但数学研究的方向和方法依然掌握在人类手中

2.8.2. 计算机还不具备在数学研究领域的独创能力

2.9. 新的数学研究方法首先会被一小部分人运用，然后逐渐普及，最终成为标准，紧接着就会出现在数学专业研究生的课堂上，进而推广到本科教育阶段

2.9.1. 这个过程大约需要几十年，接下来会发生什么就不得而知了