关注模型

改变视角真的很重要

无限：假设是球形的奶牛

陶哲轩：一个很好的例子是数学中的塞迈雷迪定理，于1970年代得以证明，它涉及在一组数字集合中寻找某种类型的模式，即等差数列，例如3、5、7或10、15、20。

塞迈雷迪证明了，对于任何足够大的数字集合，即正密度集合，都包含有任意长度的等差数列。

例如，奇数集合的密度为1/2，则其中包含任意长度的等差数列，因为其实奇数集合相当结构化，我可以轻松找到像11、13、15、17这个等差数列。

塞迈雷迪定理也同样适用于随机集合。

如果我取一组奇数集合，然后抛掷一枚硬币，只保留掷出正面的数字，随机去掉一半的数，将得到一个完全没有模式的集合。

但由于随机波动，你仍然会在这个集合中找到许多等差数列。

Q：能否证明在随机集合中存在任意长度的等差数列？

陶哲轩： 可以的，比如说无限猴子定理。如果一个房间内有无数会使用打字机的猴子，让它们随机打字，其中一只一定会打出完整的《哈姆雷特》剧本或任何其他有限的文本字符串。

这需要相当长的时间，但只要是无限，那么它终会发生。

所以如果你取一个无限的数字串或其他，最终都会呈现出你想要的任何有限模式，只是需要很长时间，等差数列也是如此。

Q：人类应当如何看待无限呢？

陶哲轩：可以把无限视作一个有限数的抽象，而它没有界限。但现实生活中其实没有真正的无限，但你可以假设，比如如果我想有多少钱就有多少钱，想走多快就可以走多快。

数学家就是利用数学将这种形式主义理想化，不是极大或极小，而是无限或零。此时，数学将变得简洁。

在物理学中，我们常常开玩笑地说，假设是球形的奶牛，现实世界中的问题总会受现实世界影响，但你可以理想化，将某些东西送到无限，某些东西送到零，数学就变得容易处理。

Lex Fridman：我想知道使用无穷大有多频繁地迫使我们偏离现实世界的物理规律。

陶哲轩：这里存在很多陷阱。我们在本科数学课上花费了很多时间教授分析学，但分析学是关于如何取极限，例如a+b恒等于b+a，有限项可以交换，但无限项时，如果有一个收敛于某值的级数，重新排列，它将突然收敛于另一个值，则会出现错误。

所以当使用无限时，必须引入ε和δ，以及特定的推理方式，以避免类似错误。

近年来，人们开始对无限极限下成立的结果进行有限化，也就是说，某件事最终将会成真，但无法确定具体时间和速率。

那么如果我没有无限只猴子，而是有限只，我需要等待多久才能看到《哈姆雷特》出来呢？

这是一个定量问题，可以用纯粹有限的方法解决，或者利用你的有限直觉。

结果表明，生成的文本长度将呈指数级增长，这也就是为什么你永远看不到猴子写出《哈姆雷特》的原因。也许你能看到猴子们写出了一个包含四个字母的单词，但仅此而已。

所以我发现，当把一个无限的陈述有限化，它就会变得直观得多，也就没那么奇怪了。当然缺点是有限化群要混乱得多，而无限化群在几十年前就得以发现，后来人们才将其有限化。

数学关注模型，物理解释模型

Q：数学与物理学之间，在理解和看待世界的方式上有什么区别？

陶哲轩：我认为科学通常是三者之间的相互作用：现实世界、我们对现实世界的观察，以及我们认为世界如何运作的心理模型。

我们无法直接接触现实，我们只拥有不完整且存在很多误差的观测结果。

当我们想要预测的时候，例如预测天气，我们只有简化的模型，有时也只能给出不切实际的假设，就像球形奶牛。

这就是数学模型，数学关注的是模型，而科学收集观察结果并提出解释模型。

数学让我们停留在模型内部，并询问模型带来的后果，以及对未来会做出什么预测、是否符合过去的观测数据。而这期间肯定存在共生关系。

数学与其他学科相比，是很不同寻常的，因为数学始于假设，比如模型的公理和模型的结论。

但几乎其它学科中，都是始于结论，比如我想建一座桥，然后去找到通往那个结果的路径。这当中很少存在假设，当然推理小说除外。

我们生活中所做的绝大多数事情都是由结论驱动的，包括物理学和科学，例如“这颗小行星会去向哪里？”、“明天的天气会是怎样？”，但数学却是从公理出发。

Q：物理学中存在理论与实验之间的张力，你认为发现有关现实的真正新颖思想的强有力方法是什么？

陶哲轩：需要同时拥有自上而下和自下而上，这是所有事物之间真正的互动关系。随着时间推移，观察、理论和建模都应该更接近现实，即使一开始它们总是相距甚远，只需要拥有其中一个就能弄清楚将另一个推向何方。

因此，如果你的模型预测的是实验未捕捉到的异常情况，它将会告诉实验者去哪里查找更多数据来优化模型，这需要反复操作。

在数学本身中，也存在理论和实验的部分。只是最近，理论几乎完全占据主导地位。99%的数学是理论数学，实验数学非常少。因为假如他们想要研究素数或者其它，可以直接利用计算机生成大型数据集。

就像高斯发现了一个猜想，数论中最基本的素数定理，它预测了一百万乃至一万亿可以有多少个素数。这个问题上，他主要靠自己计算，但也雇佣了人类计算员，用以计算前100000个素数并制作表格，做出预测。

这是实验数学的一个早期例子，但显然理论数学要成功得多，也是直到最近，做一些复杂的数学计算才变得可行。但即便我们现在拥有强大的计算机，也只有一部分数学事物可以通过数值探索。

比如有一种叫做组合爆炸的东西，当你想研究1到1000的所有可能子集，子集数量将会是2 的1000次方，这比目前的任何计算机可枚举的都要大得多。所以有些数学问题无法直接通过暴力计算来解决。

国际象棋则是另一个著名的例子。关于国际象棋排列的数量，我们至今无法用计算机完全解决，但我们现在有AI，它们不会探索博弈树中的每个位置，而是寻求近似值。

事实上人们现在就正在使用这种国际象棋引擎来做实验性国际象棋。他们正在重新审视古老的国际象棋理论，例如传统的经典开局，也许并不是最优解，他们希望用国际象棋引擎来实现改进。

我希望数学在未来会有更大的实验成分，也许将由AI驱动。

数学的不合理但有效

Lex Fridman：你提到了柏拉图的洞穴寓言。如果人们不知道洞穴是人们观察现实的影子，而不是现实本身，并且他们相信他们所观察到的就是现实——从某种意义上说，这是数学家和也许所有人类都在做的事情，即观察现实的影子——我们有可能真正接触到现实吗？

陶哲轩：这当中存在三个本体论的东西，分别是实际的现实、我们的观察和我们的模型，严格来说它们彼此不同，而我认为它们将永远不同。但它们会随着时间逐渐靠近，但在靠近的过程中必须舍弃掉你最初的直觉。

例如在天文学中，最初人们认为世界模型是平的，因为它看起来很平，且很大。而宇宙的其余部分，即天空，则看起来很小。所以当你从模型出发，它实际上与现实相去甚远，但它又符合当下你的观察结论。

但随着时间推移和越来越多的观察，模型将更接近现实，我们也会意识到地球是圆的，它在旋转，并围绕着太阳系运行，而太阳系围绕着银河系运行，而宇宙在膨胀，膨胀本身也在加速膨胀……但事实上就在今年，我们发现宇宙的加速也是非恒定的，由于暗物质或暗能量这类东西的存在。

我们有一个数据拟合相当好的模型，在某种程度上可以解释它。该模型只有几个你必须指定的参数。但人们会说，那是捏造因子，有足够的捏造因子，你就可以解释任何事情。可是数学的观点是，希望模型中的参数要比观测数据集中的数据点少。

如果一个模型有10个参数，可以解释10个观测结果，该模型将完全无用，这叫做过拟合。而如果你的模型只有两个参数，却解释了1万亿个观测结果，这就是暗物质模型，我认为它有14个参数，可以解决天文学家拥有的PB级数据。

所以你可以把一个物理数学理论看作是对宇宙的一种数据压缩，即把这些PB级数据压缩为一个可以用五页纸描述的模型，并指定一定数量的参数，如果它能以合理的精度拟合几乎所有的观测结果，那么压缩越多，你的理论就越好。

爱因斯坦说过这样一句话：“宇宙中最难以理解的事情是它是可理解的。”，这就是数学的不合理但有效。

实际上这里有一些可能的数学解释，比如数学中有一种叫做普适性的现象。许多宏观尺度上的复杂系统都是从大量微观尺度上的微小相互作用中产生，而由于组合爆炸，你会认为宏观尺度的方程一定比微观尺度的方程指数级复杂。

如果要完全精确地求解，比如模拟一盒空气中的所有原子，就像阿伏伽德罗常数这将会是巨大的，如果你真的试图跟踪每一个粒子，这将是荒谬的。

但某些定律只在微观尺度上涌现，几乎不依赖于宏观尺度上发生的事情，或者只依赖于非常少的几个参数。所以，如果要模拟盒子里包含万亿粒子的气体，只需要知道它的温度、压力、体积以及五六个参数，就可以模拟10^23或任何数量的粒子的所有信息。

因此，我们无法在数学上理解普适性，但存在一些可以帮助我们理解普适性发生原因的玩具模型，例如中心极限定理就解释了为什么钟形曲线在自然界中无处不在，那么多事物都是高斯分布。

现在甚至还有一个携带钟形曲线的模因，甚至模因也具有普适性。

如果你愿意，你可以选择元，但存在许多过程，比如选取很多独立的随机变量，以各种方式将它们平均在一起，取简单平均或更复杂的平均，我们就可以在各种情况下证明高斯曲线的出现。

但如果你有许多不同的输入，且它们之间存在某种系统关联，则可能得不到钟形曲线，所以普适性并不是100%可靠。

全球金融危机就是这方面的一个著名例子。人们认为抵押贷款违约的行为存在高斯曲线，如果在拥有抵押贷款的十万美国人中，询问违约比例，如果一切都是去相关的，将会生成漂亮的钟形曲线，然后你可以用期权和衍生品管理风险。

但如果经济中存在系统性冲击，推动所有人同时违约，那将是非常反高斯的行为，这就是2008年没有被充分考虑进去的后果。

我认为，现在人们更多地意识到，系统性风险实际上是一个更大的问题，模型很漂亮，但它可能不匹配现实。所以研究模型行为的数学非常重要，但也需要科学来验证它何时符合现实，何时不符合。两者都被需要。

而数学可以提供帮助，因为像中心极限定理就会告诉你，某些假设的输入之间如果不相关，那么你就会拥有高斯行为。它也会告诉你到哪里去寻找模型中的弱点。

所以如果你理解中心极限定理，就可以使用高斯行为或其它来模拟违约风险，如果你受过数学训练，你就会寻求输入之间的系统相关性，并询问经济学家这样存在多大的风险，然后你就可以继续了。所以在科学和数学之间总是存在这种协同作用。

Q：是否存在一种可以将不同领域的数学连接起来的底层结构？

陶哲轩：肯定存在相互联系的线索，数学的很多进展都来自于将两个先前没有联系的数学领域联系起来。一个古老的例子是几何和数论。在古希腊时代，它们并不被认为是相关的，直到笛卡尔意识到并发展了解析几何，可以用两个实数来参数化几何对象平面。几何问题最终可以转化为数字问题。

当然今天这两个领域已经统一了，类似的过程也在数学中反复上演，代数和几何曾是分开的，现在又有了代数几何。

我认为数学家也有各种风格，就像刺猬和狐狸，狐狸知道很多事但都只懂一点，而刺猬只知道一件事但知道得很深。理想的数学家合作就需要多样性，让一只狐狸与多只刺猬合作，或者反之亦然。

我主要认为自己是一只狐狸，我很喜欢套利这个金融说法，学习一个领域是如何运作的，了解该领域的技巧，然后去到另一个不相关领域，但我可以自行调整这些技巧，看到领域之间的联系。

所以还存在许多比我研究更深的科学家，他们是真的刺猬，了解一个领域的一切，且在那个领域更快、更有效，而我可以给他们提供额外的工具。

而两种思考之间，我更倾向成为狐狸，我喜欢寻找类比、叙述。假如我看到一个领域的结果并且很喜欢，但我不喜欢证明，尤其是它使用了我不是很熟悉的数学类型，我将经常会尝试用我喜欢的工具重新证明它。

通常我的证明更糟糕，但通过这样练习，我可以充分明白另一个证明试图在做些什么。由此我可以对那个领域使用的工具有所理解。这是非常具有探索性的，非常像是在疯狂的领域里做疯狂的事情，并且像是在大量重新发明轮子。

刺猬风格也会更学术，你将会非常注重知识，及时了解这个领域的所有进展。了解所有历史并对每种特定技术的优缺点有很好的理解。你会更依赖计算而不是试图寻找叙述。当然我也可以那样做，但始终有其他人在那方面更为擅长。

Q：你是在什么时候意识到数学可以有一种优雅和美感的？

陶哲轩：当我来到普林斯顿读研究生时，John Conway当时也在那里，他于几年前去世了。但我记得我参加的最早的研究讲座之一，就是Conway关于他的极端证明的报告。

Conway会以一种你通常不会想到的方式思考各种事物，他认为证明本身就占据了某种空间，所以如果你想证明某件事，比如说有无限多个素数，你可以把它们放到不同的轴上。

有些证明是优雅的，有些证明很长，有些证明是初级的。这样就有了证明空间，且空间本身具有某种形状。他对形状的极值点很感兴趣，比如在所有证明中，什么是以牺牲其他一切为代价的最短证明？或者什么是最初等的证明？或者其它。

所以他列举了一些著名定理的例子，然后他会给出他认为是这些定理的极端证明。这真的让人大开眼界，这不仅是得到一个有趣的结果证明，而且一旦你有了这个证明，试图用各种方式优化它，证明本身就拥有了一些技巧。

这也影响了我的写作风格。比如当你做本科数学作业时，你被鼓励写下任何有效的证明并交上去，得到一个勾，你就继续前进。

但如果你希望你的结果真正具有影响力并被人们阅读，它就不能只是正确的。它也应该让阅读成为一种享受，才能有动力推广到其他事物。

这和许多其他学科一样，比如像编码。数学和编码之间有很多类比。就像你可以用意大利面条式代码编写一些东西，它适用于某个任务，又快又脏而且高效。但其实有很多可以写好代码的好原则，这样其他人就可以使用它，并在此基础上构建，减少错误的发生，数学也有类似的事情。

另外还有一种叫做代码高尔夫的活动，我也觉得它美丽而有趣。人们使用不同的编程语言，来试图写出完成特定任务的最短程序。

我甚至相信这里存在一个比赛，不仅可以对程序进行压力测试，还可以对证明或者不同语言进行测试。也许这是一种不同的符号，用以完成不同的任务。

Lex Fridman：你觉得数学中最美丽或最优雅的方程是什么？欧拉恒等式常被认为是数学中最美丽的方程，你是否在那个方程式中，在欧拉恒等式中找到了美？

陶哲轩：我来说的话，我觉得最吸引人的是不同事物之间的联系，欧拉恒等式使用了所有的基本常数，这很可爱。但对我来说，指数函数是欧拉引入来测量指数增长的，所以复利或衰减，任何持续增长、持续减少、膨胀或收缩的东西，都可以用指数函数建模。

而π来自圆和旋转，如果你想转一根针180度，你需要旋转π弧度。而i复数表示虚轴上的摆动，对应90度的旋转，所以是方向上的改变。所以指数函数代表当前方向上的增长和衰减。当你在指数中加入i时，它现在变成与当前位置成直角的运动。

然后欧拉恒等式将告诉你，如果你旋转一个时间π，你最终会得到另一个方向。它将通过复化和i的旋转，将所有数学工具统一起来，包含数学、动力学、几何和复数。

而当你第一次研究任何东西时，你必须测量事物并为它们命名，有时因为模型与现实相去甚远，也会给错误的东西起了好名字，但直到后来你才发现什么是真正重要的东西。

例如在物理学中，E=MC²，其中一件大事就是E，而当亚里士多德首次提出运动定律，然后是伽利略或牛顿能测量质量、加速度、力等等，所以有了著名的牛顿第二运动定律F=ma。因为这些是主要对象，所以它们被赋予理论中的核心位置。

直到后来人们开始分析这些方程，才发现似乎这些量总是守恒的，特别是动量和能量。

而事物是否拥有能量，这并不明显，能量它不像质量、速度那样可以直接测量，但随着时间推移，人们逐渐意识到这实际上是一个非常基本的概念。

哈密顿最终在19世纪将牛顿物理定律重新表述为哈密顿力学，其中能量，也就是哈密顿量是主导对象，一旦你知道如何测量任何系统的哈密顿量，你就能完全描述动力学，即所有状态会发生什么。

它作为核心角色，起初也并不明显，而当量子力学出现时，视角的转变则提供了很大的帮助。

研究量子力学的早期物理学家，他们首先尝试将牛顿力学融入量子力学，但遇到了很多麻烦，因为一切都是粒子，而我认为它是波，总之结合起来非常奇怪。

如果你问，F=ma的量子版本是什么，这很难回答。但事实证明，在经典力学背后的哈密顿量也是量子力学的关键对象，这里也有一个叫做哈密顿算符的对象。它是一种不同类型的对象，是运算符而不是函数，但一旦指定了它，你就指定了整个动力学。

所以这里有一个叫做薛定谔方程的东西，它可以准确地告诉你，一旦你拥有哈密顿量，量子系统将会如何演变。

所以将二者放在一起，看起来是完全不同的对象，一个涉及粒子，一个涉及波。但有了中心性，就可以将很多直觉和事实从经典力学转移到量子力学。

例如，在经典力学中，有一个叫做诺特定理的东西。每当物理系统中存在对称性，就有出现守恒定律。所以物理定律是平移不变的。

比如如果我向左移动10步，我会体验到与初始位置相同的物理定律，这对应动量守恒。而如果我以某个角度转身，我又将再次体验到相同的物理定律。这对应角动量守恒。如果我等待10分钟，我仍然有相同的物理定律，由于存在时间平移不变性，这对应能量守恒定律。

所以在对称性和守恒之间存在这种基本联系，这在量子力学中也成立。尽管方程完全不同，但因为它们都源于哈密顿量，哈密顿量控制一切。当每次哈密顿量具有对称性时，方程就会有一个守恒定律。所以一旦你拥有正确的表述，很多事情都变得清晰起来。

我们无法统一量子力学和广义相对论，因为我们还没有弄清楚基本对象是什么，例如我们必须放弃空间和时间的概念，因为这些空间几乎是欧几里得类型，只在非常小的尺度上出现量子涨落，从而形成时空泡沫，试图用笛卡尔坐标xyz解释是行不通的，但我们还不知道用什么来代替它。我们没有类似于哈密顿量能组织起一切的类似数学概念。

直觉就在那里，你必须转移它

Q：你的直觉是否认为存在一个万物理论，可以找到一个统一广义相对论和量子力学的语言？

陶哲轩：我相信如此。多年来，物理学的历史就是统一的历史，就像数学一样。例如电和磁是分开的理论，然后麦克斯韦统一了它们。牛顿统一了天体的运动与地球上物体的运动。等等诸如此类，都说明了统一时有发生。

再次回到这个观察和理论的模型，我们物理学的两个大理论，广义相对论和量子力学，现在发展如此之好，加起来涵盖了我们所能做的所有观察的99.9%。

你现在要么去研究极其疯狂的粒子加速器，或者早期宇宙，再或者那些知道很难以测量的东西，才能偏离这两个理论中的任何一个，直到你真正弄清楚二者如何结合在一起。

但我相信，我们已经这样做了几个世纪，我们在以前也已取得一定进展，没理由我们应该放弃。

Q：您认为您会成为一名发展万物理论的数学家吗？

陶哲轩：经常发生的情况是，当物理学家需要一些数学理论时，通常数学家们已经研究出了一些前身理论。

所以当爱因斯坦开始意识到空间是弯曲的，他去找一些数学家询问弯曲空间理论是否可用，然后他说，他认为黎曼发展了黎曼几何学，这恰恰是一种空间以各种一般方式弯曲的理论。事实证明，这就是爱因斯坦理论几乎完全需要的。

这就又回到了数学的不合理的有效性，那些能很好地解释宇宙的理论，往往也能很好解决具有相同数学对象的数学问题。归根结底，它们只是组织数据的两种有效方式。

而弦理论，虽然几十年来一直保持领先，但我认为它正在慢慢退出历史舞台，因为它与实验并不匹配。

Lex Fridman：当前最大的挑战之一就是实验非常困难，因为两种理论都如此有效，但另一方面，你所谈论的不仅是偏离时空，更是进入一些疯狂的维度，你现在所做的事情，对我们来说，已经距离我们认为地球是平坦的时候相隔甚远，我们很难用有限的认知来感知那个所谓的现实到底是什么。

陶哲轩：这就是为什么类比如此重要。圆形的地球并不直观，因为我们被困在其上，但我们对圆形物体以及光的工作原理有相当好的直觉。

实际上，这是一个很好的练习，为了真正弄清楚日食、月相是如何发生的，可以用圆形地球、圆形月亮的模型很轻松地解释。你可以拿一个篮球、一个高尔夫球和一个光源，自己实际去做这些事情，直觉就在那里，你必须转移它。

现代科学也许是自身成功的受害者，为了更加准确，需要离最初的直觉越来越远。因此，对于没有经历过科学教育的人来说，这个过程显得相当可疑，因此我们需要更多科学基础。

有些科学家做了相当出色的外出推广工作，但在家里也可以做很多科学的事情。YouTube上有很多视频，我最近就和Grant Sanderson一起做了一个YouTube视频，我们讨论古希腊人如何能够测量到月球的距离、到地球的距离，并使用你自己也可以复制的技术，不一定是花哨的太空望远镜或令人生畏的数学。

改变视角真的很重要。旅游可以拓宽思维，而这就是智力旅行，你把自己放在古希腊人或者其它时期的人的脑海中，做出球形奶牛的假设，这是数学家所做的，也是一些其他艺术家正在做的。

如果你提出公理，那么数学会让你遵循这些公理并得出结论，有时你将可以从初始假设中走得很远。

想象自己是个矢量场

Q：能否从数学的角度解读广义相对论，它的那一方面让你感兴趣，对你来说具有挑战性？

陶哲轩：我研究过一些方程。有一个叫做波映射方程或西格玛场模型的东西，它并不完全等同于时空引力本身的方程，而是某些可能存在于时空之上的场的方程。

所以爱因斯坦的相对论方程只描述时间和空间本身，但还有其他场存在，比如电磁场、杨-米尔斯场，以及一整套不同的方程。

其中爱因斯坦方程被认为是最非线性和困难的方程之一，但在层次结构中相对较低的，是这个叫做波映射方程的东西。

这是一个波，在任意给定点上都像是被固定在一个球体上。所以我可以想象时空中有许多箭头，这些箭头指向不同的方向，像波浪一样传播。如果你摆动其中一个箭头，它会传播并使所有箭头移动，这有点像麦田里的麦浪。

我对这个方程的全局正则性问题很感兴趣，那么是否可以让所有能量集中于一点呢？所以我考虑的方程实际上是所谓的临界方程，它实际上在所有尺度上的行为都大致相同。我勉强证明了，你实际上无法强迫所有能量都集中到一点上，能量必须在此刻稍微分散一点，而一旦它分散一点点，它就会保持正则。

是的，这是在2000年发生的事。所以这其实也是我后来对纳维-斯托克斯方程感兴趣的部分原因。我开发了一些技术来解决这个问题，所以得出的部分结论是由于球体的曲率，这个问题实际上是非线性的，存在一种非微扰效应。

当你正常观察它时，它看起来比波动方程的线性效应更大，即使你的能量很小，也很难将其控制。

但我开发了一种叫做规范变换的东西，方程有点像麦浪的演化，它们都在来回弯曲，存在很多运动。但如果想象一下，通过在空间的不同点上，附加小摄像机来稳定流动，这些摄像机试图以捕捉大部分运动的方式移动，在这种稳定的流动下，流动将会变得线性得多。

我发现了一种可以减少非线性效应量的变换方程，然后我就能够求解这个方程了。这是我在澳大利亚拜访我的姨母时，发现的这个变换，当时我试图理解所有这些场的动力学，但我无法单单用纸笔完成，也没有足够的计算机设备来做任何计算机模拟。

所以我最终闭上眼睛，躺在地板上，想象自己实际上是个矢量场，然后来回翻滚，试图找到如何改变坐标，让各个方向的事物都能以合理的线性方式运行。

当我这样做时，我的姨母走进来问道，我在做什么。我回答说，这很复杂。于是姨母说，好吧，你是年轻人，我不多问了。

学会策略性“作弊”

Q：你是如何解决难题的，是否在脑海中经常可视化数学对象、符号？

陶哲轩：有很多的纸和笔。作为一名数学家，我学到的一件事情是，策略性作弊。

数学之美在于你可以随心所欲地改变规则、改变问题，这是其它任何领域都无法做到的一点。如果你是一名工程师，有人说，在这条河上建造一座桥，你不能说，我想在这里建一座桥或者我想要纸而不是钢来建造它，但作为数学家，你可以做任何你想要做的事情。

这就像试图通关一个电脑游戏，其中有无限的作弊码可用。你可以自行设置，例如有一个很大的维度，我可以先将其设为一，先解决一维问题，因此存在一个主项和一个误差项，所以我需要做一个球形奶牛假设，假设误差项为零。

所以当你试图寻找解决问题的方法，不应该在铁人模式下进行，让事情变得最大化困难，更合理的解决方式是，如果有10件事让你的生活变得困难，你可以先找到其中一个问题并关闭另外九个困难。

这样你就安装了九个作弊码，而如果你安装了十个作弊码，那么这个游戏将是微不足道的。当你安装九个，然后集中解决那一个问题，它将教会你如何解决那个特定的困难，然后你关闭这个，再打开其它问题并依次解决。在你最终学会如何分别解决这10个问题后，再将其中几个合并处理。

小时候，我看了很多我们文化中的香港动作片，每次遇到打斗画面，例如英雄会被一百个坏蛋喽啰包围，在精心设计的场景下，他一次只会与一个人战斗，打败那个人后再继续前进。正因为如此，他可以打败他们所有人。

但是，如果这群人更聪明一点，就应该直接蜂拥而上，当然这样电影效果会很糟糕，但他们会赢。

Q：你通常是使用纸和笔工作吗？是否会使用计算机和LaTeX工作？

陶哲轩：实际上主要是纸和笔。在我的办公室里，我有四块巨大的黑板，有时候只需要把我所知道的关于问题的所有信息都写在这上面，然后我会坐在沙发上，看着整个东西。

其中有很多绘画和只有自己能理解的定制涂鸦。黑板的美妙之处在于可以擦除，但现在我也开始越来越多地使用计算机，部分原因是因为AI能执行简单的编码工作，让事情变得更加容易。

以前如果我想要绘制一个中等复杂度的函数，包含一些迭代或其它东西，我必须记住如何设置Python程序、以及循环如何工作并调试它，这需要两个小时的时间。但现在我可以在10到15分钟内完成，所以我现在使用越来越多计算机进行简单的探索。

总有算法来负责将一棵树和另一棵树进行匹配

Q：可以描述一下Lean形式化证明编程语言吗？以及它是如何作为证明助手提供帮助的？

陶哲轩：Lean是一种计算机语言，就像Python和C等标准语言一样，但在大多数语言中，重点在于产生可执行代码。代码行会执行一些操作，例如翻转比特、让机器人移动或在互联网上发送文本等。

而Lean也是可以做到这一点的语言，可作为一个标准的传统语言运行，但它也能生成证书。像Python这类软件可能会进行计算并告诉你3+4的答案是7，但Lean不仅可以生成答案，还能生成它是如何得到7的证明，以及其中涉及的所有步骤。

它创建了更为复杂的对象，不仅仅是陈述，而是带有证明的陈述。每一行代码都只是将先前的陈述拼凑在一起，然后创建新陈述。

这个想法并不新鲜，它们被称为证明助手。它们提供语言，让你可以创建相当复杂精细的数学证明。如果你的编译器可信，那它们会生成证书，确保你的观点100%正确，但它们也会让编译器变得非常小，并且有多个不同的编译器可用。

Q：你是否可以描述一下在纸笔上书写和使用Lean编程语言之间的区别？形式化一个陈述有多难？

陶哲轩：很多数学家都参与了Lean的设计，所以它被设计成单独的代码行，类似于数学论证的单独行。比如你可能想引入一个变量，证明一个矛盾。有很多你可以做的标准操作，理想情况下应该是一一对应的，但实践中并非如此。

Lean就像向一个极其迂腐的同事解释一个证明，他会指出，你真的是这个意思吗？如果这个是零怎么办？你如何证明这个？而Lean中包含很多自动化功能，可以减少麻烦。

例如，每个数学对象都必须包含一个类型，比如谈论X，X是实数、自然数，还是函数或者其它，如果非正式数学，它通常需要有上下文，例如“显然X是Y和Z之和，Y和Z是实数，那么X也应该是实数。”

Lean可以做很多类似的事情，每隔一段时间它就会说，你能告诉我更多关于这个对象是什么的信息吗？它是什么类型的对象？所以你必须在哲学层面上思考更多，不仅仅是你正在做的计算，而是每个对象在实际意义上代表什么。

Lex Fridman ：它是使用LLM进行类型推断吗？还是可以与实数匹配？

陶哲轩：它使用了更传统的老式AI。你可以把这些东西都表示成树，总有算法来负责将一棵树和另一棵树进行匹配。每个物体都有历史可以追溯。

Lean是为可靠性而设计的，所以现代AI没有被用在里面，它是一个完全不相关的技术。

所以当一个数学家试图在Lean中编程一个证明时，通常会有这样一个步骤，比如“好的，我现在想要使用微积分的基本定理来做下一步。”

所以Lean开发者构建了这个庞大的项目mathlib，它是一个包含数万个有关数学对象有用事实的集合，其中就有微积分基本定理，但你需要找到它，所以现在的很多瓶颈是引理搜索。

你可以有各种专门用于数学引理搜索的搜索引擎，但现在有了这些大型语言模型，你就可以直接询问它们，例如当我编码时，我在我的IDE中安装了GitHub Copilot作为插件，它会扫描我的文本，看到我的需求。

当我需要使用微积分基本定理时，它会提供建议，25%的时间它完全正确，另外10-15%的时间它不完全有效，但足够接近，然后我会告知它需要修改的地方，它就会生效，然后大约有一半的时间，它给我的是完全的垃圾。但人们开始在上面使用一点点人工智能，主要在自动补全的层面上，你可以输入证明行的一半，让它告知你另外一半。

所以我现在估计，将一个证明形式化出来所需的时间和精力大约是写出来所花费的时间和精力的10倍，它是可行的，但很烦人。

这是它唯一迂腐的地方，但在某些情况下，形式化地做事情实际上更愉快。有一个我形式化了的定理，在最终陈述中存在常数12，12必须贯穿整个证明，所有其它数字都必须与这个最终数字12保持一致，所以我们写了一篇围绕着数字12的定理文章。

然后几周后，有人说可以通过重新处理其中一些步骤，将12改进为11。当这种情况发生在纸笔上时，每改变一个参数，就必须逐行检查证明的每一行是否仍然有效，并且可能存在一些你没有意识到的微妙之处，你没有意识到你在利用12的某些性质，所以一个证明可能在微妙之处崩溃。

所以我们用常数12形式化了这个证明，当新论文出来时，花了我们20个人大约3周时间形式化。然后现在将12更新到11，在Lean里面直接修改就行， 然后运行编译器，在所拥有的数千行代码中，90%仍然有效，只有少数几行标红。

现在我无法证明这些步骤的正确性，但它立即隔离出哪些步骤你需要改变，你可以跳过所有正常工作的部分，只会有一小部分地方需要你修改。所以在一两天内，我们就把我们的证明更新到了11。这是一个非常快的过程，比纸笔要顺利得多。

由于证明更长，每个单独的部分更容易阅读。例如当你拿到一篇数学论文，跳到第27页，看第6段，这里有一行数学文本，我常常不能立即读懂它，因为它假设了各种定义，我必须回去去找，也许10页前定义了这个，证明总是分散在各处，所以你基本上被迫连续阅读。

它不像小说那样，可以打开一半开始读，这里存在很多上下文。但当证明在Lean中时，如果你把光标放在某一行代码上，那里的每个对象，你都可以让光标悬停，它会说出这是什么，来自哪里，在哪里被证明。这比翻阅数学论文更容易回溯事物。

所以，Lean真正实现的一件事是，在原子尺度上协作证明，这在过去是无法做到的。所以传统上，当你想与另一位数学家合作时，要么在黑板前进行真正的互动，要么通过电子邮件或其它方式，但必须进行分段，例如我要完成第3节，你做第4节，但不能真正在同一时间在同一件事上协作工作。

但有了Lean，你就可以尝试形式化证明某一部分，然后说，我在第67行卡住了，我需要证明这个东西，但它并不完全有效，这是我有麻烦的三行代码。由于所有上下文都在那里，别人可以说，好的，我知道你需要做什么，你需要应用这个技巧或这个工具。

你可以进行极其原子级别的对话。因为Lean，我可以与世界各地的几十个人合作，其中大多数人我从未见过面。实际上我也不知道他们在过程中是否可靠，但Lean给了我一份信任证书，这样我就可以进行无信任数学。

Q：在合作时，解决数学难题的正确方法是什么呢？是分而治之，还是你会专注于某个特定部分，并且正在头脑风暴？

陶哲轩：首先总是有一个头脑风暴过程。对于数学研究项目，本质上从一开始，你真的无从下手。它不像一个工程项目，理论已经确立了几十年，实施才是主要困难。你甚至必须弄清楚什么是正确的路径。

就像我之前说的“作弊”，回到建桥的类比，首先假设你拥有无限的预算和无限的劳动力，现在你能建这座桥吗？那现在有无限的预算但只有有限的劳动力，现在你能做到吗？当然没有工程师能真正做到这一点，因为他们有固定的要求。

在项目开始你总是会尝试各种疯狂的事情，做出所有不切实际的假设，但你计划稍后再来修正解决。然后你会尝试看看是否存在一个可能有效的方法框架，并寄希望于将问题分解为更小的子问题，然后你就可以专注于子问题。

有时不同的合作者更擅长处理某些事情。例如我和本·格林的一个定理，叫做格林-陶定理（the Green-Tao theorem）定理。它是一个关于素数包含任意长度的等差数列的陈述，这是对塞迈雷迪定理的一个修改。

而我们合作的方式是，本已经证明了长度为3的等差数列含有一个类似的结果。他表明，像素数这样的集合包含大量长度为三的数列，甚至素数的某些子集也包含。但他的技术只适用于长度为三的数列，不适用于更长的数列。

但我有这些来自遍历理论的技术，这是我当时一直在玩的技术，我比本更熟悉。所以如果我能证明某些与素数相关的集合的特定随机性性质，就存在一定的技术条件拥有它。如果本能为我提供这个事实依据，我就可以得出定理。

但我要的是数论中一个非常困难的问题，他说我们不可能证明出来这个，所以他说，你能用一个弱假设来证明你的那部分定理吗？他提出了一些他可以证明的东西，但对我来说太弱了，我不能用这个。所以类似的对话来回进行。

我们之间存在不同的作弊方式，我想作弊更多，他想作弊更少。但最终我们找到了一种属性：A、他能证明；B、我可以使用，然后我们就可以证明我们的定理。所以要知道每次合作都会发生一些故事，没有两次完全相同。

Lean可以帮助科学家大规模地生产实验结果

Q：如何看待Lean这一类编程语言？

陶哲轩：目前只有少数数学项目可以以这种方式划分，在当前的技术水平下，大部分的Lean活动都是在形式化人类已经证明的定理，基本上一个数学论文就是一个定理或一种意义上的蓝图。

Lean可以将一个困难的陈述，比如一个大的定理，分解成100个小的引理，但通常不是所有的定理都写得足够详细以至于每一个都可以直接分解。

而蓝图就像一份非常繁琐的论文，其中每一步都尽可能详细地解释，并试图使每一步都相对独立，仅依赖于少数几个已证明的前置陈述，因此蓝图中的每个节点都可以独立处理，甚至不需要了解整个系统的运作方式。

嗯，这就像现代供应链，如果你想要制造一部 iPhone 或其他复杂物体，没有人能够独立完成整个物体，但你可以让一个专家，如果他们从其他公司获得一些部件，就能将它们组合成稍大一些的部件。

Lex Fridman：我认为这是一个非常令人兴奋的可能性，因为如果找到可以按这种方式分解的问题，就能拥有分布在全球各地的、成千上万的贡献者，是这样么？

陶哲轩：对的。目前大多数数学都是理论性的，而实验性数学则相对较少，我认为像Lean和其他软件工具，比如GitHub之类的，将允许实验数学以比我们现在所能做到的更大程度进行规模化。

现在如果你想要做任何关于数学模式或什么的数学探索，你只需要写一些代码来描述这个模式。我的意思是，有时候有一些计算机代数软件包会提供帮助，但通常只是由一位数学家编写大量的Python或其他代码。毕竟编程是一项容易出错的活，所以让其他人协作编写你的代码模块并不实际，因为如果其中一个模块有bug，整个系统就不可靠。

这些定制的意大利面条式的代码，由不是专业程序员而是由数学家编写的，它们笨拙而且缓慢，所以很难大规模地生产实验结果。但是有了Lean，数学家就能更好地进行这些工作。我有一个项目叫方程理论项目，在这个项目中我们生成了大约 2200 万个抽象代数的小问题。

(图片来源于方程理论项目页)

抽象代数研究乘法和加法等运算以及抽象的性质，比如乘法的交换律，XY总是等于YX，至少对数学来说是这样，这些运算遵循一些其它运算不遵循的法则。

但并非所有的法则都是通用的，任何操作都可能遵循其它操作不遵循的法则，所以我们生成了大约4,000种可能的代数法则，以适应不同的运算。

我们的问题是哪些法则会隐含哪些其他法则？嗯，例如，交换律是否隐含结合律？答案是否定，因为事实证明你可以描述一个操作，它遵守交换律但不遵守结合律，但另外一些法则确实蕴含其它法则，有时它们可以彼此替换，可以用一些代数进行证明。因此我们研究了这4000条法则之间的配对，大约有2200万对组合，对于每一对我们都会问：这条法则是否蕴含了那条法则？如果是，请给出证明；如果不是，请给出反例。

这2200万个问题，每一个问题都可以交给一个本科生代数学生，他们有相当大的机会能够解决这些问题。尽管在这2200万个问题中，有少数几个，比如100个左右，确实非常难，但是很多问题都很简单。这个项目的目标就是确定整个图里哪些法则暗示了其它的法则。

Lex Fridman：这真是一个了不起的项目，一个好主意、好测试。这正是我们一直在讨论的问题，规模令人瞩目。

陶哲轩：是的，所以这种事情交给人工是不太可行的，我的意思是，最先进的技术在文献中大约会有15 个方程以及它们的应用方式，这差不多就是人类研究论文所能达到的极限了。如果你需要将规模扩大，就需要把这个项目众包，还需要信任——没有人能检查 2200 万个这些证明。你需要实现自动化，这只有在有了Lean之后才成为可能。

我们也希望大量使用人工智能，所以这个项目已经接近完成了：在这2200万个证明中，只剩下2个没有得到解决。而实际上，关于这两个，我们有两份纸笔证明，今天早上我还在努力完成它。所以这个项目我们几乎完成了。

Lex Fridman：这太厉害了，你能够招募到多少人去完成这个项目？

陶哲轩：50个左右 ，这在数学上被认为是一个巨大的数字。所以我们有一篇有50位作者的论文，还有一个大的附录说明每个人贡献了什么。

Q：在这种多人参与的项目中，有没有一种类似ELO评分的情况，可以根据贡献者的专业水平来为他们的贡献打分？

陶哲轩：这些精益项目的美妙之处在于，你可以自动获取所有这些数据，你知道，所有内容都必须上传到 GitHub，而 GitHub 会追踪谁贡献了什么。所以你可以在任何时间点生成统计数据，你可以说，哦，这个人贡献了这么多行代码或者其他什么的。但这些都是非常粗糙的指标，我不希望这会成为人们晋升评审的一部分。

不过我想在企业计算领域，人们已经在使用这些指标作为评估员工绩效的一部分了，再次强调，这是一个有点可怕的方向，会导致学术水平下降，我们不喜欢指标。

Lex Fridman：但学术界却在使用它们，只是使用的是旧指标，像论文数量。感觉这是一个有缺陷的指标，但也正朝着正确的方向发展，对吗？

陶哲轩：是的，我认为研究它很有趣，我们可以做研究来判断这些是否是更好的预测指标。有一个发现叫作古德哈特定律 (Goodhart’s law)，如果一个统计数据实际上被用来激励表现，它就会变成一种游戏，而不再是一种有用的衡量标准。

因此，我们这个项目采用的是自我报告的形式。实际上，在科学领域存在关于人们贡献类型的标准分类，有概念、验证、资源提供、编程等等。

有一个包含12个左右类别的标准列表，嗯，我们要求每位贡献者在一个包含所有类别所有作者的巨大矩阵中，在他们认为自己做出贡献的地方打勾，并且给出一个粗略的想法。比如你可能做了一些编程工作、提供了一些计算资源，但没有做任何纸笔验证或其他工作什么的……

传统上数学家们只是按姓氏的字母顺序排列，而我们没有这种传统，科学也有第一作者、第二作者的划分等等，我们也没有。

我们为此感到骄傲，因为我们让所有作者拥有平等的地位。

但它也不能完全上升到这个高度。十年前我参加了一个一些被称为“多数学者项目”的事情，它是众包数学，那时候还没有Lean，所以它受限于需要一个主持人来检查所有提交的贡献是否真正有效，这实际上是一个巨大的瓶颈。嗯，我们仍然有一些项目有10位作者左右，但我们当时已经决定不要试图划分每个人做了什么，而是共同使用一个假名，因此我们以 Bwaki 的精神为基础，创造了一个名为DHJ Polymath的虚构人物，Bwaki是20世纪一群著名数学家的笔名。

当时的论文是以DHJ Polymath这个笔名来发表的，所以我们都没有获得作者署名。实际上这不算一个好结果，原因有几点，其中的一点是，如果你想要被考虑终身教职或者什么，你不能使用这篇论文作为你的出版物之一去提交，因为你没有正式的作者署名。另一件事情是，直到很久以后人们才意识到，当人们提到这些项目时，只会提到项目中参与的最著名的人，而不是其他参与者。

所以这次我们尝试了一些不同的：让每个人都有作者身份，同时附上这个矩阵来解释它如何运作。

Lex Fridman：仅仅是参与这样的大型合作项目就足够出色了。我看过几年前Kevin Buzzard关于 Lean 编程语言的一个演讲，你说这可能是数学的未来，这一点也很让人兴奋——世界最伟大的数学家之一也在拥抱这个似乎正在开创数学未来的东西。