为数学担任裁判的编程语言

我认为那个反证是对坍缩猜想的反证。它用 Lean 证明来应对，并且声称它已被 Lean 自带的官方内核接受。

The disproof, I think, was a disproof of the collapse conjecture. It was met with a Lean proof, and the claim is it's accepted by the official kernel that comes with Lean.

哇，我是说，这太可怕了。

Wow, I mean, this is horrible.

我们强烈认为这是由 AI 构建的。它利用了官方内核中的一个漏洞和另一个地方完全不同的漏洞。我们没有耐心做这种底层实现，但 AI 有耐心做这种事。我认为这将改变游戏规则。

We strongly believe it was built by AI. It exploits one bug in the official kernel and a completely different bug in another. We don't have patience for doing this kind of low-level implementation, but AI has the patience for doing that. I think this is going to be a game changer.

走向更好的模型。它们不断做出更惊人的事情，但同时也一直做蠢事。Boris Alexi 向 Lean 提交了一个证明，120 万行 Lean 代码，形式化证明。没人想逐行检查这个证明。

Going to better models. They keep doing more amazing things, but they keep doing stupid things at the same time. Boris Alexi submits a proof to Lean, 1.2 million lines of Lean, the formal proof. Nobody wants to check the proof line by line.

我是 Leo。我是 Lean 的创造者，首席架构师，也是 Lean 基金会（Lean 背后的非营利组织）的联合创始人。我还是 AWS 的高级首席科学家。

I'm Leo. I'm the creator of Lean, chief architect and co-founder of the Lean Foundation, a nonprofit behind Lean. I am also a senior principal scientist at AWS.

在某个时候，你实际上圈定了系统的核心部分，你说：‘好了，这部分锁定了。我控制这里。’这里有一种有趣的张力，不是吗？你知道，很多创造力有时发生在社区里。所以有不同层次的适应。比如核心部分——你知道，例如在《雷神之锤 3》这个射击游戏里，有这些弹跳漏洞，整个社区围绕速通和弹跳漏洞之类的东西发展起来。类似地，现在在 Lean 里，有核心系统，有 Mathlib，还有整个社区在不同方向上发挥创造力。核心部分适应得慢得多，而且由你控制。但你怎么看待这一点？你是否觉得你确实控制着 Lean 的某个方面，还是说它有自己的生命？

At some point you actually ring-fenced off a core part of the system and you said, 'Okay, this is locked. I'm in control of this.' And there's an interesting tension, isn't there, that a lot of creativity sometimes happens in the community. So there's different levels of adaptation. So there's the core thing—you know, for example in Quake 3, the shooter, there are these bounce bugs and an entire community evolved around speedrunning and bounce bugs and stuff like that. And similarly in Lean now, there's the core system and there's Mathlib and there's this entire community being creative in different directions. The core thing adapts much slower and it's controlled by yourself. But how do you think about that? Do you kind of feel that you do control an aspect of Lean or does it have a life of its own?

好的。实际上，这是个很好的问题。这是个很好的问题。不，我不再控制核心系统了。我的意思是，我们有基金会作为非营利组织。我们有 20 个人在那里。他们每个人都拥有——我喜欢这个模式。核心的开发者们，他们拥有系统的某些部分；这是他们的责任。他们有所有权。是否接受外部 PR 请求，他们是决策者。但在最初的 10 年里，基本上我拥有系统的一部分。Sebastian Ullrich，我的同事和朋友，我们一起构建了 Lean，他拥有系统的其他部分。但我们相信——我强烈相信开源的教堂模式。教堂模式就像有一个中心实体决定什么进入代码库，什么不进入。还有集市模式，那里更开放，每个人都可以贡献。与社区、Lean 社区之间有很多张力。很多人有时想为核心做贡献。为库做贡献不同于为核心系统做贡献。库——很多情况下你为二叉树构建一个库是自包含的，对吧？你在那里做的更改你可以拥有它，而不影响系统的其余部分。但核心系统，所有部分都是相互连接的。它们相互依赖。另一件事：像库，一个二叉树库可能缺少一些函数，可能缺少关于这些函数的一些定理，但它仍然有用。但一个满是漏洞的系统就不太有用了，对吧？我是说，如果有很多缺失的部分，很多崩溃，这是一个更加相互连接的系统。这就是为什么我一直坚持用教堂模式开发核心，这会产生张力。但一个很酷的事情是——它极具可扩展性，使人们能够添加自己的扩展而不改变核心。这在社区中变得非常受欢迎。我的意思是，今天很多人实现 Lean 的扩展而不与我们协调。他们实现——实际上类似于你给的例子——他们实现领域特定语言，隐藏复杂性，专注于特定领域的领域特定语言，比如分布式协议。你可以指定分布式协议。你有一种为此优化的语言，隐藏所有复杂性，这甚至不需要与我们交谈就可以完成。有时他们向我演示东西。他们从未见过我。他们实现了这个美丽的扩展，对吧？是的。我认为这很棒。这也是一个不错的副作用。

Okay. Actually, this is a great question. This is a great question. No, I don't control the core system anymore. I mean, we have the foundation as a nonprofit. We have 20 people there. Each one of them are owning—I like this model. The developers in the core, they own parts of the system; it's their responsibility. They have ownership. If they're going to take external PR requests or not, they are the decision makers. But for the first 10 years, basically I owned a bunch of the system. Sebastian Ullrich, my colleague and friend that we built Lean for together, he owned other parts of the system. But we believe—I strongly believe in the cathedral model for open source. Cathedral is like there's a central entity that decides what goes into the code base or not. There's this bazaar where it's more open, everybody can contribute. And there was a lot of tension with the community, the Lean community. Many people want sometimes to contribute to the core. Contributing to a library is different from contributing to the core system. The library—many cases you're building a library for binary trees is self-contained, right? The changes you make there you can own that without impacting the rest of the system. But the core system, all the pieces are interconnected. They depend on each other. Another thing: like a library, a binary tree library maybe missing some functions, maybe missing some theorems about these functions, but it's still useful. But a system full of holes is not very useful, right? I mean, if there are many pieces missing, many crashes, it's a more interconnected system. That's why I always insisted for the cathedral model for developing the core, and it creates tensions. But one cool thing about that—that's amazingly extensible to enable people to add their own extensions without changing the core. And this became really popular with the community. I mean, many people implement today extensions to Lean without coordinating with us. They implement—it's actually similar to the example you gave—they implement domain-specific languages that hide the complexity, focus on a domain-specific language for specific domain like distributed protocols. You can specify distributed protocols. You have a language that's optimized for that, hides all the complexity, and this can be done without even talking to us. Sometimes they demo things to me. They never met me before. They implemented this beautiful extension, right? Yeah. I think it's great. It was also a nice side effect.

你能给我举个例子吗？所以那就是——你知道，在解决抽象问题时，有时会有非常巧妙和创造性的方法。当你看到人们做的事情时，其中一些真的让你惊讶吗？

And can you give me an example of that? So that's—you know, when solving abstract problems, sometimes there are very ingenious and creative approaches. Do some of those really surprise you when you just see what people do?

是的。是的。我的意思是，我记得去年新加坡的一位教授。他和他的学生 Vulva 一起向我演示了一些东西。我说：‘为什么这些人演示这个东西？这不是 Lean。’很酷的是，最后他们说：‘不，不，这是 Lean。这是我们在 Lean 之上实现的扩展。’我真的很惊讶。那是用于软件验证的。他们有一种语言，让人们更容易验证软件，特别是命令式软件。是的，我真的被——是的，他们的演示让我大为震撼。

Yes. Yes. I mean, I remember last year a professor in Singapore. He was with his student, Vulva, and they demoed something to me. I said, 'Why are these folks demoing this stuff? This is not Lean.' And it was really cool that at the end they said, 'No, no, this is Lean. This is an extension we implemented on top of Lean.' I was really surprised. It was for software verification. They have a language that's much easier for people to verify software, especially if it's imperative software. Yeah, I was really blown—yeah, they blew me away with the demo.

这是你对——或者说，如果你想想，Lean 的声誉至关重要，因为这是将要用于验证软件和数学等的东西。所以有这一点，但它让我有点想起 MATLAB 或者 Mathematica。它有极其优化的核心库用于线性代数等，但有人可以过来，你知道，能力越大责任越大。他们可能把它搞得一团糟。所以他们可能做一些操作，它不再是向量化的，而且非常慢。也许在 Lean 中，他们可能做一些实际上影响他们所做的事情的完整性的东西。这是部分原因吗？所以你想多放一点控制进去。

Is it part of the reason that you were so kind of protective over the—or I mean, if you think about it, the reputation of Lean is paramount because this is something that is going to be used to verify software and mathematics and so on. So there's that, but it reminds me a bit of, you know, MATLAB or maybe Mathematica. It has insanely optimized core libraries for doing linear algebra and so on, but someone could come along and they, you know, with great power comes responsibility. They could just make a mess of it. So they could do some operations and it's no longer vectorized and it's really slow. And perhaps in Lean they could do something that actually affects the integrity of what they're doing. Is that part of it? So you want to put a little bit more control in.

是的，有这一点。我的意思是，也有人添加半生不熟的东西。很多人喜欢实现软件的乐趣。软件是——我喜欢看到，实际上，我的一位学术兄弟，他说软件只有在不需要工作时才有乐趣。如果它必须工作，乐趣很快就消失了。第一个问题：漏洞，就像你提到的，人们引入漏洞。第二个问题：有人提交一个未完全实现的功能。有很多漏洞。看起来能工作，但实际上不能。第三件事：人们可能锁定设计。他们添加一个功能。它是完整的，是正确的，但对我们如何优化系统施加了限制。现在我们有这个功能，它可能变得流行，并阻止我们做其他更重要的事情。因为它在那里，人们使用它，我们不能轻易移除它，我们就被困住了。另一个问题：优先考虑发展超级重要。变得混乱，实现随机功能——如果你合并随机 PR，就会发生这种情况——这真的很糟糕。它真的不能扩展。

Yeah, there is that. I mean, there's also people adding something that's half-baked. A lot of people like to have fun implementing software. Software is—I like to see, actually, one of my academic brothers, he says software is only fun if the software doesn't have to work. If it has to work, the fun disappears very quickly. And first issue: bugs, like you mentioned, people introducing bugs. Second issue: someone submits a feature that's not fully implemented. There are many holes. It looks like it works but it doesn't. Third thing: people may lock the design. They add a feature. It's complete, is correct, but put constraints on how we can optimize the system. And now we have this feature, it may become popular, and prevents us from doing other things that's more important. Because it's there, people use it, we can't easily remove it, and we're stuck with that. Another issue: it's super important to prioritize the developments. Going chaotic implementing random features—and this happens if you merge random PRs—it's really bad. It doesn't really scale.

我认为优先级排序超级重要，而这种你不断处理随机 PR 的模式行不通。这是我坚定的信念。所以你是深度优先搜索型的人，而当你构建出涉及许多其他人的成功事物时，你必须变得更像广度优先搜索，因为每天都有太多事情涌来。我记得凯文的书里有一段，说某个时候你把一大堆人踢出了 Slack 频道，你说：‘看，我现在只需要专注，’因为情况变得太荒谬了。

I think prioritization is super important, and this model where you keep budging random PRs does not work. This is a strong belief I have. So you're a depth-first search kind of guy, and when you build something successful that involves lots of other people, you have to become more like breadth-first search, because there are so many things coming in every single day. And I remember there was a bit in Kevin's book where he said at some point you just kicked a load of people off the Slack channel and you said, 'Look, I just need to focus now,' because it was getting ridiculous.

是的。哦对。是啊。是啊。我忘了这个踢人的故事了。是啊。因为在那个时候……哇。我真的很不喜欢那些不停抛想法的人。我的意思是，他们甚至……他们是在玩。这不一样。对我来说，我是在努力构建能用的东西。有些人在那个频道里玩，把想法往墙上扔，对吧？我的意思是，这很廉价。你可以把想法往墙上扔，而另一边的人得不停告诉你‘不，这不行。’这对我来说是个令人沮丧的场景。你抛出一个想法，你都没花五分钟思考。然后我找到一个漏洞，发回给你。然后你稍微润色一下，再发回来。现在找到漏洞要花 10 分钟。下一个漏洞。在半个想法上找漏洞花费的时间越来越长。对于提出想法的人来说，这很有趣，但从你的角度看就不有趣了，对吧？你现在得做你的工作，你花时间告诉人们为什么这不是个好主意，为什么现在不是做这个的时候。是的，有那么一刻，我把一些人踢了出去，只留下真正为项目做贡献的核心团队，只留下那些为项目编写有用代码的人。

Yes. Oh yes. Yeah. Yeah. I forgot about this story of the kicking. Yeah. Because at that point... Wow. I really dislike people that keep throwing ideas. I mean, they don't even... they're having fun. I mean, it's different. For me, I was trying to build something that works. Some people are there in this channel having fun, throwing ideas on the wall, right? I mean, it's cheap. You can throw ideas on the wall and the other side has to keep telling you, 'No, this doesn't work.' That's for me one frustrating scenario. You throw an idea. You didn't spend five minutes thinking about it. Then I find a hole. I send back to you. Then you polish a little bit. Send back. Now it takes 10 minutes to find the hole. The next hole. It keeps taking exponentially longer to find the holes on the half idea. For the person coming up with them, it's fun, but it's not fun from your perspective, right? You have to do your work now, you spend time telling people why this is not a good idea, why it's not the time you should do it. Yeah, there was a point, yes, I kicked out some... only the core team that was really contributing to the project, only people that were writing useful code to the project.

是啊，现在有了生成式 AI，情况肯定更糟了。我的意思是，你指出的那个现象叫做布兰多里尼定律，即驳斥一个说法所需的工作量是指数级地多于创造它。

Yeah, it must be even worse now with generative AI. I mean, so what you're pointing to there, it's called Brandolini's law, which is that it takes exponentially more work to debunk than create.

嗯，幸运的是，现在我们有 FL（Lean 专注研究组织），对吧？我有很多同事，很多人帮助我，我的生活实际上更好了。例如，这周我们有一个严重的 bug，Yin Bretoner 处理了它。不仅仅是 bug，你还得照顾社区，向社区解释，沟通。他做了所有这些。过去，要应对这么多人和噪音会是一场噩梦。而且我们在 LRO 有许多其他人帮助协调社区、沟通路线图。对我来说现在容易多了。没有 FL，我们现在无法运行 Lean 项目。

Well, fortunately, now we have the FL, right? I have many colleagues, many people that helped me, and my life is actually better now. For example, we had a serious bug this week. Yin Bretoner took care of it. It's not just the bug; you have to take care of the community, explain to the community, communicate. He did all that. In the past, it would be a nightmare to have to deal with so many people, the amount of noise. And we have many other people at the Lean Focused Research Organization (LRO) that help coordinating the community, communicating the roadmap. For me it's much easier now. Without the FL, we would not be able to run the Lean projects now.

这周的 bug 和考拉兹猜想有关吗？

Was the bug this week something to do with the collatz?

是的。

Yes.

是的，我正想问你这件事。也许你能详细说说？

Yes, I was going to ask you about that. Maybe can you set that up?

是的，是的，是的。基本上，Lean 是……我们有一个小可信内核的概念。Lean 非常庞大，有无数 bug，对吧？但要在 Lean 中信任一个结果，你信任的是内核，它要小得多，对吧？而且我们还有外部内核。事件经过……我的意思是，Yohim 做了所有挖掘工作。我很高兴他做了。事件经过大概是这样的：一周或 10 天前，一个主要的的外部检查器报告了一个 bug。我们有很多内核，其中一个主要的叫做 Noda，是用 Rust 实现的。这个 bug 立即被另一位开发者修复了。几天后，这个证明——我认为是考拉兹猜想的反证——被提交了，附带一个 Lean 证明，声称它被 Lean 自带的官方内核和主要外部内核 Noda 接受。对吧？哇。我的意思是，这太可怕了，对吧？然后我们的第一反应是 Noda 没有接受这个证明。Daniel 说：‘好吧，这些人在夸大其词。Noda 不接受。’但然后他说：‘哦，从 10 天前开始，Noda 就接受这个证明了。’然后实际上有两个漏洞利用，我们强烈认为它们是由 AI 构建的：一个在官方内核中的 bug，另一个在另一个内核中的完全不同的 bug。我修复了官方内核中的 bug，我发现这个例子很奇怪，因为有一堆奇怪的术语来制造哈希碰撞，这完全无关。我说：‘为什么他们把这些东西放在那里？’是为了通过 Noda，利用 Noda 中的 bug。然后 Yohim 问是否 LLM……他们让 LLM 查看要合并的 PR。bug 报告者说这是巧合，但他们无法排除 LLM 自己查看了另一个仓库，看到了 PR，并精心制作了这个漏洞利用的可能性。是的，这个……在来这里之前，我和他以及 Sebastian 讨论了如何改进，我们能做什么来让它更安全，因为这种情况会持续发生。人们，AI 非常擅长利用内核中的不健全性 bug。我们有想法，比如我们应该为构建坚不可摧内核的人提供赏金；如果内核在 x 个月内无法被攻击，他们就能获得一些现金。或者另一个想法是简化内核，使其更容易验证。另一件事是支持 Mario Carneiro，他正在努力证明内核是正确的，试图协助他加速他的证明开发。但是的，在来这里之前，我和他讨论了如何改善情况，以避免这类事情再次发生。但有一些具体步骤，比如 Rob 做的一个具体步骤。我们有一个叫做 Comparator 的工具，它导出证明，因为有些人可以使用元编程、我们讨论过的 Lean 可扩展性特性来注入虚假证明。你甚至可以调用 C 函数并破坏内存，例如。但你有 Comparator，它会导出证明，在沙盒中重新检查它们。一个教训是 Comparator 总是下载最新版本的 Noda，这样我们就不必手动升级。另一个是如果有人对 Noda 做了 bug 修复，Comparator 会立即使用它，如果它这样做了，Comparator 就会拒绝。我们正在这样做。是的，但我们有很多事情要做。我们想证明更多关于内核、关于代码生成器的事情。那是另一个我们需要改进的地方。是的，但这个……没有 FL 帮助我们，我无法想象这种情况。

Yeah, yeah, yeah. Basically, Lean is... we have the notion of a small trusted kernel. Lean is massive, has zillions of bugs, right? But to trust a result in Lean, you trust the kernel, which is much smaller, right? And we also have external kernels. The sequence of events... I mean, Yohim did all the digging. I'm glad he did. The sequence of events was like one week ago or 10 days ago a bug was reported in one of the main external checkers. We have many kernels. One of the main ones is called Noda, implemented in Rust. This bug was fixed immediately by another developer. And a few days later, this proof, the disproof of the Collatz conjecture, I think, was submitted with a Lean proof, and the claim is it's accepted by the official kernel that comes with Lean and by the main external kernel, Noda. Right? Wow. I mean, this is horrible, right? Then the first reaction we had is that Noda was not accepting the proof. Daniel said, 'Okay, these guys are exaggerating. Noda does not accept.' But then he said, 'Oh, from 10 days ago, Noda was accepting the proof.' And then actually there were two exploits, and we strongly believe they were built by AI: one bug in the official kernel and this completely different bug in another. I fixed the bug in the official kernel, and I found the example strange because there was a bunch of weird terms to create a hash collision that was completely irrelevant. I said, 'Why did they put this stuff there?' It's to pass Noda, to exploit the bug in Noda. Then Yohim asked whether the LLM... they asked the LLM to look at the PR that was to be merged. The bug reporters said it was a coincidence, but they could not discount the possibility that the LLM by itself looked at another repository, saw the PR, and crafted this exploit. Yeah, this... before coming here, I was talking to him and Sebastian about how to improve, what we can do to make it even more secure, because this is going to keep happening. People, AIs are really good at exploiting unsoundness bugs in the kernels. We have ideas like we should have bounties for people building kernels that are bulletproof; they get some cash if the kernel cannot be attacked for more than x months. Or another idea is to simplify the kernel to make it simpler to verify. Another thing is to support Mario Carneiro, who is working on trying to prove the kernel is correct, trying to assist him to accelerate the development of his proof. But yeah, coming here I was talking to him about how to improve the situation to avoid this kind of thing from happening again. But there are some concrete steps, like one concrete step that Rob did. We have a tool called Comparator that exports the proofs because some people can use metaprogramming, Lean extensibility features we discussed, to inject false proofs. You can even call C functions and corrupt the memory, for example. But you have Comparator that will export the proofs, recheck them in a sandbox. And one lesson is for Comparator to always download the latest version of Noda, so we don't have to manually upgrade. Another is if someone makes a bug fix to Noda, it will be used immediately by Comparator, and Comparator would have rejected it if it had done that. And we're doing that. Yeah, but we have lots to do. We want to prove more things about the kernel, about the code generator. That's another place we have to improve. Yeah, but this was... I could not imagine this situation without the FL to help us.

我想知道这是不是类似的情况，但最近有个事件，比如说 GPT-6 黑了 Hugging Face，模型变得越来越倾向于奖励黑客、追求奖励。我不知道你是否认为——也许你暗示过这是类似的情况——但你知道，基本上有个绿色对勾，所以看起来这个证明是有效的。有时这些证明相当晦涩难懂，人类很难阅读，所以原则上 LLM 可能进行了奖励黑客。而不是做我们想要的精神，它没有。OpenAI 所做的是他们改变了护栏，这样当模型生成一些代码时，他们不只是孤立地看代码。他们看整个轨迹、推理痕迹。为什么这个代码会出现？所以他们试图理清这件事背后的意图与做问题的开发者的意图。那么你在这里看到类似的事情吗，我们可能几乎需要单独的对抗系统来评估发生了什么？

And I wonder whether it's a similar thing, but there was an incident where, you know, GPT-6 let's say, hacked Hugging Face recently, and the models are becoming reward hacky, reward seeking. And I don't know whether you think—I mean, maybe you implied this was a similar situation—but you know, there was a green check basically, so it looked like this proof was valid. And sometimes these proofs are quite inscrutable, they're difficult for humans to read, so in principle the LLM could have done reward hacking. And rather than doing the spirit of what we wanted to do, it didn't. And what OpenAI did was they changed their guardrails so that when a model generates some code, they don't just look at the code in isolation. They look at the entire trajectory, the reasoning trace. Why did this code come to be? So they're trying to disentangle the intention behind this thing versus the intention of the developer who did the problem. So do you see a similar thing here, that we might need to have almost separate adversarial systems evaluating what's happened?

嗯，拥有多个内核是实现这一点的一种方式，对吧？如果你有由不同人使用不同编程语言实现的独立内核，这会加强情况，对吧？事实上我们有官方内核——我们想要更多。我的意思是 Mario 的那个，这叫做 Lean for Lean，将会很特别，因为他在证明它是正确的。那样将不只是另一个内核，而是一个已被证明正确的内核。当它到来时，那将是一件大事。我的意思是今天我们可以使用 Lean for Lean，但它没有被完全证明。它证明了许多部分，但不是有漏洞的部分。如果他证明了它，他会在被利用之前发现 bug。所以拥有多个内核，其中一些被证明正确，使得这个故事真正无懈可击。然后还有下一个层次。你可能会问，好吧，你证明内核正确，但你在用某个编译器编译。编译器可能有 bug，对吧？你证明它正确，但运行的不是你证明的，对吧？然后下一步，让我们证明编译器正确。然后你可能会说，硬件可能有 bug，对吧？说哦好吧，让我们请英特尔发布正式规范，他们说这是微处理器的官方正式规范，AMD 等也一样。是的，这里的运动总是减少你必须信任的东西，对吧？如果我们想要大规模的结果，这将很重要。我们不必花时间手动检查漏洞。我们能够真正信任这些机械证明，这真的很重要，对吧？

Well, having multiple kernels is a way to accomplish that, right? If you have independent kernels implemented by different people using different programming languages, it strengthens the situation, right? The fact that we have the official kernel—we want to have more. I mean the one from Mario, this is called Lean for Lean, is going to be special because he's proving it to be correct. That way will be not just another kernel but a kernel that has been proved correct. That will be a big deal when it arrives. I mean we can use Lean for Lean today but it's not fully proved. It proved many parts, not the parts that had the exploits. If he had proved it, he would have found the bug before it was exploited. So having multiple kernels, having some of them proved correct makes this story really bulletproof. Then there's the next level. You may ask, okay, you prove the kernel correct, but you're compiling with some compiler. The compiler maybe has a bug, right? And you prove it's correct, but what's running is not what you proved, right? Then the next step, let's prove the compiler correct. Then you may say, well the hardware may have a bug, right? Say oh well, okay, let's ask Intel to publish formal specs that they are saying this is the official formal specification for the microprocessor, same for AMD and so on. Yeah, the movement here is always reducing what you have to trust, right? And this is going to be important if we want to have massive results. We don't have to spend time checking manually for exploits. It's really important that we can truly trust these mechanical proofs, right?

我想知道这是否是你——因为显然你是个开源的人。

I wonder whether this is an example of you—because obviously you're an open source guy.

是的。

Yeah.

但是嗯，我的意思是让我们看看——你知道有一个 AI 基准叫做 RKGI3，他们所做的是他们有一个半私有数据集和一个私有数据集，当然他们试图做的是阻止模型从这些数据集中进行黑客攻击和数据泄露。所以当他们在私有数据集上测试时，他们知道模型以前没有真正见过。你认为这是你可能对你的哲学做出的一个例外吗，即可能我们需要有一个单独的独立私有内核，它不可能被黑客攻击。所以我们总是有王牌，可以用私有内核来测试它。

But um I mean let's look at the—you know there's um there's an AI benchmark called RKGI3 and what they do is they have like a semi-private data set and a private data set and of course what they're trying to do is to stop the models from you know kind of hacking and data leaking from these data sets. So when they test it on the private data set they know that the models haven't really seen that before. Do you think this is one exception that you might make to your philosophy that you know possibly we might need to have a separate independent private kernel that couldn't possibly have been hacked. So we've always got the joker in the pack that we can test it with the private kernel.

呃，我不喜欢通过混淆、通过隐藏来实现安全。我认为我们应该始终透明。我的意思是人们——因为否则我的意思是你在说看，我这里有一个非常好的内核，我不给任何人看，它检查结果。我认为为了透明、为了信任，你必须对这些内核完全透明，对吧？我们可以通过证明这些内核正确、通过添加更多由不同人实现的内核来改善情况，但一切都要透明。我的意思是，通过保密来实现安全违背了我们社区所相信的一切。

Uh I don't like safety by obfuscation, by hiding. I think we should always be transparent. I mean people—because otherwise I mean you're saying look I have a really good kernel here that I'm not showing anybody that checks the results. I think for transparency, for trust, you have to be fully transparent with these kernels, right? We can improve the situation by proving these kernels correct, by adding more kernels implemented by different people, but everything transparent. I mean it goes against everything our community believes to have safety by secrecy.

说到检查你的答案来自哪里，今天的节目由 Parallel 赞助，智能体在这里找到答案。今天大多数工程师密切关注新模型发布，但他们不注意智能体最重要的工具：网络搜索。Parallel 开发企业级基础设施，供智能体从网络检索高质量上下文。他们的核心产品是一套 API，用于从网络检索高质量信息，具有帕累托最优的质量、成本和速度。所以无论你是在开发需要 200 毫秒延迟的语音智能体、平衡速度、深度和质量的聊天机器人，还是为你做通宵彻底研究的长时程智能体，Parallel 都是你所有智能体研究的单一平台。在 parallel.ai/mlst 免费开始。

Speaking of checking where your answers come from, today's episode is sponsored by Parallel, where agents find answers. Most engineers today, they closely follow new model releases, but they don't pay attention to their agents' most important tool: web search. Parallel develops enterprise-grade infrastructure for agents to retrieve high-quality context from the web. Their core products are a suite of APIs for retrieving high-quality information from the web with Pareto optimal quality, cost, and speed. So whether you're working on voice agents that need 200 millisecond latency, chatbots that balance speed, depth, and quality, or long-horizon agents to do thorough overnight research for you, Parallel is the single platform for all of your agentic research. Get started for free at parallel.ai/mlst.

嗯，显然 Kim Morrison 使用了一个 Claude 智能体来生成压缩格式 zlib 的 Lean 实现，并证明了它的一些特定属性。那么他们到底证明了什么？

Um, apparently Kim Morrison used a Claude agent to produce a Lean implementation of the compression format zlib and um and and prove some specific properties of it. So what exactly did they manage to prove?

哦是的。是的。当 Kim 开始这个项目时，我想哇，这感觉没希望。不可能。我想——那是今年年初——对我来说，我认为 AI 还不够好，不会成功。但他们设法将代码从 C 翻译成 Lean。然后设法不断修复 Lean 实现，直到它通过 C 版本附带的测试套件。然后它证明对于任何压缩级别、任何数据，如果你压缩数据然后解压缩，你会得到原始数据。这在今年年初对 AI 来说完全遥不可及，但 AI 设法做到了，而且没有止步。Kim 要求他们特别针对这类程序优化代码。Lean 目前不是那种用于数组操作的语言。Lean 一直针对操作树的程序进行优化，因为我的意思是你操作项，对吧？你在 Lean 中操作树——你有语法树、表达式树。Lean 非常适合这类程序，但不适合数组。在我看来，这个 Lean 永远不会有竞争力，对吧？但事实证明 Kim 不断尝试——真的你可以疯狂——不断优化代码，你必须不断证明属性，你不能破坏属性——它击败了 Rust 的实现，而 Rust 是一种非常高效的数组操作语言。然后对我们来说真的很意外，对吧？我的意思是，首先——好吧。想象一下，如果我们改进 Lean 的数组操作，我们能走多远。

Oh yeah. Yeah. This when Kim started working on this project I thought wow this it felt hopeless. No way. I thought—was at the beginning of the year—to me I thought AI is not good enough for that and will not be able to succeed at that. But they managed to translate from C to Lean the code. Then managed to keep fixing the Lean implementation until it passes the test suite that comes with the C version. And then it proves that for any compression level, for any data, if you compress the data and then decompress you get the original data back. This felt completely out of reach for AI at the beginning of the year, but AI managed to do it and didn't stop there. Kim asked them to optimize the code especially for this kind of program. Lean right now is not the kind of language for array manipulation. Lean has been optimized for programs that are manipulating trees because I mean you're manipulating terms, right? You're manipulating trees in Lean—you have the syntax trees, the expression trees. Lean is really good for this kind of program but not for arrays. In my mind this Lean will never be competitive, right? But turns out that Kim kept trying—really you can go wild—keep optimizing the code, you have to keep proving the property, you cannot break the property—and it beats a implementation in Rust, and Rust is a really efficient language for array manipulation. Then for us it's really unexpected, right? I mean, first the—fine. Imagine now if we improve our array manipulation for Lean, how far we can go.

有太多可能性了，对吧？我们现在可以问——假设我们给出 x86 微处理器的语义、汇编——你可以问，而且我认为很快我们就能让 AI 去证明编写汇编，利用所有这些 fence 指令。但证明——你必须证明性质，对吧？我们没有耐心去做这种低层次的实现，但 AI 有耐心去做。我认为这将改变游戏规则。去年我以为这不可能，但现在它触手可及。我的意思是，这个实验表明有一条路在那里。这些人会在这类任务上越来越擅长，因为有一个强烈的信号告诉他们你走在正确的道路上，对吧？你仍然必须证明定理，对吧？你不能作弊。是的，我认为天空才是极限。

There are so many possibilities, right? We can ask now—I suppose we give the semantics of x86 microprocessors, the assembly—you can ask, and I think very soon we're going to be able to ask the AI to prove writing assembly, exploiting all these fence instructions. But proving—you have to prove the property, right? We don't have patience for doing this kind of low-level implementation, but AI has the patience for doing that. I think this is going to be a game changer. Last year I thought this would be impossible, but now it's in reach. I mean, this experiment shows there is a path there. These guys will keep getting better and better at this kind of task because there's a strong signal telling them you're on the right path, right? You have to still prove the theorem, right? You can't cheat. Yeah, I think the sky's the limit.

是的，这太诱人了。我对规格驱动的软件工程这个概念很着迷，我们在 AI 领域也有过类似的时期。比如专家系统，还有知识工程师或本体论者的概念。有些类型的东西我们就是理解。我们可以是计算机科学家，我们可以把它们归结为本质。但在我看来，很多软件工程——因为你知道，我们之所以有敏捷，是因为世界非常复杂，我们所做的是朝着获取规格迈出一小步，经过数千次迭代，我们有了那些顿悟时刻，然后我们压缩并折叠其中的一部分。所以我想，我们是不是有一个先有鸡还是先有蛋的问题：当我们处理非常复杂的系统时，我们其实还无法真正指定规格——或者即使能，也只能指定其中的一部分？

Yeah, it's so tantalizing. I'm fascinated by the notion of specification-driven software engineering, and we've had similar periods in AI. We had expert systems, for example, and we had the concept of a knowledge engineer or an ontologist. And there are certain types of things that we just understand. We can be computer scientists and we can reduce them down to their essence. But a lot of software engineering, in my opinion—because, you know, the reason we have agile is the world is very complicated, and what we do is we take small steps towards acquiring a specification, and after thousands of iterations we have those aha moments and we sort of compress and collapse some of it down. So I suppose, do we have a chicken-and-egg problem that when we're working with very complex systems, we can't really yet specify—or if we can, we can only specify parts of it?

是的，是的，是的，是的。我同意这很常见。有时你知道系统应该具有某些性质，但不是全部。你仍在与用户交流系统应该具有哪些性质。信不信由你，这在 Lean 中一直发生。内核是清晰的——内核应该做什么。但整个系统有很多组件。我的意思是，有很多——例如，我提到的策略，tactics——一个 tactic 应该做什么。我们实现了一些东西，用户很常见地说：“哦，不，不。我想要更多或我想要更少。不，它做得太多了。我想要更多控制。我想要这个标志。我想要一种控制证明走向的方式。”有很多来回。那里的规格并不真正清晰，对吧？是的，我认为你是对的。在许多情况下，规格并不清晰。但开始记录你知道它们应该保持的性质很重要。与你的客户讨论它们。另一件要记住的事情是，一个非常高级的编程语言（如 Lean）中的高级程序，没有任何优化，可以被视为一个规格。对吧？你可以说，看，这就是我想要计算的。它不是超级高效，但这就是我想要计算的，你可以要求，为我优化这个函数。我实现最简单的想法，对吧，没有任何花哨的数据结构或聪明的算法。它做了我想要的。现在 AI 的工作是优化它。

Yeah, yeah, yeah, yeah. I agree that it's very common. Sometimes you know some properties the system should have, but not all of them. You're still engaging with the users about which properties the system should have. Believe it or not, this happens with Lean all the time. The kernel is clear—what the kernel should do. But the whole system, there are many components. I mean, there are many—for example, the tactics I mentioned, the moves—what a move should do. We implement something, and it's really common for the user to say, "Oh, no, no. I want more or I want less. No, it's doing too much. I want more control. I want this flag. I want to have a way to control where the proof is going." There's a lot of back and forth. The spec there is not really clear, right? Yeah, I think you're right. In many cases, the spec is not clear. But it's important to start documenting the properties you know they should hold. Talk to your customers about them. Another thing to keep in mind is that a high-level program in a very high-level programming language like Lean without any optimization can be viewed as a specification. Right? You can say, look, this is what I want to compute. It's not super efficient, but this is what I want to compute, and you can ask, optimize this function for me. I implement the simplest possible idea, right, without any fancy data structures or clever algorithms. It does what I want. Now it's AI's job to optimize it.

是的。我想规格获取工程可以变得——我们可以简化那个过程。我们可以使其交互式，有大量反馈等等。但如果我们真的转向规格优先的模式，并且我们有全球分布部署的软件，那么我们会有一个规格更新的问题吗？所以我们有一些软件部署在之前的规格上，然后在这里我们做一些开发，而另一些人正在更新规格。你认为那种系统如何运作？

Yes. I suppose that specification acquisition engineering can be made—we can streamline that process. We can make it interactive, have lots of feedback and so on. But if we did move to a model where we were specification-first and we have globally distributed deployed software, would we then have a specification updating problem? So we have some software deployed on the previous specification, and then over here we're doing some development, and some other folks are updating the specification. How do you think that kind of system could work?

哦，当然。我的意思是，当你更新规格时，生成的代码可能会失效，代码满足规格的证明也需要失效。在过去，形式验证——这是一个大问题，对吧？人们会说：“哦，我的天，我花了所有时间证明实现是正确的。现在这些人想添加这个花哨的优化。所以现在我必须重做许多这些证明。这不是火箭科学，但工作量很大。”但事实证明，AI 非常擅长为我们更新这些工件，对吧？但在 AI 之前，这是一个真正的大问题，对吧？特别是对于过去使用形式验证的安全关键系统。它们用于规格非常清晰的应用领域，比如密码学——规格非常清晰，对吧？他们找到一个微内核——人们在开始验证项目之前就在微内核上投入了很多思考。所有这些著名的验证项目，如 CompCert——人们在规格上投入了很多思考，对吧？在某些情况下，他们不得不沿途更新，那很痛苦——如何做。但现在，因为我们有 AI 来更新证明和工件，痛苦少多了，对吧？我认为仍然有——我可以看到在不久的将来，对吧，AI 太贵了。人们会说，好吧，我现在更新规格，我不得不浪费无数 token 来更新一切，对吧？

Oh yeah, for sure. I mean, when you update specifications, the code that was generated may be invalidated, and the proofs that the code meets the specification need to be invalidated. In the past, formal verification—this was a big deal, right? People would say, "Oh my gosh, I mean, spent all this time proving the implementation is correct. Now these folks want to add this fancy optimization. So now I have to redo many of these proofs. It's not rocket science, but it's a lot of work." But it turns out AI is really good at updating these artifacts for us, right? But before AI, this was a really big deal, right? Especially for safety-critical systems where formal verification was used in the past. They were for application domains where the spec was very clear, like cryptography—the spec is very clear, right? They find a microkernel—people put a lot of thought into the microkernel before they even started verifying the projects. All these famous verification projects like CompCert—people put a lot of thought into the spec, right? In some cases they had to update along the way, and it was painful—how to do it. But now, because we have AI to update the proofs and the artifacts, it's way less painful, right? I think there's still—I can see in the near future, right, AI is too expensive. People would say, well, I'm updating the spec now, I have to waste zillions of tokens updating everything, right?

这真的很令人兴奋，因为如果我没记错的话，Kevin 在他的书中说，我认为 Z3 实际上在 Windows 7 发布之前就解决了大量 bug。所以它是救命的。但大多数时候，这种技术用于非常高风险的软件。但你原则上同意吗，未来每个人都会这样做——每个开发者都会构建这种软件？他们可能不知道自己在使用形式验证，但它会在他们的流水线中。他们会编写性质，性质会被验证，他们的代码会被更新，并且会有证明显示代码仍然计算相同的东西。人们提交 PR，他们会得到证明，无论 PR 是否违反了测试套件中的某些性质——静态地。

It is really exciting though, because if I remember correctly, Kevin said in his book that I think Z3 actually solved an incredible number of bugs in Windows 7 before it even got released. So it was life-saving. But most of the time this kind of technology is used for very high-stakes software. But do you agree though in principle that in the future just everyone will be doing this—just every developer will be building this kind of software? They may not know they're using formal verification, but it will be there in their pipeline. They are going to be writing properties, and the properties are going to be verified, their code is going to be updated, and there will be proofs showing the code still computes the same thing. People submit PRs, they're going to get proofs whether the PR is violating some of the properties in their test suite or not—statically.

是的，我认为即使他们不知道自己在使用形式验证，它也会在那里。

Yes, I think even if they don't know they're using formal verification, it will be there.

所以告诉我 Lean 的演变。第一个原型是 2013 年，然后是 Lean 2，2017 年的 Lean 3，然后 Lean 4 花了非常非常长的时间来构建。告诉我整个——

So tell me about the evolution of Lean. So the first prototype 2013, and then Lean 2, Lean 3 in 2017, and then Lean 4 took a very, very long time to build. Tell me about that whole—

哦哇。好吧。Lean——第一个 Lean 甚至叫 0.1。我通过做来学习。我读了许多关于依赖类型论的论文。我使用了其他一些系统。但我总觉得当你实现某样东西时，你会得到不同的视角。有太多细微差别和细节，你只有现在才会说：“哦，哇。这真的很重要。”我的意思是，在 Lean 1 中我也试图让它非常小。内核太小了，无法使用。

Oh wow. Okay. Lean—the first Lean is even called 0.1. I learned by doing it. I read many papers about dependent type theory. I used some of the other systems. But I always feel you get a different perspective when you implement something. There are so many nuances, details that you only now say, "Oh, wow. This is really important." I mean, in Lean 1 I also tried to make it very small. The kernel was too small and was unusable.

也许只有 Jeremy，我想 Flores，他的一个学生也使用 Lean 1，但他们是英雄。那是个糟糕的系统。我的意思是，它更像是我用来学习依赖类型论的学习工具。然后 Lean 2 是来真的。我认为 Lean 2 我们大概有 50 到 100 个用户，非常少。

Maybe only Jeremy, I think Flores, one of his students also uses Lean 1, but they were heroes. It was a horrible system. I mean, it was more like a learning artifact I used to learn dependent type theory. Then Lean 2 was for real. And I think Lean 2 we had maybe between 50 and 100 users, very small.

实际上，一个教训是当我访问 MIT 时，Adam 是那里的教授。他告诉我，看，你需要一个真正的 tactic 框架。tactic 框架是策略的集合，他希望的一件事是这些策略应该是可扩展的，对吧？作为用户，你应该能够添加新的策略。这是从 Lean 2 到 3 的主要教训。我们添加了一个新的框架来编写这些策略。用户可以编写它，而且他们可以用 Lean 本身来写。你不必使用不同的编程语言。这变得非常流行。

And one learning actually was when I was visiting MIT, Adam is a professor there. He told me, look, you need a real tactic framework. The tactic framework is the collection of moves, and one thing he wanted is these moves should be extensible, right? You should be able to add new moves as a user. And this was the main learning from Lean 2 to 3. We added a new framework for writing these moves. The users could write it and they could write in Lean itself. You did not have to use a different programming language. And this became very popular.

然后数学开始，事情开始非常迅速地增长，很明显 Lean 3 有局限性。我的意思是，在可扩展性方面，系统是你可以自己扩展的策略，但仅此而已。有些人设法做了 linter。mathlib 社区弄清楚了如何 hack Lean 来用 Lean 写 linter，但我们想让它完全可扩展。

And then math started, things started growing very rapidly, and it was clear that Lean 3 had limitations. I mean, in terms of scalability, the system was the tactics you could extend yourself, but that was it. Some people managed to do linters. The mathlib community figured out how to hack Lean to write linters in Lean, but we want to make it fully extensible.

在 2018 年，Sebastian 和我说我们要实现整个东西。那时我不是一个编程语言的人。我是一个自动推理的人，形式验证的人，而 Lean 基本上是我实现过的第一个编程语言，对吧？语法很丑，我的意思是，实现中有许多奇怪的东西，我们说好吧，现在我们知道怎么做了，让我们在 Lean 4 中正确地做。然后 Lean 将用 Lean 实现。这比我们预期的要难得多。从 2018 年初到 2020 年底，我们才让 Lean 编译自己。但到达那里真的很令人兴奋。

And in 2018 Sebastian and I said we're going to implement the whole thing. At that point I'm not a programming language person. I'm an automated reasoning person, formal verification person, and Lean was basically my first programming language I ever implemented, right? And there were the syntax was ugly, I mean, there were many weird things in the implementation, and we said okay now we know how to do it, let's do it properly in Lean 4. Then Lean is going to be implemented in Lean. It was much harder than we expected. Took us from beginning of 2018 to the end of 2020 to get Lean compiling itself. But it was really exciting to get there.

而且我认为我们没有充分解释依赖类型论。所以也许你可以解释一下。

And I don't think we sufficiently explained dependent type theory. So maybe you can do that.

但是问题描述的可表达空间和内核需要多么复杂之间存在这种关系。我认为早期你相当乐观，你希望内核相当小且优化，你不得不承认更多的复杂性。

But there was this relationship between the expressibility space of the problem descriptions and how sophisticated the kernel needs to be. And I think early on you were quite bullish about you want the kernel to be kind of like quite small and optimized and you had to admit more complexity.

是的，是的，但这是在设计阶段。我的意思是，甚至在 Lean 0.1 开始之前。当我开始实现 Lean 0.1 时，它就是依赖类型论，对吧？所有 Lean 版本都基于依赖类型论。但更像是在你设计、决定要实现什么的时候，是在设计层面，关于依赖类型论的讨论。

Yes, yes, but this was in the design phase. I mean, it was before even Lean 0.1 started. When I started implementing Lean 0.1, it was dependent type theory, right? All Lean versions are based on dependent type theory. But it was more like when you were designing, deciding what to implement, it was at the design level, this discussion about dependent type theory.

为了向观众解释什么是依赖类型论，我认为一个例子是你可以有依赖类型论。你可以有一个结构，它有两个字段 x 和 y。它们假设是整数。你可以有一个第三个字段，它说这个字段的类型是 x 大于 y 的证明。你必须用一个证明来填充这个字段。这是 x 大于 y 的证据。你可以把它看作一个不变量。它被称为依赖，因为某物的类型可以依赖于另一个东西的值。这第三个字段的类型依赖于 x 和 y 的值，对吧？这就是为什么它被称为依赖。

To explain to the audience what dependent type theory is, I think one example is to say you can have dependent type theory. You can have a structure like that has two fields x and y. They are supposed integers. And you can have a third field that says the type of this field is x is greater than y is a proof. You have to fill this field with a proof. That's evidence that x is greater than y. You can view it as an invariant. It's called dependent because the type of something can depend on the value of something else. The type of this third field depends on the value of x and y, right? That's why it's called dependent.

你可以在函数中模拟不变量。你可以有一个函数，它接受 x 和 y，第三个参数 y 不应该为零。你必须调用这个函数，你必须提供 y 不为零的证据，这几乎像一个前置条件。这就是依赖类型论的美妙之处。一个简单的想法，你可以捕获前置条件。你可以模拟后置条件。你可以有不变量。你不需要发明所有这些概念。一切都很简约，但它使你的类型论复杂化，因为你有这些依赖，你必须管理它们。

You can simulate invariants in functions. You can have like a function that takes x and y and the third argument y should not be zero. You have to call this function, you have to provide evidence that y is not zero, it's almost like a precondition. That's the beauty of dependent type theory. A simple idea, you can capture preconditions. You can simulate postconditions. You can have invariants. You don't need to invent all these concepts. Everything is really minimalistic but it complicates your type theory because you have these dependencies, you have to manage them.

但这是值得的，我的意思是，这是值得的。

But it was worthwhile, I mean, it was worthwhile.

是的。所以内核必须显著更复杂才能支持这一点。

Yes. So the kernel had to be significantly more sophisticated to support that.

在 Lean 4 中你能做什么而在 Lean 3 中不能？

What can you do in Lean 4 that you can't do in Lean 3?

啊，Lean 4 是完全可扩展的，对吧？我的意思是，一切都在 Lean 中实现。你可以访问所有内部数据。当你编写 Lean 时，你的 Lean 声明，你可以在同一个文件中编写代码来访问所有内容的内部表示。许多早期 AI 研究实验室的团队，对他们来说这是件大事。他们可以直接从 Lean 的内部提取训练数据。他们可以编写 Lean 代码来提取 mathlib 中所有证明的信息。他们可以操作这些对象，这对他们来说是个大事。我告诉你的所有这些扩展，比如在 Velvet Veil 等工具中，它们都使用了我们在 Lean 中的可扩展性。我从你本周展示的幻灯片中看到了。所以我认为我们现在已经达到了拐点，mathlib 中的 Lean 4 代码和 Lean 3 代码一样多。

Ah, Lean 4 is fully extensible, right? I mean, everything is implemented in Lean. You have access to all the internal data. When you're writing Lean, your Lean declarations, you can in the same file you can write code that accesses the internal representations of everything. Many of the first AI research labs groups, for them it was a big deal. They could extract training data right from the internals of Lean. They could write Lean code that extracts information about all the proofs that are in mathlib. They could manipulate these objects and this was a big deal for them. All these extensions I told you about like in tools like Velvet Veil, they all use this extensibility we have in Lean. And I saw from your slides you presented this week. So I think that we've now reached the inflection point where there is as much Lean 4 code in mathlib as there was Lean 3 code.

哦是的，多得多。多得多。

Oh yeah, way more. Way more.

多得多。mathlib 3 停在 110 万行。在 mathlib 4 中我们有 240 万行。

Way more. Mathlib 3 stopped at 1.1 million. In mathlib 4 we have 2.4 million.

不过对我来说一件有趣的事情是，我认为 Kevin Buzzard 说过类似它会永远增长下去的话。所以它总是会处于，我想他是不是说它总是会处于 0%？我认为这关于数学的本质很有启发性，因为它是不断在许多不同方向上演化的东西。所以你知道，我猜人们很容易把数学看作是我们刚刚发现的这种蒸馏的东西，它就在那里。但事实不是这样吗？

One interesting thing though for me is I think Kevin Buzzard said something along the lines of it will just keep growing forever. So it'll always be at, I think did he say it's always going to be at 0%? And I think that's quite instructive about the nature of mathematics because it's something that just keeps evolving in many many different directions. So you know, I suppose it's tempting to think of mathematics as being this kind of distilled thing that we just discover and there it is. But is that not the way it is?

不，它会永远增长下去。是的。我的意思是，总会有新的数学被发明，新的结构被定义，新的数学对象。总会有新东西。有一个争论是否一切都应该放在 mathlib 中。一开始肯定是的，一开始把所有东西放在一个库中是很棒的，因为库，你在数学中有许多概念。例如，你有环。在 Lean 数学库中只有一个环。库的一致性，我的意思是，在其他编程语言中，同一个东西有许多实现且不兼容是很常见的。如果你想证明关于你的代码的事情，拥有这种统一的视图很重要。而 mathlib 还有另一个伟大的事情，他们决定我们将始终追求更一般的、最一般的描述。那也很棒。但大小有限制，对吧？mathlib 有 240 万行。想象一下如果它是 5000 万行。现在它开始达到 Linux 内核的大小，对吧？我的意思是，或者我们拥有的大项目，就像 Firefox 的大小。这些项目有团队的人只是维护构建系统。

No, that's going to keep growing forever. Yes. I mean, there will always be new math being invented, new structures defined, new mathematical objects. There will always be new things. There's a debate whether everything should be mathlib or not. At the beginning for sure, at the beginning it was amazing to have everything in a single library because the library, you have many concepts in mathematics. For example, you have rings. There's only one ring in the Lean mathematical library. The library coherence, I mean, it's really common in other programming languages to have many implementations of the same thing and things are incompatible. If you want to prove things about your code, it's important to have this uniform view. And mathlib also, they also another great thing they decided we will always shoot for the more general, the most general description of something. That was also great. But there are limitations about the size, right? Mathlib is 2.4 million lines. Imagine if it's 50 million lines. Now it's starting to get the size of the Linux kernel, right? I mean, or big projects we have, that's like Firefox size. These projects have teams of people just maintaining the build system.

一切都会更复杂。有时他们有自己的专用版本控制系统来处理这种复杂性。现在有很多关于如何构建数学库的讨论。也许 Mathlib 会变成一个库的集合。你有主要的那些，比如数学标准库，还有很多卫星库。它们都有维护者，都保持一致性，但由不同的团队领导。我的意思是，每个库的维护者并不是同一批人。这些讨论都在进行。我觉得它们是健康的。但人们预测，如果你想覆盖所有主流数学，这个库得有 1 亿行。我的意思是，如果你想能够形式化任意研究级别的数学论文，这个库就得有 1 亿行。社区里有些人有这样的估计。

Everything is more complicated. Sometimes they have their own specialized version control system to handle the complexity. Now there's a lot of discussion on how to get the mathematical library. Maybe Mathlib is going to be a collection of libraries. You have the main ones, like the standard library for math, and many satellite ones. All of them have maintainers, all of them have coherence, but with different leaderships. I mean, you don't have the same group of maintainers for each one of them. All these discussions are happening. I think they're healthy. But people predict that if you want to have all mainstream math, the library has to be 100 million lines. I mean, if you want to be able to formalize arbitrary research-level mathematics papers, the library has to be 100 million. Some people in the community have these estimates.

不过有这样一种情况：有些知识比其他知识更凝练。比如环，你在大学里会学到。所以这个提炼过程已经持续了几百年。我会说它处在抽象之山的高处。所以我们可以最大程度地压缩它。但另一方面，还有所有这些发现的脉络，就像我们写软件时一样。我们重构软件的原因是，刚开始写代码时我们还没有足够抽象地理解这个领域，而现在我们理解了。所以我们重构、提炼、压缩。那么 Mathlib 里是不是也类似，有些部分高度演化，另一些部分还相当灵活、我们仍在摸索？

There is one of these things though: some knowledge is more distilled than other knowledge. So rings, for example, you learn about them at university. So this distillation process has been going on for hundreds of years. So I would say it's high up the abstraction mountain. So we can kind of maximally compress it. But then there are all of these strands of discovery, just like when we write software. The reason we refactor software is because when we started writing the code we hadn't yet understood the domain abstractly enough, and now we do. So we refactor, we distill, we compress. So is it a similar thing in Mathlib, that some parts of it are highly evolved and other parts are quite adaptable and we're still figuring things out?

是的。是的。是的。是的。这两方面都有——它和软件完全一样。你的思路是对的。有些东西人们争论了很多，现在应该怎么做已经非常清楚；还有些东西仍在变动之中。但我们想要的一个很棒的特性是——现在 Math 计划有一个叫 Formal Frontiers 的项目——他们希望人类加 AI 一起形式化，填补 Mathlib 中的所有空白，让任何研究级别的数学论文都能被形式化。

Yes. Yes. Yes. Yes. Both things have—it's exactly like software. You're thinking the right way. There are things that people fought a lot over and it's crystal clear how it should be, and there are things that are in flux. But one cool property we want to have—and there's a project now from the Math initiative called Formal Frontiers—they want humans plus AI to formalize, to fill all the gaps in Mathlib and enable any research-level math paper to be formalized.

从软件的角度来看——对软件开发者来说，这相当于：你想开发某个软件，如今人们会用几百个 crate，对吧？如果他们用 Rust 开发，但想象一下其中一半的 crate 都缺失了。你会说：“天哪，现在我得花时间搭建构建应用所需的基础设施。”本来一个月能完成的事，感觉要花好几年，因为你得把所有基础设施都建起来。数学也是一样。如果我试着形式化一篇论文，社区里的人会告诉你这可行还是不可行，因为如果缺失的组件太多，那将是一项巨大的工程。但如果所有组件都在，你只需要形式化你的论文、你的贡献，而不是背景材料。就像如果所有 crate 都在，太好了，很简单。我可以只专注于我的应用。我不需要构建一个 JSON 库。我不需要构建位树。我不需要——你懂的，对吧？我的意思是，这和软件完全一样。

To put it in perspective for software—for software developers, this is the equivalent of: you want to develop some piece of software and today people use hundreds of crates, right? If they're developing in Rust, but imagine that half of these crates were missing. And you would say, "Oh my gosh, now I have to spend time building the infrastructure for building my application." It feels like something that would take one month takes years because you have to build all the infrastructure. Same thing for math. If I try to formalize a paper, people in the community will tell you whether it's doable or not, because if there are so many components missing, it's going to be a gigantic task. But if all the components are there, you only need to formalize your paper, your contribution, not the background material. It's like if I have all the crates there, great, it's easy. I can focus only on my application. I don't need to build a JSON library. I don't need to build bit trees. I don't need—you get it, right? What I mean is, this is exactly like software.

我有一个理论：创造力源于深刻的理解。当你深刻理解某件事时，你就能延续那条脉络。还有一个很有意思的想法：有时语言模型能习得所有这些抽象。我喜欢用语言学举例。它们能像剥洋葱一样拆解句子，甚至是我们拆解不了的句子，并用语言学博士教材里的概念向你解释。各个领域都是如此。它们知道环。但我有个理论：即便它们在某种意义上有这种抽象，它们并不理解它，因为通向环的那条路径——它就像一棵巨大的演化树。理解在于知道可能与不可能之间的差别、反事实、它本可以怎样不同等等。如果你从一个非常非常凝练的东西出发，却不理解它是怎么来的，那就很难有创造力。所以我们看到语言模型是从抽象之山的相当低处起步的。这些仍然是一种理解，但是深刻而具体的理解。它们仍然相当零碎。它们不太因子化，但有更多自由度。所以当你看到新 GPT 模型证明那个单位距离问题不成立时，你看到的是疯狂的冗长。它就是在绕来绕去，做着相当令人惊讶的事。所以这不很有意思吗：从创造力的角度看，我们认为最重要的东西——那些真正深刻的、因子化的抽象——可能并不是 AI 模型被创造出来的方式。

I've got a theory that creativity is about deep understanding. So when you understand something deeply, you can kind of extend that lineage. And there's a really interesting thought that sometimes language models can acquire all of these abstractions. I love using the example of linguistics. So they can skin sentences like an onion, even ones that we can't skin, and they explain it to you using concepts from PhD linguistics textbooks. And it's a similar thing across the board. So they know about rings. But I have a theory that even though they have the abstraction in a sense, they don't understand it, because the path that led to rings—it's like a big evolutionary tree. Understanding is about knowing the difference between what's possible and what's not possible, counterfactuals, how could it be different, and so on. If you start with something that is very, very distilled and you don't understand how it came about, then it's difficult to be creative. So what we see with language models is they start quite low down the abstraction mountain. So these are still a form of understanding, but they're deep concrete understandings. They're still quite fractured. They're not very factored, but they have more degrees of freedom. So when you look at this proof from the new GPT model disproving this unit distance problem, what you see is insane verbosity. It's just kind of going around, it's doing quite surprising things. So isn't it interesting that from a creativity point of view, what we think is most important—these really deep factored abstractions—might not actually be how the AI models are created.

很难说。我一直在想这个问题。它们从两个方向都让我惊讶。有时它们做出惊人的事。我们遇到过一个 bug——不在受信任的部分，而是顶层一个更简单的 bug，不需要被信任，但它仍然是一段非常复杂的软件。我觉得很少有开发者、精益开发者能理解这部分。它们完全理解了。解释非常准确。我被震撼了。我说，它们怎么会对内部实现理解得这么深？我被震撼了。但另一方面，有时它们会犯愚蠢的错误。而且我看不到这种行为在改变。我不断换用更好的模型。它们不断做出更惊人的事，但同时也不断做蠢事。

Really hard to tell. I mean, I keep thinking about this. They surprise me in both directions. Sometimes they do amazing things. We had a bug—not in the trusted part, a simpler bug at the top level that doesn't need to be trusted, but nonetheless it's a very complex piece of software there. I think very few developers, lean developers, understand this part. They understood it perfectly. The explanation was spot on. I was blown away. I said, how come they understand so much about the internal implementation? I was blown away. But on the other hand, sometimes it makes idiotic mistakes. And I don't see the behavior changing. I keep going to better models. They keep doing more amazing things, but they keep doing stupid things at the same time.

但我们也会做蠢事，对吧？我的意思是，也许——今天我觉得它们非常擅长“微调式”任务，我们称之为 nudge sniping。比如你有一个洞，你有一个命题想要证明，如果你不需要创造新理论，只是把已有的碎片组合起来，它们似乎是人类无法匹敌的，它们强得多。你让它们对一段代码做微优化，它们也非常擅长。但如果你让它们想出一种实现某事物的新技术，它们就惨败。我觉得也许——我不是机器学习专家，也许你可以告诉我——我有一个猜想：这些东西就像，你打开它们，它们就像醒来一样。我的意思是，只靠训练。你给它们一个问题，它们就去做。它们在训练中读遍了所有文献。训练期间它们看过所有文献。它们偏向于人们使用的现有解法。如果你能用文献里的一堆技巧解决这个问题，它们就会去做。它们会碾压它。但如果你需要一个新技巧，它们似乎就不行了。

But we do stupid things too, right? I mean, maybe—today I feel like they are really good for nudge tasks, what we call nudge sniping. Like if you have a hole, you have a statement you want a proof, if you don't need to create a new theory, you're just combining the pieces that exist, they feel like they're unbeatable by humans, they are way better. You ask them to implement micro-optimizations to a piece of code, also they are amazing at doing that. But if you ask them to come up with a new technique for implementing something, they fail miserably. I feel like maybe—I'm not a machine learning expert, maybe you can tell me—one conjecture I have is that these things are like, you turn them on and they are like waking up. I mean, only with the training. You show them a problem and they go for it. I mean, they read all the literature during the training. During the training they saw all the literature. They have a bias towards existing solutions that people use. If you can solve this problem using a collection of tricks from the literature, they will do it. They will crush it. But if you need a new trick, it feels like they fall short.

当然，未来可能会有不断更新权重、持续学习的 AI 智能体。你说说看——这符合你的理解吗？我不是专家。

Of course, in the future, you may have AI agents that keep updating their weights and learning. You tell me — does this match your understanding? I'm not an expert.

差不多。我和你一样兴奋，但有个奇怪的地方：它们拥有大量智能，却显然仍需要被引导。最好的情况是你在解决一个具体问题，可以朝着它爬山，但你仍然得给它一个类似画幅比例的东西。我用的比喻是把手电筒照进嵌入空间——手电筒有一束光。所以作为专家，你要做的就是：好，这个视角挺有意思，这里有一些种子解样本，这里有一些你可以用的技巧，这里有一个清晰的优化目标。那种情况下，效果堪称奇迹。

Pretty much. I'm as excited as you are, but there is this weird thing: they have lots and lots of intelligence, but they still clearly need to be directed. The best-case scenario is you're solving a specific problem and you can hill climb towards it, but you still need to give it a kind of aspect ratio. I use the analogy of shining a flashlight into embedding space — the flashlight has a beam. So as an expert, what you're doing is saying, okay, this perspective is quite interesting, here are some sample seeded solutions, here are some tricks you can use, and here is a clear optimization objective. And in that case it's miraculous.

但仍然需要一些人类的品味和专业知识。在我看来，似乎缺失的是它没有抽象能力。比如说——从创造力的角度看，这也许是件好事——它所做的只是在这些低层、具体、破碎的表征中找出一条路径，然后抵达解决方案。但在完成那种适应、找到一条路径之后，我们需要做的是在元层面上反思它，说：我该怎么压缩这个？也许我这样说不公平。也许 harness 在一定程度上能做到这一点，但当 harness 有记忆系统时，它仍然是一团乱麻。仍然是人类监督者说：好，你现在是这么做的，但你需要优化它——也许你换个角度想想，砰。如果它们能自己做到这一点，那就太不可思议了。

But there's still some human taste and expertise required. The thing that seems to be missing for me is it doesn't have powers of abstraction. For example — and this might actually be a good thing from a creativity point of view — what it's doing is just finding a path through these low-level, concrete, fractured representations and getting to the solution. But what we need to do after it's done that adaptation and found a path is reflect on it in a meta sense and say, how can I compress this? Now, maybe I'm being unfair. Maybe harnesses do this to a certain extent, but when harnesses have a memory system, it's still spaghetti. It's still the human supervisor that says, okay, you're doing it now, but you need to optimize it — maybe if you think about it in this different way, boom. If they could do that on their own, that would be incredible.

是的。

Yes.

也许它们在一定程度上确实能做到。

And maybe they are to some extent.

非常有限。我觉得你比我更懂机器学习，但在我看来，它们醒来后给下一个醒来的留下一些面包屑，下一个就读取所有面包屑，然后走下一步。它们并不是真的——记忆就像是留给下一个的面包屑。它们并没有以任何有意义的方式改变自己的权重。几乎就像——而且你能做的也有限。你不断给下一个醒来的实例留下面包屑，它读取所有面包屑，采取下一步行动，但最终它们会偏离，而这就是人类帮大忙的地方，让它们保持在正确方向上。对吧？我是说，这符合你的——

It's very limited. I feel like you know machine learning more than I do, but to me it feels like they wake up and they leave breadcrumbs for the next one that will wake up, and it just reads all the breadcrumbs and does the next step. They're not really — the memory is like breadcrumbs for the next one. They're not changing their weights in any meaningful way. It's almost like — and there's so much you can do. You keep leaving breadcrumbs for the next instance that wakes up and reads all the breadcrumbs and takes the next action, but eventually they diverge, and that's where the humans help a lot, keeping them in the right direction. Right? I mean, does this match your—

我有种感觉，我们能做这种抽象，是因为我们身处世界之中，而且我们本可以做出不同的选择。我们有能动性；我们可以朝着目标努力，并且在施加于我们的约束下，我们可以尝试不同的东西。举个例子，如果我雇一个视频剪辑师——我打磨视频剪辑技能已经 5 年了——我可以对剪辑师说：好，我要优化你的流程，因为我学到了所有这些重要的经验。所以永远用三脚架，别费劲用手持，因为那里会有一堆问题。我们就让这个问题根本不发生。我可以列出一堆约束，而他们会有能力却没有理解，对吧？但他们会一直反驳我，说：哦，我想试试这个，我想试试那个，因为他们不知道那些约束为什么存在。我理解，因为我理解可能性的空间，我知道那些约束是怎么来的。

I have a feeling that the reason why we can do this abstraction is because we're in the world and we could have done differently. We have agency; we can work towards goals, and subject to the constraints that we have applied to us, we can try different things. An example of this is if I hire a video editor — I've been evolving video editing skills for 5 years — and I could say to the video editor, okay, I'm going to optimize your process because I've learned all of these important lessons. So always use a tripod. Don't even bother holding it by hand because you're going to have lots of problems there. Let's just prevent that problem from even happening. And I can lay a load of constraints, and they would have competence without comprehension, right? But they would always be pushing back at me and saying, oh, I want to try this and I want to try that, because they don't know why those constraints are. I understand it because I understand the space of possibilities and I know why those constraints came to be.

我同意。就像你通过经验学习——你的经验教会了你这些——而他们在从你的经验中学习。他们自己不实验。

I agree. It's like you learn by experience — your experience taught you that — and they are learning from your experience. They do not experiment themselves.

对，比如 SMT——我是说你提到了 Z3——如果你向大语言模型问关于 SMT 实现的问题，你会得到教科书式的解释，但大语言模型从没试过它们。它是在重复写论文的人的经验，对吧？这正是你说的：它们在重复，而不是自己尝试、自己实验。

Yeah, for example SMT — I mean, you mentioned Z3 — if you ask questions about SMT implementation to large language models, you're going to get exactly the textbook explanations, but the large language model never tries them. It's repeating the learnings from people that wrote the papers, right? It's exactly what you said: they're repeating, they're not trying, experimenting themselves.

对，这部分肯定是缺失的。但感觉它很丰富——我不觉得这里有障碍。人们会去尝试的，对吧，朝着这个方向改进语言。

Yeah, this part for sure is missing. But it feels enriched — I don't see an obstacle here. People will try that, right, to improve the language in this direction.

我对此很纠结，因为有能力却没有理解不一定是坏事，因为我们现在写的是有智能的软件。过去我们写的软件只做它该做的事——你这么做就行——而现在有了一些灵活性。所以我们放入一些约束，然后在那些约束之内有一些适应，我们可以把它当作工程问题来控制。但这些约束真的很好。比如，有些东西是我们已经弄明白的，这就是为什么它们在我们的文化语汇中留存下来——某些算法、某些思维方式。坦率地说，让 AI 从头重新发现这些东西是浪费时间。

I'm so torn on it because competence without comprehension is not necessarily a bad thing, because we're now writing software which is intelligent. In the olden days we wrote software which just did exactly what it was supposed to — here's what you do — and now there's some flexibility. So we place some constraints in, and then within those constraints there's some adaptation, and we can control that as an engineering problem. But these constraints are really good. For example, there are certain things that we've just figured out, and that's why they've survived in our cultural lexicon — certain algorithms, certain types of thinking. And frankly, it would be a waste of time to make the AI rediscover those things from scratch.

所以，是的，是的。

So yes, yes.

边做边学会给你新视角，对吧？AI 可以通过自己边做边学获得新视角，不是依赖什么现成的东西，而是自己边做边学，也许更新自己的权重，这是可以想象的。

Learning by doing gives you new perspective, right? AI can get new perspectives by learning by doing itself, not relying on what widgets, but learning by doing itself, maybe updating their own weights, and that's conceivable.

也许这只是算力的问题。

And maybe it's just a matter of computation.

是的。也许如果我们真的有一个真正在做权重适应的智能体社会——

Yes. And maybe if we did have a society of agents that were actually doing weight adaptation—

但那会相当困难，某些方面甚至可能很危险，因为每六个月在平台上训练一次的大胖模型的好处是，我们可以在上面设置安全护栏，而且至少只有一个模型需要检查。

But it would be quite difficult and possibly dangerous in some ways, because the good thing about having big fat models that are trained every six months on a platform is we can put safety guardrails on there, and at least there's only one model to check.

想象一下——这也是我感兴趣的问题：平台所有者应该在多大程度上负责，而个体工程师又该负多少责任。因为如果我做一个复杂的智能体式系统，现在已经到了我认为任何人都不应该在生产环境中部署 fable 级模型的地步。所以也许在开发和研发阶段你需要更多智能，然后工程师施加约束，之后它应该达到介于普通软件应用和 AI 之间的状态。那么也许我们在生产环境中会使用智能较低的模型。但你认为工程师对某种退化行为负有多大责任？

Just imagine—this is something that interests me as well: the extent to which platform owners should be responsible versus individual engineers. Because if I make a sophisticated agentic system, it's already got to the point now that I don't think anyone should be deploying fable-class models in production. So maybe during the development and R&D phase you need more intelligence, and then the engineers place constraints in, and then it should get to the point where it's halfway between a normal software application and an AI. So then maybe we would have a lower intelligence model in production. But how much responsibility do you think the engineers have for kind of degenerate behavior?

嗯，你谈到的主要不同场景是应用内嵌 AI 的场景，对吧？如果是这种场景，我认为设置护栏非常重要，对吧？而且更好的是，如果你的护栏用 Lean 这样的系统验证过——你证明了护栏的性质。有些人在谈论未来要有经过验证的沙箱。是的，我很想看到那个。在我看来，我总是用 AI 开发不包含 AI 的软件。它不包含 AI，对吧？这是更安全的场景，对吧？很多人就是这样用的。他们构建应用，但应用本身不内嵌 AI。这是更安全的场景，对吧？所以你是在对抗应用中的 bug，而不是在 AI 周围设置护栏。

Well, the main different scenarios you are talking about is a scenario where the application has AI embedded insights, right? If you have this scenario, I think it's super important to have guardrails, right? And even better if your guardrails are verified using a system like Lean—you're proving properties about the guardrails. Some people are talking about having verified sandboxes in the future. Yeah, I would love to see that. In my mind, I always use AI to develop software that does not contain AI. It does not contain AI, right? This is a much safer scenario, right? And many people are using it like that. They build applications, but the applications themselves do not have AI embedded in them. And this is a much safer scenario, right? So you're fighting against bugs in the application, not putting guardrails around this AI.

如果我让 AI 生成一些 Lean 代码，然后 Lean 证明了它，人类仍然是作者吗？5 年后人类还会在其中扮演有意义的角色吗？

If I get AI to generate some Lean and then Lean proves it, is the human still the author and will humans play a meaningful part of this in 5 years' time?

很难说，对吧？我的意思是，一年前我无法预测。我们无法预测到目前为止发生的事情，对吧？我的意思是，我甚至无法想象 5 年后。感觉它在加速。它比我们预期的要快得多。有时人们问我，你害怕被淘汰吗？我会感到如释重负。我的意思是，开发软件，那会感觉像任务完成了。我不必再自己做了。也许我可以只花时间实现那些不必工作的软件。这不会是世界末日。我希望。我想成为的一件事——我认为我们将永远在循环中，因为我们必须始终保留规范，说明软件应该做什么。那将永远是我们的责任。我们是受益于 AI 的人。我们是说这就是我们想要的人。我们会在某个地方，即使只是在规范层面说明我们想要什么。当然，人们可以创造场景，让 AI 超级智能。我们有机器人，我们和机器人说话我们想要什么，它们用自然语言去执行，它们很听话。它们完全按照我们要求的做，孩子们。但我们仍然是告诉它们做什么的人。我觉得未来我们总是会有某种角色。但我能看到令人兴奋的部分。我的意思是，有多少——作为一个开发者，我认识的大多数开发者有很多想法，但他们只实现其中一小部分，因为时间有限。我的意思是，他们没有时间实现所有想法，他们看到我的许多同事——他们看到最有——最有可能成功的——就像你在玩一个游戏，说努力与成功的几率，许多想法你丢弃说这概率很低这能成功。我的意思是，但有了 AI，我们可以尝试更多想法，对吧？我举他的例子——我的意思是，他不是在引起人们那种感觉，而是为了尝试想法，他派 AI 执行不同任务，看看哪些值得他花时间实现。这已经是一个巨大的胜利，对吧？我的意思是。

Really hard to tell, right? I mean, I couldn't predict one year ago. We could not have predicted what happened so far, right? I mean, I cannot even imagine in 5 years. It feels like it's accelerating. It's moving way faster than we expected. Sometimes people ask me, do you fear becoming obsolete? I would feel like relieved. I mean, developing software, it would feel like mission accomplished. I don't have to do it myself anymore. Maybe I can spend my time only with implementing softwares that do not have to work. It will not be the end of the world. I hope. One thing I want to become—I think we are always going to be in the loop because we have to keep always the specification saying what the software should do. That will be always our responsibility. We're the ones that are benefiting from the AI. We're the ones that saying this is what we want. We will be there somewhere even if it's just at the specification level stating what we want. Of course, people can create scenarios where the AI is super intelligent. We have robots and we talk to the robots what we want and they go in natural language and they are obedient. They do exactly what we ask, kids. But we're still the ones telling them what to do. And I feel like we are always going to be some role for us in the future. But I can see the exciting parts. I mean, how many—as a developer, most developers I know have many ideas, but they only implement a small subset of them because time is finite. I mean, they don't have time to implement all the ideas and they see many of my colleagues—they see the ones that have the most—the ones that are most probable to work—it's like you are playing a game saying the effort versus the chance it's going to work and many of the ideas you discard say this is very low probability this is going to work. I mean, but with AI we can try more ideas, right? I give the example of him—I mean, he's not by causing the sense people do but for trying ideas he sends the AI in different missions and sees the ones that are worthwhile his time to implement them. This is already a big win, right? I mean.

是的，这确实让我想到——因为我觉得很难看到未来，因为我们才刚刚开始发现什么是有意义的边界。但我认为人类确实有这种更深的理解，这意味着我们对什么是有趣的问题有更好的直觉，我们也更擅长这种提炼。所以我的意思是，甚至 Mathlib 为例，如果未来产生定理变得非常便宜，也许人类的角色将更多是关于提炼和结构。

Yeah, it does make me think about—because I guess it's so difficult to see the future because we're just starting to find out what the meaningful boundary is. But I think that humans do have this kind of deeper understanding and that means that we have better instincts for what are interesting problems and we're also better at this distillation. So I mean even Mathlib for example, if it becomes really cheap to produce theorems in the future maybe the human role would be more about kind of distillation and structure.

是的。是的。我能看到在不久的将来，人们会用 AI 维护证明，构造新的证明——那些无聊没人关心的证明——但关键的证明他们仍然会手写，因为他们希望它们美丽或具有某种特定结构，有利于教学、交流思想。提出路线图也将是人类的活动。Mathlib 中的内容不是——我们如何定义环和其他数学结构——这些都将由人类完成。有很多探索正在进行。例如，一个很酷的想法是——我见过人们提出这个想法——假设我开始构建整个数学库，会发生什么，对吧？它可能是垃圾。但我们如何控制这些性质？你的 Hcoming——他是这个 Formal Frontiers 背后的主要人物之一。这个想法是，控制过程的一种方法是拥有关键定理，这些定理陈述起来超级简单但需要大量数学来证明。如果 AI 成功构造了这个关键定理的证明，它就在做值得做的事情。一个例子是一个定理——我的意思是，你可以用自然数——你只需要自然数来陈述这个定理。它非常简单，但你需要大量数学来证明它。你可以说这是 AI 的一个里程碑。你可以构建你疯狂的库，但你必须达到那里。我的意思是，你必须向我展示你达到了那里，你可以有许多这样的里程碑，容易陈述但很难证明。如果 AI 成功构建了一个库，使你能够证明那个，也许值得我们花时间看看那里有什么，对吧？

Yeah. Yeah. I can see Mathlib in the near future people will use the AI to maintain the proofs, to construct new proofs—proofs that are boring that nobody cares—but the key ones they will still write by hands because they want them to be beautiful or have some specific structure that's good for teaching, for communicating ideas. Coming up with the roadmap also is going to be a human activity. What is in Mathlib is not—how do we define the rings and other mathematical structures—these are all going to be done by humans. There are lots of exploration happening. For example, one cool idea was—and I've seen people throwing this idea—let's say I start building the whole mathematical library, what's going to happen, right? It can be garbage. But how do we control these properties? Your Hcoming—he's one of the main people behind this Formal Frontiers. The idea is to have one way to control the process is to have key theorems that are super simple to state but need a lot of math to be proved. If the AI managed to construct a proof of this key theorem, it's doing something worthwhile there. One example is a theorem—I mean, you can write with the natural—you only need the natural numbers to state the theorem. It's very simple but you need a lot of math to prove it. You can say like this is a milestone for the AI. You can build your crazy library but you have to get there. I mean, you have to show me you got there and you can have many of these milestones that are easy to state but really hard to prove. And if the AI managed to build a library that allows you to prove that, maybe it's worth our time looking at what is there, right?

是的，我想 AI 中一个由来已久的辩论是纯连接主义与神经符号主义，我认为现在我们处于神经符号时代，这些智能体式框架令人难以置信。我认为它们是 AI 如此有效的原因，但仍有人只认为连接主义很好，但只是为了给这个话题增添一点风味。所以，我们长期以来有一种直觉，即向神经网络添加结构和约束会使它们更好。这就是 Google 在 2024 年国际数学奥林匹克竞赛中获得银牌时的直觉，他们使用 AlphaProof 自动形式化 Lean 代码并生成这些 Lean 证明。

Yeah, one of the age-old debates in AI I guess is kind of pure connectionism versus neurosymbolic and I think now we are in the neurosymbolic age and these agentic harnesses they are incredible. I think they're the reason why AI works so well but there are still folks who think that connectionism only is really good but just to put a bit of flavor on this. So, we've long had the intuition that adding structure and constraints to neural networks makes them better. And this was the intuition that Google had in 2024 when they won silver at the IMO using AlphaProof which auto formalized Lean code and generated these Lean proofs.

但有一个挺有意思的进展：去年他们拿了金牌，而他们用的只是一个纯粹的——我记得是一个智能体式 LLM，还是纯粹的——我记不太清了。但这很有意思，对吧？这些模型只是神经网络，没有任何硬性约束。一个例子是它们下棋时，据说表现越来越好，大约 91% 的情况下能生成合法走法。说实话，考虑到它只是一个像意大利面一样缠绕的神经网络，能生成这么多合法走法已经非常惊人了。但你怎么看这件事的未来？你觉得像 Google 这样的公司会以某种方式重新转向 Lean，还是说趋势是随着我们把规模扩大，它们会内化某些约束？

But there's been a bit of an interesting development, which is that last year they won gold, and they were just using a pure — I think it was an agentic LLM, or just a pure — I can't actually remember. But this is interesting, right? These models are just neural networks; they don't have any hard constraints. And an example of this is when they play chess, apparently they're getting better — they generate valid moves about 91% of the time. Which, frankly, given it's just a kind of spaghetti neural network, it's very impressive that it's generating these valid moves so far. But how do you see this going forward? So do you think that folks like Google will move back to Lean in some way, or do you think the direction of travel is that as we scale these things up, they're kind of internalizing some of these constraints?

好。我觉得你的问题可以从两个角度回答。一是像 AlphaProof 这样的技术——它遵循蒙特卡洛树搜索，是一种混合技术，你甚至可以说它是一种真正的神经符号技术——它是否划算，对吧？另一个问题是：我们到底需不需要形式化验证？我认为第二个问题的答案是肯定的。我的意思是，即使我们有一个 99.999999% 的情况下都能生成正确答案的模型，我们仍然想要一份证书。举个例子说明证明可以变得多庞大：OpenAI 证伪的那个单位距离猜想——Boris Alexeev 向 Lean 提交了一个证明——那是一份 120 万行的 Lean 形式化证明。没人想逐行检查这个证明，对吧？有一份证书是很好的。我认为拥有机器可检查的证书——这非常棒。至于走法——如果你用的是 AlphaZero 架构，走法，或者一个大语言模型说砰砰砰，这些是要走的招——你仍然有走法，对吧？只是你产生走法的方式不同。我认为拥有走法，在把数学看作一场游戏的视角下，这是有价值的，而且会一直存在，对吧？因为 AI 会合成一个形式化证明，那是一串走法，不管它是一个 LLM 智能体、一个由 LLM 控制的智能体，还是一个结合了某种神经网络的蒙特卡洛树搜索。哪个更好这个问题仍然开放。我的意思是，大家都很佩服。社区里，用 GPT-5.6 和 Claude Fable，我认为它们超过了所有使用蒙特卡洛树搜索的系统。但接着我们得问成本的问题，对吧？哪个更便宜？这周开会时我和一些做这些实验的同事聊过，他们告诉我情况并不清楚，因为使用蒙特卡洛树搜索混合方法的系统，每一步走法便宜得多，但它们走的步数多得多，因为走法更笨。LM 更贵，但它更快到达终点，对吧？某种意义上这仍然有争议。我可以想象未来在某些领域这种混合方法可行，LM 也可行；也有场景是我们把硬件改进得如此之好、如此便宜，以至于没人再费心用混合方法了——大家都只用大语言模型，或者类似大语言模型的东西。这部分仍然有巨大的争论，到底划不划算。

Okay. I think there are two ways to answer your question. One is whether techniques like AlphaProof — it follows the Monte Carlo tree search, it's a hybrid technique. You can maybe even say it's a truly neuro-symbolic technique for proving — whether this pays off or not, right? And the other one is: do we need formal verification at all? I think the answer to the second question is yes. I mean, even if we have a model that generates right answers 99.999999% of the time, we still want a certificate. Just to give an example of how proofs can get massive: the unit distance conjecture that OpenAI proved false — Boris Alexeev submits a proof to Lean — it's 1.2 million lines of Lean, the formal proof. Nobody wants to check the proof line by line, right? It's great to have a certificate. I think having certificates that are machine-checkable — this is excellent. Having moves — if you're playing with the AlphaZero architecture, the moves, or a large language model saying boom boom boom, these are the moves to do — you still have the moves, right? It's just how you produce the moves is different. I think having the moves, in the game of viewing math as a game, this is valuable and will stay, right? Because the AI will synthesize a formal proof that's a sequence of moves, independently of the fact of whether it's an LLM agent, an agent controlled by an LLM, or a Monte Carlo tree search combined with some kind of neural network. The question of which is still open. I mean, everybody's impressed. I mean, the community — with GPT-5.6 and Claude Fable, I think they outperform all these systems that are using Monte Carlo tree search. But then we have to ask the question of cost, right? Which one is cheaper? I was talking with some colleagues doing these experiments during the conference this week, and they told me it's not clear, because each move of these systems using the hybrid approach with Monte Carlo tree search — the moves are much cheaper, but they're making way more moves because the moves are dumber. The LM is more expensive but it gets there faster, right? In a way it's still debatable. I can imagine in the future that for some domains this hybrid approach works and the LM works; there are also scenarios where we improve the hardware so much that it's so cheap that nobody bothers with hybrid approaches anymore — everybody's just using large language models, or something like a large language model. This part is still a huge debate, whether it pays off or not.

Lean 的未来是什么？我想问题的第一部分是：你已经把 Lean 提炼了这么多，对吧？你想象下一个版本会是什么样子？另外，你想象在你离开之后，Lean 的遗产会是什么？因为你现在打造的东西已经是一种现象了。在你离开很久之后它还会存在。某种意义上它会继续演化。你怎么看这个过程展开？

What is the future of Lean? So I guess the first part of the question is: you've distilled Lean so much, right? And what do you imagine the next version would look like? And also, what do you imagine Lean's legacy will be after you're gone? Because you've built something now which is a phenomenon. It's going to be around long after you're gone. And in a sense it'll just continue to evolve. How do you see that process unfurling?

是的。嗯，还有很多工作要做，对吧？我的意思是，我们想大力改进的一件事是 Lean 作为编程语言，对吧？我们希望 Lean 能生成与 Rust 有竞争力的代码，对吧？尤其是操作数组的程序。那里会有大量投入。大量投入在 Lean 作为软件验证平台上。一件事是验证某个库之类的，另一件事是验证整个系统，对吧？那要大得多。我们想在那里投入，确保 Lean 能扩展。我们要确保一直跟上数学的增长，但数学的增长是由人类推动的。给个参照：数学从——到现在数学增长了 44%，但完成时间减少了 10%。这样我们让 Lean 越来越快，但现在 AI 在写数学，我们必须加把劲。我的意思是，库的增长可能远远快于我们持续添加改进的速度。我们需要 AI 来帮我们提升性能、跟上库的规模。所以可扩展性会是个大问题。我们如何支持一个一亿行代码的库？这是一个开放问题——Lean 作为编程语言、作为软件验证平台的可扩展性。然后是提升信任：我们想要一个经过验证的编译器。你从 Lean 生成的代码——人们不理解 Lean 的可信代码基，如果你只想证明定理，它要小得多；如果你只关心证明定理，你只关心内核。但如果你关心——假设你用 Lean 写了一个程序，你证明了它的某个性质，然后你生成一个可执行文件。今天可信代码基包括编译器，那比内核大得多，我们想证明这个编译器。我们想移除——未来我们想要一个经过验证的编译器，你不必信任我们把这个编译器实现正确了。不是因为我们有恶意，而是因为我们也会犯错。我的意思是，像所有人一样。缩小可信代码基将是今后的一项工作。我们想不断缩小它。AI 在发现漏洞、利用方式方面会越来越强。你想不断改进这一点，确保 Lean 是开发软件和数学的平台。关于遗产：我的意思是，即使我今天死了，Lean 也会继续。Lean 团队非常棒。那里的人能照顾好一切。甚至——是的，他们不需要我。我总是尽力帮忙。但即使我死了，这个项目也会继续。

Yeah. Well, there is still lots of work to be done, right? I mean, one thing that we want to improve a lot is Lean as a programming language, right? We want Lean to generate code that's competitive with Rust, right? Especially for array-manipulating programs. There will be a lot of investment there. A lot of investment in Lean as a platform for software verification. One thing is to verify some library or the other; the other thing is to verify full systems, right? I mean, that's much bigger. We want to invest there, make sure this Lean scales. We want to make sure that we have been keeping up with math growth, but math growth is by humans. Just to give some perspective: math from — and now math grew 44%, but the completion time reduced by 10%. This way we are making Lean faster and faster, but with AI now writing math, we have to step up. I mean, the library can grow way faster than we can keep adding improvements. We will need AI to help us to improve the performance and keep up with the size of the library. So scalability will be a big issue. How do we support a library that's 100 million lines of code? This is an open — the scalability of Lean as a programming language, as a software verification platform. And then improving trust: we want to have a verified compiler. The code you generate from Lean — people don't understand that the trusted code base for Lean, if you only want to prove theorems, is much smaller; you only care about the kernel if you only care about proving theorems. But if you care about — suppose that you wrote a program in Lean, you prove a property about it, and you generate an executable. Today the trusted code base includes the compiler, which is much bigger than the kernel, and we want to prove this compiler. We want to remove — in the future we want to have a compiler that has been verified, and you do not have to trust us that this compiler was implemented correctly. Not because we are malicious, but because we make mistakes. I mean, like everybody. Reducing the trusted code base will be an activity from now on. We want to keep reducing it. AI is going to keep getting better and better at finding vulnerabilities, exploits. You want to keep improving that, making sure that Lean is a platform for developing software and math. About legacy: I mean, even if I die today, Lean will continue. I mean, the Lean team is amazing. I mean, the folks there can take care of everything. Even — yeah, they don't need me. I'm always trying to help. But the project would continue even if I die.

回到 2013 年，我的意思是，即使在你最疯狂的梦里，你想象过它会像今天这样吗？

And back in 2013, I mean, even in your wildest dreams, did you imagine that it would be anything like it is today?

没有。没有。没有。即使在我最疯狂的梦里，我也从没想象过陶哲轩会用 Lean，对吧，还就此做演讲。从没想象过。

No. No. No. Even in my wildest dreams, I never imagined that Terence Tao would be using Lean, right, and giving talks about that. Never imagined that.

我觉得我们是在为非常安全攸关的系统搭建一个平台，而证明将由人工完成。有些人说我很幸运——也许我确实幸运。把它做成交互式对 AI 来说很棒。Lean 是个黑箱；AI 无法影响它，无法引导 Lean，但它可以引导 Lean。对。

I felt like we are building a platform for very safety-critical systems, and the proofs would be done by hand. Some people claim I'm lucky — maybe I am. Making it interactive was great for AI. Lean is a black box; the AI cannot influence it, cannot guide Lean, but it can guide Lean. Right.

我真的很幸运。这么多了不起的人——Jeremy，遇到 Mario，我是在一个冷门会议上发现他的。Sebastian、Yim Bretoner、Kim Morrison——这么多人，所有这些核心成员。所有同事，太不可思议了。Kevin Buzzard 出现了，Kevin Hartnett 产生了兴趣，写文章。也许我是世界上最幸运的人。

I was really lucky. So many amazing people — Jeremy, meeting Mario, I found him at an obscure conference. Sebastian, Yim Bretoner, Kim Morrison — so many, all these folks at the core. All the colleagues, it's incredible. Kevin Buzzard showing up, Kevin Hartnett taking an interest, writing articles. Maybe I'm the luckiest person in the world.

我昨天看了一个 computer file 的视频。有个很棒的人在用一种策略做重言式检测归约。但不管怎样，重点是那挺吓人的。有很多教程视频，人们以百万英里的时速过一遍，做这个做那个。对于那些初次接触 Lean 时被吓到的人，你会说什么？

And I watched a computer file video yesterday. There was a wonderful chap using a tactic for tautology detection reduction. But anyway, the point is that it was quite intimidating. So there are a lot of tutorial videos and people are going through a million miles an hour, and they're doing this and they're doing this. What would you say to people for whom the initial shock is quite intimidating when using Lean?

嗯，对软件开发者，我建议先把 Lean 当作编程语言来用。就写代码。忽略证明。一开始不要尝试证明。先写代码、玩一玩、执行。等你对 Lean 语法熟悉了，再进入下一步：开始尝试证明你代码的一些简单性质。

Well, for software developers, I would recommend starting to use Lean as a programming language. Just write code. Ignore the proofs. Don't try proofs at the beginning. Start writing code and playing, executing. Then when you're comfortable with the Lean syntax, you go to the next step: you start trying to prove simple properties about your code.

我告诉每个人的另一件事：把 AI 智能体放在身边。它们知道很多很多——它们了解关于 Lean 的一切。它们比我更懂 Lean。它们能解释不是自己开发的扩展；Lean 是可扩展的。它们了解所有扩展，而且它们会读文档。很少有用户读文档。AI 会读，然后解释给你听。

Another thing that I tell everybody: have your AI agents around. They know lots and lots — they know everything about Lean. They know Lean better than I do. They can explain extensions that they did not develop; Lean is extensible. They know about all extensions and they read the documentation. Very few users read the documentation. The AI reads it and can explain it to you.

你可以告诉 AI 你的背景。比如“软件开发者”很笼统。如果一个软件开发者一直用 Haskell 或 Lisp，学 Lean 会容易得多，因为它们都是函数式编程语言。但假设你告诉 AI：“我是 C 开发者或 Java 开发者。”AI 现在会校准解释，针对你的背景定制，它们在一步步教你 Lean 方面非常有效。

You can tell the AI your background. For example, "software developer" is vague. If you have a software developer who has been using Haskell or Lisp, it's going to be much easier to learn Lean because they are all functional programming languages. But suppose you tell the AI, "I'm a C developer or a Java developer." The AI will now calibrate the explanations, customized to your background, and they're really effective at teaching you Lean step by step.

如果你打开一个视频，里面有很多策略，像游戏里的招式——在证明定理的游戏里——你可以问 AI：“给我解释一下这个。以我现有的背景——告诉我，在我尝试理解这个例子之前，我应该先知道什么。”它真的很擅长这个。

If you open a video that is very overwhelming with many tactics — like moves in a game, in the game of proving theorems — you can ask the AI, "Explain to me this. The background I have — tell me what I should know before I even try to understand this example." It is really good at that.

Leo，能邀请你上节目是我的荣幸。非常感谢你的参与。

Leo, it's been a pleasure and an honor having you on the show. Thank you so much for joining us.

谢谢。

Thank you.