陶哲轩3時間インタビュー：難題解決とAIによる数学の再定義 陶哲轩が語る、Leanを使った証明の形式化とAIの数学への影響 LeanとAIが数学証明に新たな視点をもたらす方法 数学者として、Leanと紙上の証明の違いとは何か？ Leanが数学証明の形式化と共同研究にどのように貢献しているか 数学の基礎から複雑な理論まで、Leanがどのように証明をサポートするか Goodhartの法則とLeanプロジェクトでの協力者の評価方法 要約： 数学者の陶哲轩氏が、Leanという証明助手システムとAIが数学研究にどのような影響を与えるかについて詳しく語る。Leanは伝統的な証明手法と異なり、形式的な論理構造を生成することで証明の信頼性を高め、共同研究を容易にする。しかし、その利用には専門的知識が必要で、全ての問題を扱えるわけではない。AIとの連携可能性についても言及し、数学の未来像を描いている。

陶哲轩三小时超长访谈：我们如何解决难题？AI将如何重塑数学？ 在最近的一次访谈中，菲尔兹奖得主、加州大学洛杉矶分校教授陶哲轩（Terence Tao）分享了他在解决数学难题时的经验以及对AI未来在数学领域应用的看法。 陶哲轩谈计算辅助证明 陶哲轩指出，虽然像Python和C这样的传统编程语言主要用于执行计算任务，但Lean不仅仅是一个执行代码的工具，它还能“生成证明”。例如，你使用Python计算3+4的结果是7，而Lean不仅告诉你结果，还会生成详细的证明流程，包括每个推理步骤。 因此，Lean处理的对象比普通语句更为复杂：它能够创建带有完整注释的逻辑结构。每行代码实质上是将已有的数学句子拼接起来，形成新的结论。 陶哲轩讨论Lean的设计理念 陶哲轩提到，这种思维方式其实并不新鲜，这类系统被称为“证明助手”（proof assistants），为构建复杂的数学证明提供了形式化的语言。如果你信任Lean的编译器，那么它输出的每一个证明都可以被视为100%正确的“证实证书”。此外，Lean的编译器非常小巧且有多个版本可选。 Lean的设计吸收了许多数学家的意见，因此它的语法尽可能模仿“数学证明的语言”。你在Lean中引入变量、使用反证法等，都可以用标准的方式来表达。尽管如此，每行代码都能与证明中的步骤一一对应，但也存在一定的差异。 Lean更像是一种“高级语言”，能够将高度抽象的数学问题分解成模块化的问题，使得每个推理步骤都明确具体。 数学中的协作与问题解决 这种形式化方法并不会破坏数学家的“感觉”（vibe）。相反，它在解决特定问题时表现出色。陶哲轩以他的研究为例，描述了传统纸质证明与形式化证明之间的区别。在传统的研究中，每次修改一个参数，你都需要从头检查整篇证明是否有误。但在Lean中，你可以即时反馈，逐步修正每个步骤，确保整个证明的正确性。 数学研究的新方向 Lean及其类似平台如GitHub，可以将实验数学的规范扩展到前所未有的程度。现在的数学依然以理论为主导，实验仅占一小部分，但Lean使得实验过程更加严谨。例如，他们正在开展“等式理论项目”（Equational Theories Project），生成了约2200万个小问题，并通过配对算法逐步解决这些小问题，形成最终的证明图谱。 这在过去是不可能实现的，因为当时只能手动处理少量的关系。有了Lean，他们可以在不同层次上自由扩展，确保每一步推理都可信，而不必依赖人工逐个验证数百万个命题。 陶哲轩谈数学研究中的评价体系 尽管学术界已经有一些传统的评价体系，如文献数量，但陶哲轩认为这种新的标志虽然有缺陷，但更趋向准确。他们这次采用了“自我报告”的方式，建立了一套标准分类，描述协作者的贡献：思想、验证、资源、编码等，总计十二项。 数学界的协作模式 陶哲轩还谈到数学界的合作模式是否可以根据合作者的专业水平来组织。他表示，目前还没有一种有效的方法按专业水平来组织协作。未来如果加入AI协助者，或许可以像Elo等级评分那样，根据每个人的贡献进行评分，增加游戏元素。 十年来，陶哲轩参与过一些“众包研究项目”（Polymath projects），虽然人数多，但实际上并没有很好地分配任务，导致了相当大的混乱。相比之下，Lean的形式化证明方式更能够促进有效的分工和协作。例如，他们在DHJ Polymath项目中创造了一个人工角色，模拟了20世纪著名数学家团体（布尔巴基学派）的工作模式，提高了项目的效率。 总结 陶哲轩的访谈揭示了Lean在数学领域的巨大潜力，不仅帮助数学家生成严谨的证明，还能促进高效的团队协作。他相信，在AI技术的辅助下，数学研究将进入一个更加精确和高效的时代。