--- id: "r913hk9CYw0" title: "AI 写代码，谁来验证？" channel: "Gradient Flow" host: ["Ben Lorica"] guests: ["Leo de Moura"] date: "2026-10-29" updated: "2026-11-01" duration: "54:00" duration_seconds: 3240 source_type: "youtube" youtube: "https://www.youtube.com/watch?v=r913hk9CYw0" canonical: "https://pod-exp.pages.dev/r913hk9CYw0/" transcript_jsonl: "https://pod-exp.pages.dev/r913hk9CYw0/transcript.jsonl" language: "zh-CN" translation: true translated_from: "en" timestamp_precision: "block" topics: ["AI 编程","AI 安全","数学与科学"] series: ["AI 与软件"] --- # AI 写代码，谁来验证？ > 中文译文，由英文原音字幕翻译整理，不是官方逐字稿；引用原话请核对英文原视频。说话人标签由整理者依上下文标注，带「未确认 / 未标注 / 不确定」等字样的标签不可靠。时间戳一般为块级（所在时间块的起点），不是逐句时间；正文自带 [hh:mm:ss] 的段落除外。 **内容提要：** Ben Lorica 与 Lean 创造者 Leo de Moura 讨论 AI 生成代码为何需要形式化验证，以及 Lean 如何让代码性质和数学证明接受机器检查。两人谈到自动形式化、Rust 程序建模、Mathlib 的规模增长、AI 发现软件与数学证明中的问题，以及规格说明、模型与可信内核各自的作用。他们也讨论形式化验证如何进入长时间运行的 AI 智能体、沙箱和安全策略，并展望数学、物理、金融、化学、会计与法律中的应用。随着代码生成成本下降，人类工程师的重心可能转向定义需求、建立精确模型并判断验证声明是否有意义。 ## [0:07] 介绍 Leo de Moura 与 Lean · YouTube **Ben Lorica：** 今天我们请到了一位特别嘉宾：Leo de Moura，AWS 自动推理团队的副总裁兼杰出科学家。更重要的是，他还是 Lean 的创造者，Lean 可以在 lean-lang.org 找到。Lean 既是一门编程语言，也是一套定理证明器；Leo 还是 Lean Focused Research Organization 的首席架构师。介绍有点长，Leo，欢迎来到节目。 **Leo de Moura：** 谢谢，谢谢。我很高兴能来。 ## [0:46] 为什么 AI 生成的代码需要形式化验证 · YouTube **Ben Lorica：** 这次谈话的核心观点是：我们进入了一个“生成变容易”的时代。用“氛围编程”的人都知道，生成未必便宜，但确实越来越容易。因此，关键挑战之一就是验证。Lean 通常被视为首选工具；我想在未来一年里，AI 领域谈到形式化验证时，越来越多人会提起它。先从基础问题开始：对于熟悉代码审查、质量保证和测试的听众来说，形式化验证增加了什么？ **Leo de Moura：** Lean 既是一门编程语言，也是一套证明辅助工具。你可以一边写代码，一边陈述代码应该具备哪些性质；也可以提出尚未解决的数学猜想，并为这些命题给出证明。这里的证明不是非正式的说明，而是用 Lean 语言写成的，更重要的是，它会经过机器检查。 Lean 本身是一大套代码，但要信任 Lean 给出的结果，你只需要信任它的内核，也就是实际检查证明的那一部分。它当然也有各种编程语言工具：LSP 服务器、智能提示、代码生成、自动补全等；但这些都不是证明检查这一步的关键。 而且，Lean 不只有一个检查器。Lean 的证明可以看成可操作、可转换的数据。你可以导出证明，再交给不同的检查器验证。现在已有两个经过验证的检查器，第三个也快来了。机器可检查的证明，能缓解信任瓶颈，不只是人与人之间的信任问题，也包括人和 AI 之间的信任。 比如，你想生成一段满足特定性质的代码。过去，你会先实现软件，也许再搭一套测试设施，确保这些性质成立。如今属性测试很流行，你会编写测试框架。测试对找出 bug 很有用，但不能证明没有 bug。 **Ben Lorica：** 你甚至可以另外安排一个团队来做测试。 **Leo de Moura：** 对，对。现在有了形式化验证，你可以从性质出发。比如先把性质写清楚，再让 AI 实现满足这些性质的代码，并证明给你看：它会实现代码、写出 Lean 证明，而且这个证明能通过机器检查。现在的 AI 已经完全能做到这一点。 ## [4:47] 为什么 AI 生成的代码需要形式化验证（续） · YouTube **Leo de Moura：** 举个例子，我的同事兼朋友 Kim Morrison 做过一项实验：她把 Zlib 这个压缩库移植到了 Lean。她还写了一条性质：如果把数据压缩后再解压，就应该得到原数据，不能有任何丢失或损坏；无论采用什么压缩级别，这条性质都应该成立。 **Ben Lorica：** 对。 **Leo de Moura：** 正是如此。定理说的就是这件事，它是其中一个参数对应的性质。 **Ben Lorica：** Leo，我给听众确认一下：她用 Lean 写了这个压缩工具。 **Leo de Moura：** 是的。 ## [5:35] 验证 Rust、自动形式化与 Mathlib 扩展 · YouTube **Ben Lorica：** 所以 Lean 在这里充当形式化验证工具。如果我是开发者，想用 Lean 验证软件，但软件本身是用 Rust 写的，Lean 还能帮上忙吗？ **Leo de Moura：** 可以，有两种方式。第一种是用 IMES。它能让你用 Lean 验证 Rust 代码。微软的 SyncCrypt 团队就用它验证他们的密码学库。你可以从这里开始。另一种方式是让 AI 在 Lean 里为你的代码建立模型。AI 会读你的代码——不管它是用什么语言写的。 **Ben Lorica：** 任何语言都行？ **Leo de Moura：** 对，任何语言。要是去年有人这么跟我说，我会觉得这简直是科幻。这件事有个名字，至少在数学领域叫“自动形式化”（autoformalization）。 **Ben Lorica：** 对听众来说，数学论文由文字、数学符号、定理、引理等等组成。Leo 刚才说的自动形式化，大概一年前还不是现实，现在已经做得到。 **Leo de Moura：** 完全正确。对 Lean 来说，这带来的变化是可扩展性。比如，人类为 Lean 搭建的数学库 Mathlib 已经有 250 万行代码。 **Ben Lorica：** 太惊人了。听众可以想象一下：假设几乎所有数学书籍和论文都像我们说的那样，通过自动形式化转换成 Lean，那就意味着我们都能访问它们。 **Leo de Moura：** 没错。再看看现在 Lean 证明的发展速度：已经发表的证明有 5,000 万行。Mathlib 是人类花了十年，从零写到 250 万行的。现在有人开始用 AI 写证明，有一个证明就有 5,000 万行。最近由 Entropic AI 写出的那个定理证明有 1,300 万行。 **Ben Lorica：** 但正如你指出的，在软件领域也有类似的情况，适用于每一种编程语言。 **Leo de Moura：** 是的。 **Ben Lorica：** 现在前沿模型已经能够把用任何编程语言写的程序翻译成 Lean，再利用 Lean 的基础设施来验证。 **Leo de Moura：** 是的。 ## [9:22] AI 生成的形式化模型可信吗？ · YouTube **Leo de Moura：** 不过有一点很重要：如果你用 AI 在 Lean 里为程序建立模型，关键问题是这个模型是否忠实反映了你的代码。现在有人用差分测试：同时运行 Lean 模型和原程序，看看它们是否计算出相同结果，从而找出差异。人们确实已经发现了一些 bug。 **Ben Lorica：** 所以你的意思是，这个模型是否准确，责任仍然在你。 **Leo de Moura：** 对，完全正确。 **Ben Lorica：** 我看到这种做法正逐步发生。几周前，Claude Code 的主要开发者 Boris 发了一个视频：他只是让 Claude“用 Lean 检查 Claude Code 有没有 bug”。Claude 开始建模、发现 bug、尝试证明性质；发现有些性质证不出来后，它找到 bug、提交了 PR，Boris 把它们合并了。那些都是真实的 bug，Boris 还说自己根本不会 Lean。 **Leo de Moura：** 对。不过这种办法用于找 bug，效果还算不错；但如果下一步你要说“现在可以确认没有 bug”，就得检查模型，并确认它确实准确地代表了你的代码，而且还要让模型和代码保持同步。你可以借助 AI 证明一些性质。如果你的代码是 Rust 写的，也可以尝试证明模型忠实地反映了代码。 接下来几个月、几年里，我们预计大家会更关注规格、模型，以及希望软件具备的性质。其实，数学领域最近也发生着同样的事，比如 Navier–Stokes 方程的证明。 ## [11:29] Navier–Stokes、证明不匹配与可编辑证明 · YouTube **Ben Lorica：** 也许自动形式化这一步——把问题的原始表述翻译过来——不够忠实，或者有别的问题。后来发现，他们实际上证明了结果，只是还需要人来察觉这个问题并做一些细微调整，对吧？ **Leo de Moura：** 对。Navier–Stokes 这个结果非常重要，有一点必须讲清楚：OpenAI 开始训练模型之前，Navier–Stokes 问题的表述就已经由人精心整理好，并以 Lean 形式写出，也经过专家校订。所以问题陈述是否被正确形式化，并没有什么疑问。 结果之所以有争议，是因为 OpenAI 同时给出了自然语言写成的非形式证明，以及 Lean 写成的形式证明，而两者之间存在不匹配。 **Ben Lorica：** 我想差异在于，你假设的是四阶还是五阶导数？ **Leo de Moura：** 对，没错。 **Ben Lorica：** 这对数学家来说很重要。可以看出两者的差别有多细微。Boris…… **Leo de Moura：** 我来补充一个要点。有个工具我觉得值得介绍给听众，叫做 Vessel Blueprint。它适合用来展示 Lean 的结果，把自然语言和 Lean 放在一起，形式有点像文学式编程。你可以把自然语言和 Lean 代码结合起来，让两种表述彼此对齐。 我们很有把握地认为，如果 AI 当时使用 Vessel Blueprint，这种不匹配就不会发生。这是改进工具链的问题。另一个误解是，有人以为 Lean 证明是静态对象。其实证明也能像代码一样重构、简化。比如，有团队已经把那个 Fermat 最后定理的证明缩短了一半。 **Ben Lorica：** 而且这一点对人写的证明也成立。 **Leo de Moura：** 是的，没错。但这里你还有机器检查。你找到一个证明，Lean 会告诉你它确实成立。你可以操作证明，也可以让 AI 帮你理解证明、导航证明，还可以用 Lean Blueprints 把证明和非形式表述对齐。这些都做得到。我在社交媒体上常看到人们忽略这一点：形式证明不是静态对象，你可以操作它、简化它、探查它、向它提问，也可以和它交互。 ## [15:11] 形式化验证与传统软件测试 · YouTube **Ben Lorica：** 我想把这个重点再说清楚，让不熟悉这些概念的听众也能明白：形式化验证和普通的质量保证、测试有什么区别？如果 AI 已经能替我写一大堆测试，覆盖各种边界情况，测试覆盖率也很高，为什么还需要形式化验证？ **Leo de Moura：** 测试很擅长证明 bug 的存在，却不能证明 bug 不存在。就算你用 AI 生成大量测试用例，拿来找软件漏洞的 AI 也可能比你的 AI 更聪明。两种技术并不冲突，而是互相补充。 我常看到一种错误做法：试图证明某个可能本身就有 bug 的东西。无论你投入多少资源、烧掉多少 token，都不可能证明一个错误命题。测试始终是很好的起点，它能提升你的信心和理解；之后再做证明。测试只检查你试过的那些输入，而证明是针对任意输入，证明程序对所有可能输入都成立。这是“对所有”，而不是“对其中一些”。 **Ben Lorica：** 老实说，软件工程可能落后于航空航天等其他工程学科。我不太确定，但其他领域在验证方面的纪律可能更严格，毕竟出错的后果严重得多。我觉得这是个很好的观点。 ## [17:44] AI 如何让形式化验证变得实用 · YouTube **Leo de Moura：** 我觉得现在的情况是，写代码的人越来越多，代码也越来越容易写；与此同时，验证也迎来了自己的“ImageNet 时刻”。 **Ben Lorica：** Leo，你们做 Lean 已经有一段时间了，它也一直很稳健。所以这次真正的转变，主要是自动形式化，以及前沿模型能够写 Lean，对吗？你刚才也说过，一些行业过去就用形式化验证；如果它这么好，为什么以前不普及？因为手工证明太耗时了。AI 大幅降低了验证代码的成本，而且形式化证明完成后还有额外好处：你可以让 AI 修改、优化代码，但要求它始终证明代码正确。证明就像护栏，AI 可以尝试大胆的优化，即便你未必完全理解它是怎么做到的；但证明会告诉你，程序依然计算同样的东西，而且效率更高。 ## [19:24] 需求缺口、模型缺口与证明检查器的可信度 · YouTube **Ben Lorica：** 按我们刚才的讨论，软件工程师以后可能不再主要写代码，甚至验证也许能部分自动化，真正的重点会变成需求：把你想要的东西描述清楚。这里大概有两类缺口。第一是需求缺口：你想要什么，和你能写下来的要求之间有没有差别？第二是模型缺口：你测试时的条件，是否能代表生产环境？也就是说，测试场景会不会过于理想化？ 还有一点是对 Lean 内核的信任。随着 Lean 越来越普及，你依赖的不只是 Lean 验证了你的代码，还依赖代码所用到的所有库。总的来说，有三件事：需求、模型，以及 Lean 内核。 **Leo de Moura：** 实际上我们有多个内核。你不必相信我们，也可以使用其他团队实现的内核。 **Ben Lorica：** 我觉得这方面我们做得不错。现在甚至有一个内核竞技场，收集各种内核。 **Leo de Moura：** 对，它们会互相比速度。要是结果错了、内核有 bug，就会受到惩罚，所有人都能看到。网站叫 arena.lang.org。具体来说，我不能保证每一个都是开源的，因为我没有用过全部；我用的主要几个都是开源的。 **Ben Lorica：** 它们必须用 Lean 写吗？ **Leo de Moura：** 不必。某些是 Rust 写的，有一个用 C，还有一个用 Haskell。甚至有一个是用 TeX 写的。TeX 常用来排版数学和计算机科学论文，不过它也是一门完整的编程语言。我的同事 Kim Morrison 就用 TeX 实现了一个检查器内核，正是为了展示内核可以用很多不同的编程语言实现。还有一个是用 Coq 实现的。 ## [22:36] 软件工程的未来：从代码转向规格说明 · YouTube **Ben Lorica：** 那么软件工程师的教育和训练也会改变，对吧？以前明星程序员是特别会写代码的人；以后可能更重要的是能把复杂系统的需求讲清楚，比如要用 Kafka、Spark 之类的技术。 **Leo de Moura：** 我认为大家会更重视编写形式化规格、定义性质和需求。这很关键，因为很多时候我们甚至不知道软件究竟应该做什么。模型也会有不精确的地方，有时是因为人们自己都不完全清楚想要什么。 **Ben Lorica：** 而且应用往往很复杂，会和数据库、分布式系统交互。 **Leo de Moura：** 没错。过去设计数据库或架构时，人们会写自然语言文档，有时会用某种规格说明，也会画架构图。但那些文档是非形式的，你无法自动检查实际实现是否和文档一致，只能让人去读代码、维护两边的同步。这很麻烦：文档改了，还要确认实现是否仍然匹配。我们都见过代码注释和代码本身已经脱节的情况。 如果所有内容都是形式化的，就能用工具检查设计文档是否与实现匹配，这是向前迈进了一步。当然，文档一开始肯定会不精确：客户想要 X，你写下的规格可能是 X′。你会持续打磨、细化，逐渐弄清什么才是事实基准。随着系统和真实世界互动，你再回头完善规格；与此同时，工具会检查代码是否符合更新后的模型。 人们常说“代码已经验证过了”，但这句话有很多前提：你写下的性质真的是你想要的吗？你得不断打磨规格，让它更精确。有些软件还会建模攻击者，描述他们可能如何攻击系统。所以这些需求文档、产品需求文档（PRD）会成为源代码管理系统里持续跟踪的内容。 **Ben Lorica：** 这样一来，随着你不断学到新东西，每个版本都要验证；甚至每次都可能直接让 AI 从头重写代码，为什么还要保存旧代码？真正珍贵的东西就变成规格本身，而它最终仍由人负责维护。 ## [26:37] 软件工程的未来：从代码转向规格说明（续） · YouTube **Leo de Moura：** 完全正确。 **Ben Lorica：** 也就是说，再加上 AI 和 Lean 这样的工具，计算机科学整个课程体系是不是都得重做？ **Leo de Moura：** 不用彻底重做，但肯定会调整。我见过很多学院和大学，形式化验证甚至不是必修课，只算一种好奇心；以前它太贵，工业界用得不多。今后对形式化验证的关注会增加。不过学习底层知识仍然有价值：总会有人学习汇编、低级语言、如何写代码和检查代码，以及如何在非常底层设计系统。这些都会继续存在。 **Ben Lorica：** 但变化肯定很大。在这样的世界里，一个工程师即使不擅长实际写代码，也可能效率很高、很受需要。 **Leo de Moura：** 是的，这种情况会发生。不过你写的仍然可以算代码：写形式化模型也可以视为编程，只是你在更高层次上工作。 ## [28:30] 经验证的软件栈，以及如何评估验证声明 · YouTube **Ben Lorica：** 你写过一个我很喜欢的说法——“经验证的软件栈”（verified stack）。如果确实是你提出的，能解释一下它的意思吗？ **Leo de Moura：** 经验证的软件栈说的是关键软件栈。有些代码出了 bug 不算太严重，比如电子游戏有 bug 会让用户恼火，但不会引发世界危机。关键软件栈则包括操作系统、编译器和 TCP/IP 通信层。如果这些组件都有模型和规格说明就好了。我们可以让专家编写、讨论这些规格，再开始验证，确认实际代码和规格相符。我觉得这是未来很值得投入的方向。 **Ben Lorica：** 假设你是一家《财富》500 强公司的 CTO，我是供应商，跟你说“请相信我们的软件，我们已经做过形式化验证”。你会问哪些关键问题，确认我不是在胡说？ **Leo de Moura：** 先给我看规格说明和性质：你到底验证了什么？形式化验证可能只证明了某个性质为真，但如果你没提出有意义的性质，就没有做出什么主张。我们应该警惕“代码已经形式化验证”这种说法，并追问：验证了哪些性质？是依据什么规格验证的？ **Ben Lorica：** 还要问用了哪种证明检查器内核。 **Leo de Moura：** 对，这也很重要。另一个问题是可信代码基的大小。Lean 和 Rocq、Isabelle 等证明助手，有些工具的可信代码基很大；而可信代码基应该尽可能小。 **Ben Lorica：** 当然，如果还能说明软件曾在类似、真实的环境里运行过，也会让验证声明更有说服力。 ## [31:53] 验证 AI 智能体、沙箱与安全策略 · YouTube **Ben Lorica：** 我们谈软件时，好像它都是静态的东西；但现在有了智能体软件，而且开始出现长时间运行的智能体。验证在智能体世界里意味着什么？ **Leo de Moura：** 首先要给这些智能体加护栏，最好有可靠的沙箱。过去几周我们看到不少人声称智能体能逃出沙箱。作为经验证软件栈的一部分，我们需要可靠的沙箱、写得好的规格，以及实现符合规格的证明。 我们还希望为智能体行为制定策略，并确保执行这些策略的代码经过形式化验证。想象一下，你花很多时间规定智能体能做什么、不能做什么，结果执行策略的代码自己却有 bug。那就麻烦了。可如果负责形式化验证的又是另一个智能体呢？ **Ben Lorica：** 这就出现了好几层信任。 **Leo de Moura：** 对。有些人会问：智能体能不能利用 Lean 内核或内核运行环境中的漏洞？这些问题都合理。这也是我们有多个内核的原因。即使智能体找到漏洞，想骗你相信一个并不成立的证明，证明证书也必须被多个已经实现并验证过的内核接受。 **Ben Lorica：** 是的，完全正确。这很严肃，因为这些智能体特别擅长发现漏洞。你接触过用这些方法专门验证智能体的人吗？ **Leo de Moura：** 在 AWS，我们的 Agent Core Dogwoods 都在用 Lean。外面也有一些例子，比如我刚才说的，让 Claude 用 Lean 检查 Claude Code 并找出 bug。我们会看到越来越多类似项目。形式化验证和 Lean 这类工具的一个主要障碍，是学习曲线陡：你得先学 Lean、自己写模型，开始成本太高。AI 可以降低启动成本，让你几乎立刻看到价值。Boris 的视频就是这样，他只是让 Claude 尝试用 Lean 验证 Claude Code，马上就有收获。 一旦你立刻看到价值，就会愿意投入更多时间学习这项技术，然后开始想：也许我应该为代码写下形式化性质；也许我不必自己写模型，但至少应该学会读 Lean 模型，判断 AI 智能体建立的模型是否准确，并和智能体讨论模型的准确性。 ## [35:53] 验证 AI 智能体、沙箱与安全策略（续） · YouTube **Ben Lorica：** 所以，像这样的系统是为长时间运行的智能体准备的；它们可能连续几天探索、做研究、彼此协作。我们刚才谈到，其中一个挑战显然是把需求说清楚。对于一个像人一样探索各种方向、仿佛拥有无限资源、能走遍世界、什么都能做的智能体，怎么定义需求？ **Leo de Moura：** 这确实是个大挑战。不过 AI 可以帮你起步，先写出第一个模型，让你看到形式化的方式。智能体系统是复杂系统，包含多个相互作用的部分，也有不同部分之间的通信协议。你希望这些协议是正确、准确的。AI 智能体可以帮你建立形式模型的初稿，然后你再从那里不断迭代。 ## [37:37] Mathlib、AI 辅助数学与协作证明 · YouTube **Ben Lorica：** 所以我们刚才谈的所有事情，起点都是编程和数学。最近几周数学界的变化很大，甚至有菲尔兹奖得主都激动得哭了。整个领域可以说受到了巨大冲击。我有数学博士学位，以前也在这个领域，不过我并不算优秀。也许现在有了无限算力，我就能行了。Lean 和 Mathlib 的结合，似乎让数学比编程更适合这项技术，是我想错了吗？ **Leo de Moura：** 不，不是。Mathlib 是数学家用数学家的背景构建的，因此里面的定义很精确。 **Ben Lorica：** 所以他们多年前开始做这件事时，可能已经预见到，总有一天规模会扩大？当时他们像在没人注意的矿井里辛苦劳作，但一旦扩展起来…… **Leo de Moura：** 我觉得当初没人预料到 AI 会变得这么强。不过对数学界来说，一大进展是他们发现 Lean 能帮助大家大规模协作。 **Ben Lorica：** 比如 2024 年 Terence Tao 有个项目，把一个项目拆成许多小部分。他像个架构师，负责搭建结构。 **Leo de Moura：** 对。 **Ben Lorica：** 他不可能亲自验证每一部分，于是许多他没见过的人来补上证明缺口，给他提交证明。他不必亲自检查每个证明是否正确；这些人就像在他的大设计里填补空白。大家都觉得很棒。我记得他跟我说，自己从没想过会和业余爱好者一起工作，他一直只和专业人士合作。 **Leo de Moura：** 这又回到了你一开始说的信任。 **Ben Lorica：** 对。数学和大多数科学都建立在信任上。数学家证明一个定理时，会引用许多过去的定理，有些可能是五十年前的。即使自己不会证明那些定理，也会相信它们是正确的。这就是他们用 Mathlib 做的事情。 **Leo de Moura：** 没错。当时我记得 Terence Tao 做报告时说过，有一天 AI 智能体会参与进来，填补这些空白。但我想我们谁都没料到它来得这么快。几个月前如果我告诉任何 Lean 开发者或 Lean 数学库的维护者，AI 会这么强，他们都不会相信。 ## [41:24] AI 与形式化验证能改变理论物理吗？ · YouTube **Leo de Moura：** 现在 AI 已经能自动形式化，把数学翻译成 Lean。 **Ben Lorica：** 我想这还会继续发展。Leo，那为什么不能把同样的事用在理论物理上？ **Leo de Moura：** Lean 有一个叫 PhysLib 的物理学库，大家一直在手动形式化物理学。现在我觉得他们很可能已经转向用 AI 了，所有人都在转向 AI。甚至我们 Lean 开发者也在用 AI 实现 Lean。一开始是发现 AI 很擅长找出并定位 bug，接着发现它很会修补库里的 bug，然后发现 AI 能写代码，而且写得比我们还好。 **Ben Lorica：** 理论物理被颠覆到像数学那样的程度，大概要多久？ **Leo de Moura：** 他们已经有了第一个成果。几个月前，有人尝试形式化一篇重要物理学论文的结果时，发现了一个 bug。物理学的挑战在于，我们建立的是现实世界的模型，这些模型总是不精确，毕竟它们只是对现实的建模。 **Ben Lorica：** 不过有些理论一开始就是理论性的。比如弦理论从来没有得到实验验证。理论物理学家即使还没有实验，也能继续研究、发表论文；这些人也可能很快受到冲击。 **Leo de Moura：** 是的，他们现在可以用 Lean 写出非常精确的数学模型，这完全做得到。 ## [43:35] 数学家的未来、AI 算力与科学发现 · YouTube **Ben Lorica：** 自从 Navier–Stokes 事件以来，OpenAI 又发表了不少结果。你有从数学界的朋友那里听到什么吗？他们会不会问你：“Leo，你对我们的领域做了什么？” **Leo de Moura：** 大家感受很复杂。有些人特别兴奋，觉得我们将能攻克超出想象的问题；也有人担心未来会怎样，比如学生会问“我该怎么办？”就像软件开发一样，开发者还会存在，只是工作会变；数学领域也会如此。 **Ben Lorica：** 这确实是重大变革。有人生气，有人兴奋，有人害怕。不过我希望它会带来好的变化。过去在数学领域，你大致知道谁是最优秀的数学家，于是就去和他们交流。他们知道得比你多，反应更快，能证明更难的定理。原始智商似乎决定一切，这也是我离开这个领域的原因：我比不过这些人。未来菲尔兹奖得主会因此改变吗？也许胜出的是聪明但不是天才级别、却能获得更多算力的人。在软件领域也是一样，有更多算力可能就能做更多事。 **Leo de Moura：** 是的，你说的确实有道理。我觉得自己的一个优势是能忍受痛苦，写软件很痛苦。 **Ben Lorica：** 证明定理也很痛苦。 **Leo de Moura：** 对。我把这种痛苦消除了，但这也让我的“超能力”不像以前那么有用了。不过我们会推进得更快、做成更多事。我认为这是好事。未来拥有不同技能的人，可能更有价值，也可能更善于利用这项技术。我们会遇到 token 获取的问题，但科学领域一直有类似情况，比如詹姆斯·韦伯太空望远镜。你可以提交申请，获得望远镜的使用时间，然后排队。未来数学领域也可能一样：一个大型项目要花很多钱，你提交申请，或许得到资助，就能访问极其强大的模型。 ## [47:35] 数学家的未来、AI 算力与科学发现（续） · YouTube **Ben Lorica：** 除非出现突破，让模型变得更高效。就像国际象棋那样。Leo，我没太跟进这方面：在笔记本电脑上运行的国际象棋程序，和在集群上运行的程序有什么区别？后者会给我更好的答案吗？ **Leo de Moura：** 我不太清楚，我不是棋手。不过我的印象是，现在在电脑上运行的棋类程序已经非常厉害了。希望你说得对，未来我们也会有能在自己电脑上运行的模型。但这里的利害关系很大，所以我相信超级计算机仍然会存在，就像詹姆斯·韦伯太空望远镜一样。我们能买一架很好的望远镜放在家里，可韦伯望远镜好得多，也贵得多。 **Ben Lorica：** 所以展望未来，参加数学学术会议时，以前最受关注的是最聪明的人、菲尔兹奖得主；现在可能变成拥有计算集群的人了。 **Leo de Moura：** 大家当然总想和拥有集群的人聊聊。不过拥有集群的人未必就是提出想法的人，就像詹姆斯·韦伯望远镜可能由一个委员会管理。科学家一直都在提交申请、争取使用机会，我觉得未来数学领域也会这样。 ## [49:16] 超越数学：金融、化学、会计与法律 · YouTube **Ben Lorica：** 我们从编程谈起，然后谈到数学，也聊了理论物理。还有哪些不太受关注的领域，正在发生类似 Mathlib 的事情？ **Leo de Moura：** 我看到很多人对金融感兴趣。金融有很多算法，也有人想在这个领域应用形式化验证、建立更精确的模型。 **Ben Lorica：** 但数学和理论物理里有证明。金融算法这边呢？ **Leo de Moura：** 金融里有很多数学。确实有人对这个方向很兴奋。不过这方面的人通常不公开工作，比较保密。 **Ben Lorica：** 那要怎么建出类似 Mathlib 的东西？ **Leo de Moura：** 我见过一些人愿意公开追踪算法，但他们大概不想把所有东西都泄露。与此同时，也有金融数学背景的人希望把成果形式化并公开。你说得对，仍然会有人把自己的独门诀窍保密。 **Ben Lorica：** 除了金融，还有什么？ **Leo de Moura：** 我觉得有人在尝试建立化学、生物学的库，任何领域都有可能。 **Ben Lorica：** 你刚才提到的这些领域，进展分别如何？ **Leo de Moura：** 数学库显然遥遥领先，因为数学是精确的。物理学库和计算机科学库正在努力追赶 Mathlib。金融和化学也有新的项目。不过你看看各个领域的论文，就能从其中数学部分的精确程度和严谨程度，看出要建立形式化库会有多难。 **Ben Lorica：** 化学还分理论化学和计算化学，对吧？既然有了自动形式化，决定朝这个方向走的领域是不是会更快追上？Mathlib 的人多年来默默耕耘，但自动形式化出现后，进展一下子就起来了。 **Leo de Moura：** 完全正确。 **Ben Lorica：** 那非科学领域也会出现类似情况吗？比如会计：有公认会计原则，也有税法，在很多方面它们像定理。但我和一些会计师聊过，问题在于某笔资金究竟该记在这里、那里还是另一个地方，有时是主观判断。 **Leo de Moura：** 对。我也见过有人尝试把法律形式化。 **Ben Lorica：** 我也和人聊过这个问题。不过法律的问题在于，我们之所以互相起诉，就是因为彼此意见不一致。 ## [53:16] 超越数学：金融、化学、会计与法律（续） · YouTube **Leo de Moura：** 没错。不过法律也有一些部分适合形式化。我有个熟人是律师。比如民事诉讼程序的规则就非常…… **Ben Lorica：** 形式化？它几乎像一个程序。 **Leo de Moura：** 对，法律里有些部分可以形式化。 **Ben Lorica：** 明白了。那就谢谢你，Leo。 **Leo de Moura：** 非常感谢。