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