Terence Tao Discusses AI's Role in Transforming Mathematics and Problem Solving

在最近的一次长达三小时的深度访谈中，陶哲轩探讨了如何解决难题以及人工智能（AI）将如何重塑数学领域。以下是一些关键点的总结： 陶哲轩： 我们可以聊一聊AI，特别是计算机辅助证明的情况。你能介绍一下Lean形式化证明语言吗？它是如何工作的？你是如何开始使用它的？它在哪方面帮助了你？ 解答： Lean是一种编程语言，与Python和C等传统语言类似，但其主要功能不仅仅是执行指令，例如翻转比特、驱动机器人或传输信息。Lean的独特之处在于它可以“生成证明”。比如用Python计算3 + 4时，你会得到答案7，而Lean不仅给出答案，还会生成一个形式化的证明，解释为什么等于7。每一行代码实质上是将已有的数学命题拼接起来，从而推导出新的结论。 这种方法并不新颖，这类系统被称为“证明助手”(proof assistant)，它们为构建复杂的数学证明提供了一个形式化的语言。如果你相信Lean的编译器，那么它产生的每一个证明都可以被视为100%正确的“证明证书”。而且，Lean的编译器设计精巧，目前已有多个版本可供选择。 陶哲轩： 那Lean与传统的纸笔证明有什么不同？把一个数学问题形式化到计算机中有多难？ 解答： Lean的设计吸收了很多数学家的意见，因此它的语法尽可能地模拟“数学证明的语言”。你在引入变量、使用反证法等过程中，可以用标准化的方式表达。从理论上讲，Lean可以实现证明语言与代码之间的一一对应，但在实际操作中仍存在一定的差异。Lean更像是一种极具挑战性的工具，它会不断质疑你：“你确定这就是你想说的吗？如果是0呢？这一步你如何保证的？”尽管如此，Lean要求你对每个对象类型进行明确说明，例如变量X是实数、自然数还是函数；而在非正式写作中，这一点往往通过上下文推断。 Lean的强大之处在于它可以在推理过程中自动推导大量信息，但有时也会打断你的思路，不断要求你提供更多细节。这种交互方式有点像是在进行极其严格的逻辑推导，你需要始终保持警惕，思考每一个对象的本质。 陶哲轩： 这是否会影响数学家的工作氛围？如果能形式化的问题拆分得足够模块化，是否就能吸引大量合作者，实现分布式的数学协作？ 解答： 确实如此，我认为这是一个非常鼓舞人心的可能性。虽然目前只有少数数学项目能够采用这种方式拆分，但在未来，随着技术的发展，Lean及其类似平台可能会吸引更多人参与数学研究。例如，在处理一个数学问题时，你需要写代码来模拟这个过程。即使有一些计算软件包可以辅助，很多时候数学家还是需要自己写一堆Python代码，这种过程极易出错，并且因为代码的不稳定性，很难与他人合作。如果有bug，整个系统就不可信了。因此，大家写出的代码常常如同“意大利面条”一样复杂、冗余且难以共享，这正是实验数学研究的一个障碍。 然而有了Lean，我已经开始了一些项目，不仅是利用数据进行实验，而是在证明本身上进行实验。我们的一个叫“等式理论项目”(Equational Theories Project)的研究生成了大约2200万个抽象代数中的小问题。每一个问题都由不同的规则推导出来——例如，交换律（X × Y = Y × X）和结合律（(X × Y) × Z = X × (Y × Z））等特性。我们列出大约4000条可能的代数规则，并试图弄清楚某些规则是否能推导出其他规则。例如，交换律是否能推导出结合律？如果能，请给出证明；如果不能，给出反例。 这些问题是很好的学术练习材料，大多数都很基础，只有大约100个左右稍显复杂。项目的目标就是画出一张详细的“推理论证图”——哪些规则可以推导出哪些其他规则。这项工作在过去是不可能完成的，因为即使是人类数学家也很难处理这么复杂的规则网络。而现在，得益于Lean，我们可以通过“自我报告”的方式追踪每个规则的来源。科学界有自己的一套分类标准，用于描述合作者的价值：构想、验证、资源、编码等，总共大概十二项。我们把所有参与者排成矩阵，让他们自行选择在哪些类别上有贡献。例如，你写了代码并提供了计算力，但没有参与人工验证，那你的贡献就很明确。 陶哲轩： 那这些项目的协作方式是否有按照贡献者的背景进行组织？ 解答： 确实有一些天马行空的想法，特别是在如何评估个人贡献时。项目的一个亮点是Lean可以自动生成所有数据。我们将所有代码上传到GitHub，GitHub记录着谁写了什么，这样我们就可以随时生成数据统计，例如谁写了多少行代码。当然，这只是粗略的指标。我们不希望这些数据被用于正式的考核评价，因为那样可能会引发类似“Goodhart’s Law”的问题：如果一个统计数据被用来激励绩效，人们就会“钻空子”，失去数据原本的参考价值。相反，我们采用了“自我报告”的方式。 数学界的传统是按姓氏字母排序。我们并不像自然科学那样按“第一作者”“第二作者”等方式区分，而是将所有作者视为平等。即便如此，一些大型项目中维持这一传统也非常困难。比如，十年前我参与了一个叫博学计划(Polymath projects)的研究项目，那是集体合作的数学研究，但没有Lean的形式化支持。完全依赖人力核对贡献，这导致了很多混淆。即使是如此，我们也有约10位合作者。当时我们决定不指定谁做了什么，而是使用一个共同的名字DHJ Polymath。这个虚拟的集体名字给人一种20世纪著名数学团体的感觉。 总的来说，Lean不仅提升了数学证明的严谨性，还为分布式合作提供了新的可能性。尽管目前的应用还比较有限，但它已经显示出未来发展的巨大潜力。