Kevin Hartnett 谈 Lean：形式化证明、AI 数学与理解的边界

简要描述Brief Description

Kevin Hartnett 与 Lean 社区成员探讨了形式化证明的历史、Lean 和 mathlib 的发展、AI 辅助数学、验证的局限，以及项目背后的人际关系。Kevin Hartnett and members of the Lean community discuss the history of formal proof, the development of Lean and mathlib, AI-assisted mathematics, the limits of verification, and the human relationships behind the project.

目录Table of Contents

• 直接开场：证明、代码，以及错误的问题
  Cold open: proof, code and the wrong problem
• 开普勒的橙子与无人能验证的证明
  Kepler's oranges and the proof nobody could check
• Thomas Hales，《开普勒猜想的证明》（《数学年刊》，2005）
  Thomas Hales, A proof of the Kepler conjecture (Annals of Mathematics, 2005)
• 数学家如何判断一个证明是否正确
  How mathematicians decide a proof is true
• 正确不等于有用
  Correct is not the same as useful
• 赞助商：Cyber Fund
  Sponsor: Cyber Fund
• Lean 是什么，以及它所信任的小型内核
  What Lean is, and the small kernel it trusts
• 从微软的 Z3 到 Lean
  From Microsoft's Z3 to Lean
• 关于 Lean 基础的争论
  The argument over Lean's foundations
• 一位研究人员面对不断增长的用户群体
  One researcher versus a growing user base
• 凯文·巴扎德的纸牌屋
  Kevin Buzzard's house of cards
• Mathlib：一场集体建谷仓式的协作
  Mathlib as a barn raising
• 完美拟完备空间的噱头
  The perfectoid-spaces stunt
• 舒尔策那篇无人读过的证明：液体张量
  Scholze's proof nobody had read: Liquid Tensor
• AI 能学会寻找证明吗？AlphaProof
  Can AI learn to find proofs? AlphaProof
• 2026年的人工智能数学与陶哲轩的实验
  AI mathematics in 2026 and Tao's experiment
• 等式理论项目（Terence Tao）
  The Equational Theories Project (Terence Tao)
• Lean 在人工智能数学中的地位
  Lean's place in AI mathematics
• AI 暴力穷举与恰当抽象的较量
  AI brute force versus the right abstraction
• 自动形式化的特洛伊木马
  Autoformalisation's Trojan horse
• 形式化鸿沟
  The formalisation gap
• 证明不等于理解。
  A proof is not understanding
• 集成地狱与 zlib 规范
  Integration hell and the zlib specification
• lean-zip（zlib 证明）
  lean-zip (the zlib proof)
• AI 软件生命周期中的验证
  Verification in the AI software lifecycle
• 精益背后的人文故事
  The human story behind Lean
• 生日漫步
  The birthday walk
• 告别
  Farewell

冷开场：证明、代码与错误的问题Cold open: proof, code and the wrong problem

菲尔兹奖得主彼得·舒尔策。他的证明不过是六页技术性计算，我们顶多也只是粗略浏览了一遍。他开始相信，实际上根本没人读过他的作品。The Fields Medalist, Peter Scholze. The proof was just sort of six pages of technical calculations that we had skimmed through at best. He'd become convinced that nobody had actually read his work.

我们发现，四位菲尔兹奖得主确实在《数学年刊》上证明过定理。严格来说，这个定理并不成立。显然，那些人懒得提 n 必须至少为 3。We found four Fields Medalists have actually proved theorems in the annals of mathematics. Strictly speaking, that theorem is not true. The humans hadn't bothered to mention that, obviously, n had to be at least three.

当你使用 Lean 这样的工具证明某个结论时，可以得到证明证书。然后，你可以用一个算法来检查证明是否正确。机器会说证明是正确的。When you prove something using a tool like Lean, you can get certificates. You have an algorithm then can check whether the proof is correct or not. The machine says it's right.

现在终于真的有某种东西读过它了。人工智能正向数学领域进军，这一点再清楚不过了。Something has now actually finally read it. AI is coming for mathematics. This is absolutely clear.

像 OpenAI 和 Anthropic 这样的公司正在做数学，然后只是把它翻译成 Lean。数学家对此反应各不相同，从——你知道——只能说是悲痛的反应，到“我能让机器来证明东西吗？”Companies like OpenAI and Anthropic are doing mathematics and then just translating it into Lean mathematicians have had various different reactions to this, ranging from you know, what could only be described as grief Can I make a machine proof stuff?

当然。不过我想弄明白这件事，对吧？Sure. But I'm interested in understanding it. Right?

而最终还是得由我来理解它。它可以输出数百万个可能的证明，但你接下来需要迅速从中筛选出可信或正确的那些。Lean 可以告诉你哪些证明符合要求。And I'm still the one who has to understand it. It can output millions of potential proofs but you need to then quickly sort among them to the ones that are plausible or correct. Lean can tell you which ones those are.

但经过检查的证明仍然可能证明错了东西。关键在于思想，在于理解。But a checked proof can still be a proof of the wrong thing. It's about the ideas. It's about the understanding.

你知道吗？这是 GitHub 仓库。想看的话可以去看看之类的。You know? Here's the GitHub repo. Read it if you want kind of thing.

有人想要那个吗？你在计算器上把两个数字相乘，就会得到一个结果。你就相信计算器给出的结果。Does anyone want that? You multiply two numbers on a calculator, you get a result. You just take the calculator's word for it.

没人会检查的。Nobody's gonna check it.

开普勒的橙子与无人能验证的证明Kepler's oranges and the proof nobody could check

四百年前，约翰内斯·开普勒在一家蔬果店里萌生了一个有趣的想法。他看着橙子以金字塔形堆叠在一起，便想到这种排列方式或许可以证明是可能达到的最密集排列。four hundred years ago when Johannes Kepler was in a greengrocer, he had an interesting idea. He was looking at the way the oranges were stacked on top of each other in a pyramid structure, and he thought that might be provably the densest possible configuration.

Thomas Hales，《开普勒猜想的一个证明》（《数学年刊》，2005 年）Thomas Hales, A proof of the Kepler conjecture (Annals of Mathematics, 2005)

遗憾的是，他无法确定自己的想法是否正确。快进到大约1990年，这就成了开普勒猜想。Unfortunately, it was impossible for him to know for sure whether his idea was correct. So fast forward to about 1990. This had become Kepler's conjecture.

这是数学领域最有趣的问题之一，许多著名数学家都曾花费数十年试图解决它，但说实话，进展并不大。如今，两位数学家托马斯·黑尔斯和塞缪尔·弗格森将它归结为1762种组合。那时候，计算机的速度慢得惊人。It was one of the most interesting problems in mathematics, and many famous mathematicians had spent decades trying to solve it, honestly, without making too much progress. Now, two mathematicians, Thomas Hales and Samuel Ferguson, they reduced it to 1762 combinations. Now, back in these days, computers were incredibly slow.

所以，几乎每个案例都得单独处理：他们必须编写一个经过疯狂优化、包含大量启发式方法的计算机程序，来检查交叉情况等等，从而逐一证明每种情况的比率都低于约 0.74，也就是最优的金字塔式摆放方式的比率。凯文·哈特内特在他的新书《代码中的证明》里讲述了这个故事。这本书讲的不只是橙子和开普勒猜想，但故事确实是从这里开始的。So almost on a case by case basis, they had to write this insanely optimized computer program with lots of heuristics doing intersection checking and so on to individually prove that each one was less than about 0.74, which is the ratio of the optimum, you know, pyramid placement. Kevin Hartnett tells this story in his brand new book, Proof in the Code. Now, the book isn't just about oranges and, Kepler's conjecture, but that's certainly where it starts.

不过，这本书的主旨主要是讲一位名叫 Leo de Moura 的先生，他是 Lean 的创造者；书中还讲述了他与许多合作者一路走来、历经波折而又精彩的历程，最终让 Lean 发展到今天的样子。他还提到，Thomas Hales 这个人曾在墙上贴着一张纸。纸上的每一个图案都代表一种构型，而随着密度逐渐趋近于 0.74，这些构型也变得越来越难。But, the thrust of the book is mostly about this gentleman called Leo de Moura, who is the creator of Lean and the tumultuous and interesting fascinating journey that he went on with many of his collaborators to get to where Lean is today. And he was saying how this guy Thomas Hales, he actually had a bit of paper on his on his wall. And every single one represented one of these configurations, and they became harder and harder as the density converged towards naught 0.74.

他花了很多很多很多年才做到这一点，最终终于成功了。因此，他为这些球的每一种可能排列都编写了一个计算机程序，总共 1,767 个，他欣喜若狂。于是，他把这项工作发表在《数学年刊》上，期待着大家为他欢庆——毕竟，他刚刚证明了开普勒猜想。And it took him many, many, many years to do this, and eventually he did it. So he had 1,767 computer programs for every single configuration of these balls and he was elated. So he published his work to the Annals of Mathematics expecting a celebration that he had just, you know, proven Kepler's conjecture.

遗憾的是，事情并没有那样发展。Unfortunately, that's not what happened.

他把这份证明直接投给了《数学年刊》——这个领域最负盛名的期刊。编辑们基本上不知道该如何审稿，也不知道该怎么把它送给其他数学家核实其正确性，于是这份证明就搁置了很多年，始终没有真正被判定为真还是假。因为你想想，很多年前，数学证明的做法都处在抽象之山的高处。人们会提出这些非常高层次的论证，而某些论证此前已经得到证明这一点，往往被视为不言自明。He dumps this proof on the journal on the editors of the Annals of Mathematics, the most prestigious journal in the field and they essentially don't know how to referee it, how to kind of send it out to other mathematicians to verify its correctness and it languishes for like many years without actually being kind of determined true or false. Because if you think about it, many years, the way mathematical proofs were done were high up the abstraction mountain. So they would make these really high level arguments and it would just go without saying that certain arguments had been proved before.

因此，你不必一步一步地进行，而且整个过程非常、非常简洁。提交论文给期刊后，他们可以审阅论文，也可以核查你的工作。但这次情况不同。So you didn't need to go step by step and it was very very parsimonious. And when you submitted your paper to a journal, they would be able to review it and they would be able to check your work. But this was different.

它的内容实在太多了，几乎没法一一核对。征得凯文同意后，我想从他的书里读几段给大家听，让大家稍微感受一下这个故事。那我们开始吧。The sheer volume of it made it almost impossible to check. With Kevin's permission, I'm going to read out a few bits from his book just to give you folks a little flavor of the story. So here we go.

审稿人查看的证明每个部分似乎都正确，但整个证明却像一座庞大的计算大厦，深深埋藏在计算机代码之中；人们很难弄清这些部分如何彼此衔接，也难以判断它们最终是否真的得出了海尔斯声称已经证明的结论。1998年夏天，海尔斯完成证明时，曾设想运用他为开普勒问题开发的方法，去攻克其他类似问题。数学研究往往就是这样。Every part of the proof that reviewers looked at seemed correct, but the proof as a whole was such a sprawling edifice of calculations buried deep in computer code, and it was hard to determine how they all hung together and whether in the end they yielded the proof Hales claimed they did. When Hales had finished the proof in the summer of 1998, he had imagined he would use the methods he had developed for Kepler to attack other similar problems. That's how it goes in math.

解决一个难题的方法通常也适用于解决其他难题。然而，随着审查过程迟迟没有结果，哈尔斯改变了主意。Methods that solve one hard problem are generally good for solving others. Yet as the review process dragged on without resolution, Hales changed his mind.

他没能让数学界验证他的开普勒猜想证明。为什么他会在把同样的方法应用于其他问题时遭遇挫折？这位是 Lean 的创始人 Leo Demora。这篇论文被接收时附带了一条免责声明，大意是：“我们有百分之九十九的把握认为这个证明是正确的。”He couldn't get the math community to verify his proof of Kepler's conjecture. Why would he caught frustration by applying the same methods to other problems? This is Leo Demora, the creator of Lean The paper was accepted with a disclaimer saying something like, we're ninety-nine percent confident this proof is correct.

但随后，Tom 开始使用证明助手。这一切都发生在 Lean 出现之前。他用 HOL Light 和 Isabelle 来完成这项工作，但这仍然是一个里程碑。But then Tom starts using proof assistants. This all happened before Lean. He uses HOL Light and Isabelle to do this work, but it was a milestone.

我是说，这是一个重大成果，已经在证明助手中被形式化了。汤姆因解决开普勒猜想和使用证明助手这两件事而闻名。对吧？I mean, it was a big result that has been formalized in a in proof assistant. And Tom was famous twice for solving the Kepler conjecture and for using a proof assistant. Right?

在我们的论文中，数学界关心的……而他决定用 Lean 来做接下来的项目，这对 Lean 来说是件大事。但值得注意的是，这仍然让人觉得不够令人满意。In our paper that the math community cares. And the fact that he decided to do the next projects using Lean was a big deal on Lean. But the remarkable thing is that it still feels unsatisfying.

即使我们能够从第一性原理出发，完整地解决问题，仍然存在一种理解债务，因为我们无法同时把所有内容都记在脑海里。Even if we can solve problems from first principles end to end, there's a kind of understanding debt because we can't hold it all in our brains at the same time.

数学家如何判断一个证明是正确的How mathematicians decide a proof is true

那么，数学家如何知道一个证明是正确的？他们又如何相信一个新定理，并将其作为输入用于进一步的证明呢？这在很大程度上是一个社会过程。他们，他们大致已经对哪些方法行得通有了共识。So how do mathematicians know when a proof is correct when they can trust a new theorem and then use that as an input into additional proofs? It's very much a social process. They, they kind of have a general understanding for what works already.

他们算是了解证明背后的人，也多少能相信这个人懂得事情应该怎么做。然后他们就可以检查证明。They kind of like know the person behind a proof. They can kind of like trust that this person kind of understands the way things should go. And then they can check a proof.

他们可以检查论证中各行的类型，但不一定每次都会检查所有细节。大多数情况下，这种做法是行得通的，尤其是当证明与现有知识体系比较接近、只是比我们已经确认属实的内容略微推进一步时。是的。They can check the kind of the lines in the argument but they don't necessarily check every last line all the time. And for the most part that works especially when proofs are kind of close to the existing body of knowledge when they kind of go just incrementally beyond things we already understand to be true. Yeah.

我的意思是，假设这是个很基础的小白问题：为什么证明某件事很重要，而不只是知道它是真的？I mean, suppose, like, a fundamental noob question is, why does it matter that we can prove something versus just know something is true?

嗯，我觉得主要的一点是，当你使用 Lean 这样的工具证明某件事时，可以得到证明证书。然后，你可以用一个算法来检查证明是否正确。比如在数学领域，这有助于建立信任。我的意思是，你可以和从未见过的人合作。Well, I I think the main thing is that we can when you prove something using a tool like Lean, you can get certificates. You have an algorithm then can check whether the proof is correct or not. for math, for example, this is useful for trust. I mean, you can collaborate with people you never have met.

我觉得，即使在人工智能出现之前，数学界的很多人就已经为此感到兴奋了。这就像是在说：“哦，哇！我甚至可以和高中生一起合作，他们也能为我的项目做出贡献。”I think many people in the math community got excited about that even before AI. It's like saying, oh, wow. I can work even with high schoolers, and they can contribute to my projects.

我不需要检查他们的证明是否正确。大型数学项目可以看作工程项目。比如 Johan Commelin，他是一位非常硬核的数学家，也是一名软件工程师。I don't need to check if their proofs are correct or not. a big math projects, you can view as engineering projects. I mean, Johan Commelin, for example, he's a really hardcore mathematician. And he he's a software engineer.

他不知道这一点，但他是一名软件工程师。他会把大型项目拆分成更小的部分，其他人可以负责完成这些小部分。He doesn't know, but he's a software engineer. He breaks big projects in smaller pieces, and people can fill the smaller pieces.

他就像是这个项目的架构师。人们开始填补漏洞，他就不需要手动检查了。对吧？He's like the architect of the project. And people start filling the holes and he doesn't need to check manually. Right?

当然，他之后会再看看自己是否能让人们继续维护这个证明。但你不必一直纠结这个证明是否正确。他知道这个证明是正确的。Of course, he will look later for to see if he's he can people can maintain this proof later. But you don't have to keep thinking about is this the proof is correct or not. He knows the proof is correct.

他可以整理和改进，但证明是正确的。这很有价值。He can clean up, improve, but the proof is correct. This is valuable.

正确不等于有用。Correct is not the same as useful

今年早些时候，我在墨尔本和我们最喜欢的范畴论学家 Paul Lessard 见了面。我们想追溯其来源，想知道为什么。对吧？Earlier this year in Melbourne, I caught up with our favourite category theorist Paul Lessard we want provenance. We want to know why. Right?

如果你想聊符号人工智能，这才是我更感兴趣的地方。真正有意思的是，我不满足于它只是不出错，因为那还远远不够。我想知道它为什么会得出某个特定的答案。And that's the thing that I'm much more interested with if you wanna talk about symbolic AI. The thing that's interesting is I don't want merely things that don't get it wrong because, like, that's still not enough. I wanna know why it comes up with a particular answer.

我想知道原因。托马斯·黑尔斯的证明极其冗长，而且很复杂。I want the reason. Thomas Hales' proof was extremely verbose. It was complex.

他是在逐个实例地展开讲解，不像之前那些证明那么抽象。这让你想起什么了吗？是的。He was going through on an instance by instance basis, and it wasn't very abstract like the proofs that came before. And does that remind you of anything? Yes.

如果你现在看看 AI 的证明，它们也有类似的特点。对吧？它们看起来有点像一团意大利面，我们完全看不懂，这让人感觉不太满意。If you look at AI proofs now, they have a similar property. Right? They are they look a bit like spaghetti, and they're inscrutable to us, and that doesn't give us a very satisfying feeling.

那么，我们能说它们仍然正当吗？它们仍然和抽象版本一样好吗？嗯，他既然已经解决了这个问题，它们就不会因此显得不那么正当。So can we say that they are still legitimate? Are they still as good as the abstract versions? Well, it's not less legitimate because he settled the question.

我觉得，评估一项新数学结果价值的一种方式，是看它能否促成更多结果。你在推进论证的过程中，是否创造了新的概念、抽象或定义，而这些东西后来能广泛用于解答其他问题？就 Hales 的情况而言，我是说，他有一些想应用于其他问题的计算方法，但他并没有创造那种具有广泛意义的新数学。I think one thing that one way in which you can kind of like assess the value of a new mathematical result is it like does it enable additional results? Do you invent new concepts, new abstractions, new definitions in the process of prosecuting an argument that then have like widespread utility for answering other questions? In Hales' case, I mean there were some computational methods that he would have wanted to apply to other problems but he was not inventing kind of like broadly new mathematics.

从某种意义上说，他用的方法相当基础，他自己也多少承认了这一点。所以，他并不像安德鲁·怀尔斯那样创造新的数学。怀尔斯看到费马大定理时，不得不发明一些非常强大的新概念，从而开辟了这一领域的全新分支。In a certain sense the techniques he used were like fairly elementary, he himself kind of acknowledges that. So he was not creating new math in the same way that like Andrew Wiles had to create new math when he saw Fermat's Last Theorem where he had to like invent some very like powerful new concepts that just opened up entirely new branches of the field.

所以，Hales 的 Hales 的证明并不是那样的。因此，生成不受我们对可解释性的追求所限制的证明，可能是有用的。但一旦谈到比如真正做数学，我还是希望——我仍然愿意相信，你知道，人类的理解仍然是其中的核心。So Hales' Hales' proof was not like that. So there's utility probably in the generation of proofs that are not constrained by our desire for interpretability. But once you talk about, like, doing actual mathematics, like, that's I'd like I still like to think that, you know, the human understanding is still centered in this.

可能不是，但我觉得那些那些在某个时候是不同的任务。就像，我能让机器证明一些东西吗？当然可以。It may not be, but I think those those are different quests at some point. It's like, can I make a machine proof stuff? Sure.

但我感兴趣的是，嗯，理解它。对吧？而且我还是那个必须理解它的人。But I'm interested in, like, understanding it. Right? And I'm still the one who has to understand it.

人们之所以对此有所抵触，是因为数学家们总体而言并不认为——或者说过去并不认为——这种时间投入有价值。因此，Hales 花费二十人年将他的开普勒猜想结果形式化，最终得到的也只是对该结果正确性的确认。There is resistance because mathematicians don't see, by and large or didn't see the value in that type of time investment. So Hales invests twenty person years in formalizing his Kepler conjecture result and at the end all he gets out of it is assurance that the thing is correct.

不过，这就……这可远没有获得新的数学成果和新发现那么令人兴奋。尤其是在你已经相当确信事情是正确的情况下，就更没意思了。所以在大多数情况下，数学家知道事情对不对。Now that is like that's much less exciting than getting new math and new discoveries. It's especially not exciting in situations where you're already fairly confident that things are correct. So in most cases, mathematicians know when things are right or not.

他们并不担心正确性。有一个因素叫作德布鲁因因子，指的是在 Lean 中，为了对应一行非形式化数学内容（比如 LaTeX PDF 中的一行），需要编写多少行代码。这个比例很高，通常是二十比一，甚至更高。数学家通常看不出为什么要投入额外的时间，只为验证某件事的正确性。这正是阻力的来源。They're not troubled by correctness. there's a factor called the de Bruijn factor which is the amount of lines of code you need to write in lean for every one line of informal math like in a LaTeX PDF and it's very high, twenty to one often higher. Mathematicians don't generally see the reason to invest that additional time just to verify the correctness of something. So that's really where the resistance comes from.

他们看不到精益方法对他们最关心的事情——发现新的数学——有什么用处。They don't see the utility of lean for the thing they most care about which is discovering new math.

赞助商：Cyber FundSponsor: Cyber Fund

本期节目由 Cyber Fund 赞助。如果你正在 AI 前沿领域开拓，他们希望听到你的想法。Cyber Fund 相信，未来属于那些立志实现不可能之事的 AI 原生者。This episode is supported by Cyber Fund. If you're building at the frontier of AI, they want to hear from you. Cyber Fund believes the future belongs to AI natives who want to achieve the impossible.

这就是他们推出“AI 原生创始人修道院”的原因。这里为以 AI 原生速度创业的创始人提供专注纯粹、高效执行的环境，并向每支参与的团队提供 200 万美元。立即访问 cyber.fund 申请。And that's why they're introducing the Monastery for AI native founders. It's an environment of pure focus and rapid execution for founders operating at AI native speed, and they're offering teams $2,000,000 each to participate. Apply now at cyber.fund.

Lean 是什么，以及它所信任的小型内核What Lean is, and the small kernel it trusts

对于刚接触 Lean 的人来说，它是什么？它到底是做什么的？你能用 Lean 做什么？哦，Lean 既是一种编程语言，也是一种证明助手。folks who are new to Lean, what is it what is it all about? What can you do with Lean? Oh, Lean is both a programming language and a proof assistant.

你可以编写代码。Lean 实际上是用 Lean 本身实现的。但很酷的一点是，你可以证明代码的性质。You can write codes. Lean is actually implemented in Lean itself. But the cool thing is that you can prove properties about your codes.

你可以陈述数学定理，也可以证明它们，还可以像 Lean 的 mathlib 一样构建数学库。You can state mathematical theorems. You can prove them. You can build a mathematical library like Lean's mathlib.

因此，在凯文的《证明与代码》一书中，他对内核给出了精确定义。内核是 LEAN 这类交互式定理证明器的一个组成部分。交互式定理证明器有两个基本组件：逻辑基础，它决定如何表达各个思想以及它们如何相互作用；以及一个名为内核的检查程序，用于验证程序是否正确遵循逻辑基础的规则。So in Kevin's book Proof and the Code he gives a precise definition of a kernel which is a component in an interactive theorem prover like LEAN. An interactive theorem prover has two basic components: a logical foundation, which determines how ideas are expressed and interact with each other, and a checker program, called a kernel, which verifies that programs correctly adhere to the rules of the logical foundation.

内核回答了每个初次了解 ITP 的人都会问的第一个问题：如果 ITP 说一个证明是正确的，我怎么知道它没有出错？答案就在内核。我们有“小型可信内核”这个概念。Lean 非常庞大，有无数个 bug。The kernel answers the first question anyone asks when they learn about an ITP, which is that if the ITP says a proof is correct, how do I know it hasn't made a mistake? The kernel is how. we have the notion of a small trusted kernel. Lean's massive, has zillions of bugs.

对吧？但要信任我们在 Lean 中得到的结果，我们只信任内核。内核小得多。Right? But to trust our results in Lean, we only trust the kernel. That's much smaller.

对吧？对内核而言，最不可饶恕的错误就是把错误陈述验证为真，这远比把正确陈述判为错误糟糕。把正确陈述判为错误，只不过是造成了阻碍。Right? The cardinal sin for a kernel is to verify false statements as true, which is far worse than rejecting true statements as false. Calling true statements false merely creates a roadblock.

这确实令人不便。但把虚假陈述说成真话，就会为认可更多虚假陈述打开大门，而这些陈述都以最初的虚假主张为依据。到了那时，在内核中的错误修复之前，ITP 就毫无用处。It's an inconvenience. But calling false statements true opens the door to validating countless more false statements, all justified by the original false claim. At that point, the ITP is useless until the bug in the kernel is fixed.

多年来，Agda、Coq 和 Isabelle 等交互式定理证明器的内核都曾存在漏洞，使用户能够验证错误的命题。Over the years, ITPs such as Agda, Coq, and Isabelle had all contained bugs in their kernels that allowed users to validate false statements.

他的答案是独立验证：让用户构建自己的内核。为了让这一选择切实可行，de Moura 知道，他必须尽可能缩小内核的规模、简化其设计，并将代码行数压到最低。His answer was independent checking. Let users build their own kernels. To make this option realistic, de Moura knew he would need to keep the kernel as small and minimalistic as possible, comprising as few lines of code as he could possibly achieve.

在当时已有的交互式定理证明器中，de Moura 欣赏 HOL Light 的极简设计，因为它的内核非常小。Among the ITPs already on the market, de Moura admired the minimality of HOL Light, which had a very small kernel.

从微软的 Z3 到 LeanFrom Microsoft's Z3 to Lean

早在 2006 年，微软内部就有大量重复劳动。有些人在构建自己的定理证明器，有些人则在研究已经过时的定理证明器。就在那时，LEO 决定开始开发 Z3。Leo 开发 Z3，是为了提供一种系统化的方法来检查软件是否存在有问题的执行路径，并且可以在一定程度上以数学证明的形式进行检查。Back in 2006, there was loads of duplicate effort at Microsoft. Some were building their own theorem provers, some were working on obsolete theorem provers and it was at that point that LEO decided to start working on Z3. Leo built Z3 in order to provide a systematic way of checking that software had no bad pathways and he could kind of do it in the style of a mathematical proof.

比如，他可以用 Z3 在某种程度上证明这一点：你构建一条软件执行路径，将其表示为一系列变量，然后证明这些变量永远不可能取到某种恰当的值组合，从而使某个语句成立。如果你证明它不可能取到这些值，也就是说软件不可能到达那种状态或变量取值，那么你就能明确排除某个特定方向上的错误，至少是这样。Like he could kind of prove with Z3 where you construct you construct a pathway through the software as a series of variables and you prove that those variables can never take the right combination of values that would make a statement true. And if you prove that it cannot take, the software cannot arrive at that state, that set of variables, then you just have ruled out categorically a bug at least in this like one particular direction.

Leo 构建 Z3，旨在自动检查微软软件中的不同执行路径是否存在错误，并证明、保证其中没有错误。Z3 是一种称为自动定理证明器的程序，因为一旦完成设置，所有这些工作都会自动完成。此时几乎不需要人工输入。Leo built Z3 as a way to automatically check different pathways through Microsoft software for bugs, prove, guarantee that there were no bugs. Z3 is a type of program called an automated theorem prover because all of this work once you set things up is done automatically. There's not a lot of human input at that point.

Z3 相当强大。它发现了大量漏洞，并在 21 世纪初为微软省下了数亿美元。不过，在 Z3 大获成功之后，Leo 和他的合作者不只是把它用于微软的项目，还把它带去参加自动定理证明器竞赛。在这类竞赛中，来自世界各地的自动定理证明器齐聚一堂，在限定时间内解决一批问题；谁能最准确地证明这些问题为真或为假，谁就获胜。Z3 was quite powerful. It caught lots of bugs and saved Microsoft hundreds of millions of dollars in the early two thousands. Leo though, following the great success of Z3, not just for Microsoft but like he and his collaborator entered it into these automated theorem prover competitions where all the ATPs from all over the world come together and they're given a bunch of problems in a set amount of time and whichever ATP can kind of correctly prove true or false for those problems, most accurately wins.

Z3 曾是该领域的世界冠军。因此，他本质上已经登上了自动定理证明器领域的顶峰，但他也对自动定理证明器技术的一些根本局限感到不满。比如，这类程序能够证明的内容范围有限。Z3 was the world champion at. So he essentially had climbed to the top of the automated theorem prover mountain but he also was dissatisfied with the kind of the fundamental limitations of automated theorem prover technology. Like there's kind of a limited range of things that programs of that sort can prove.

如果想把范围说得稍微宽泛一点，它们能够验证其正确性的知识范围是有限的。因此，他把注意力转向构建一种相关但更强大的程序，称为交互式定理证明器。它拥有一种表达能力丰富得多的语言，可以尝试编码并验证范围更广的真理；它之所以是交互式的，是因为人类用户可以引导程序，使其具备更强的表达能力。这让它变得强大得多。A limited range of knowledge that they can verify is correct if you wanna go a little broader. And so he turns his attention to building a related but more powerful type of program called an interactive theorem prover where you have a much richer expressive language that kind of just a wider range of truths you can try to encode and verify and interactive in the sense that the human kind of a human user can can nudge the program towards greater expressiveness. It makes it a much more powerful thing.

我的书归根结底讲述的是这样一个故事：de Moura 构建了 Lean 这个交互式定理证明器，用它以比 Z3 更丰富的方式验证软件程序的正确性；而数学家看到了它的潜力，某种意义上便将它接手过来。于是，ITP 首次突破圈层，成为一种更主流的数学工作方式。不过，由于 Lean 使用依赖类型论，它还能用于解决许多其他抽象数学领域中的问题，而且这些问题要复杂得多。what my book is ultimately the story of how Lean, this interactive theorem prover that de Moura builds to verify the correctness of software programs in a richer way than he could with Z3 gets in a sense co opted by mathematicians who see the potential in it and for the first time an ITP breaks through into a more mainstream way of working in math. But in Lean, because it uses this dependent type theory, it can be used for solving many, many other problems in abstract mathematics which are significantly more complex.

关于 Lean 基础的争论The argument over Lean's foundations

卡内基梅隆大学的数学家兼哲学家杰里米·阿维加德，多年来一直与利奥通信。我受过数学训练，具体来说，是一名逻辑学家。你知道，我喜欢逻辑的一点是，它介于数学、计算机科学和哲学之间。Jeremy Avigad, a mathematician and philosopher at Carnegie Mellon, has been corresponding with Leo for many years. I'm a mathematician by training, specifically a logician. And so, you know, what I like about logic is that it's somewhere between mathematics, computer science, and philosophy.

所以，在卡内基梅隆大学，我的主要任职部门是哲学系。证明助手最初只是我的一个爱好；大约在2000年，我开始摆弄它们，只是因为觉得它们很有趣，那已经是很久以前了。西海岸时间刚过午夜，德·莫拉给小组发了一封长邮件，缓和了他此前提出的一些担忧。So here at Carnegie Mellon, my primary appointment is in the philosophy department. Proof assistants started just as a hobby, just messing around with them because I thought they were interesting around the year 2000, so quite a long time ago. Just after midnight on the West Coast, de Moura sent a long email to the group softening some of the concerns he had raised.

如果我今天听起来太消极了，我很抱歉。他写道，我还在努力了解其他选择。我一直在阅读有关这些证明助手的资料，并研究它们的实现方式。I apologize if I sounded too negative today. I'm still trying to understand the alternatives, he wrote. I've been reading about all of these proof assistants and studying their implementations.

当我质疑是否需要依值类型或其他任何特性时，是因为我确实对 HOL Light 的设计和实现印象深刻。在我看来，它远比其他系统优雅。他承认，这种看法与 Avigad 的观点相悖。When I questioned the need for dependent types or any other feature, it's because I'm really impressed with HOL Light's design and implementation. In my opinion, it's the most elegant by far. He acknowledged that this perspective was at odds with Avigad's.

我理解 Jeremy 的观点：他说 HOL Light 不太适合做抽象代数。Lean 的设计当时还在实时讨论中。我想使用高阶逻辑。I understand Jeremy's point when he says HOL Light would be really inconvenient for doing abstract algebra. The design of Lean was being negotiated in real time. I want to use higher-order logic.

它的基础更简单，也更容易实现。对于许多软件验证任务来说，这已经足够了。对吧？It's a simpler foundation, much easier to implement. And for many software verification tasks, it's enough. Right?

但对于抽象数学来说，并非如此。要验证软件，拥有一个优秀的数学库很重要。例如，密码学需要大量数学知识，差分隐私也是一个例子。But for doing it abstract mathematics, it's not. it's important to have a good library math library for verifying software. For example, cryptography, we need a lots of math. Differential privacy is another example.

因此，即使你只关注软件验证，拥有一个优秀的数学库也很重要。So having a good mathematical library is important even if you only care about software verification.

在我看来，你有用户很重要。这就是用户想要的。我想要支持。我想让杰里米成为一名用户。In my point of view, you have it's important to have users. that's what the users wanted. And I want support. I want to have Jeremy as a user.

我知道其他人也会陆续出现，并最终有所收获。我的意思是，很多人，很多从事密码学研究的同事，都会这么说。比如，其中一位就是我的前同事 Cédric Fournet。I knew others would come and pay off. I mean, many people, many of my colleagues that work on cryptography, they say. For example, one of them is a former colleague of mine, Cédric Fournet.

他现在用 Lean。他跟我说：“你看，mathlib，也就是 Lean 数学库，具备我验证密码学所需的合适抽象。对吧？”He uses Lean now. And he told me, look, mathlib, the Lean Mathematical Library, have the right abstractions I need for verifying cryptography. Right?

我的意思是，正因为依赖类型理论提供了如此广泛的通用性，我们才有了一个表达能力更强、抽象恰当、也更整洁的库。是的，从长远来看，这确实很值得。So I mean, because of all the generality that's having dependent type theory provided, we have a library that's more expressive, that has the right abstractions, is cleaner. Yeah. It paid off long long term.

最终证明这是值得的。一开始增加了很多额外工作，而要把它做好也费了不少功夫。It paid off. It was a lot of extra work at the beginning. And to get it right, it was also lots of work.

不过我觉得这已经有回报了。But it's I think it's paid off.

我想，最大的分歧之一，以及最终你赢下的那场争论，就是你希望 Leo 支持这种依赖类型理论，因为它对解决你感兴趣的那类问题非常有用。在启动 Lean 项目之前，我曾在 2009 年和 2010 年工作过。我花了一年的学术休假，致力于形式化费特–汤普森定理。那是在一个名为 Rocq 的证明助手中完成的。I suppose one of the biggest tensions and ultimately the battle that you won was that you wanted Leo to support this dependent type theory because that was very useful for solving the types of problems that you were interested in. before starting the Lean project, I had worked in 2009 and 2010. I spent a sabbatical year working on the formalization of Feit Thompson theorem. And that is in a proof assistant known as Rocq.

而 Rocq 基于依赖类型理论。在此之前，我曾广泛使用 Isabelle，它是一种基于更简单的逻辑框架——简单类型理论——的证明助手。Isabelle 是一个非常出色的系统，因此在很多方面，它绝对是理想的选择。And Rocq is based on dependent type theory. Before that, I had worked with Isabelle extensively, which is a proof assistant based on a simpler logical framework called simple type theory. Isabelle is a wonderful system, and so for many things, it's it's absolutely ideal.

直到今天，它仍然拥有出色的自动化功能和自动化支持。因此，对于某些类型的数学问题来说，它确实是一个很棒的系统。It still to this day has excellent automation, automated support. So for certain types of mathematics, it was really a great system.

但对于某些类型的事物，你就会碰壁。因此，在现代数学中，数学家会谈论代数结构，你知道，这些结构是通过公理刻画的。它们确实无处不在。But then for certain types of things, you hit a wall. So, in modern mathematics, mathematicians talk about algebraic structures, you know, axiomatically characterized. It they're really ubiquitous.

存在这些由代数结构构成的复杂网络，而简单类型论并不适合处理它们。于是，在我使用 Rocq 工作了一年之后，我逐渐意识到，这正是能够开展这类数学研究的框架。我认为，其他曾尝试使用 Isabelle 和其他系统的数学家也得出了类似的结论：要做他们想做的数学研究，就需要这样一种表达能力极强的框架。There are these complex networks of algebraic structures, and simple type theory is just not good for that. And so after my year working with Rocq, it became clear to me that this was the framework that was capable of doing that type of mathematics. And I think other mathematicians who had experimented with Isabelle and other systems were coming to similar conclusions, that to do the mathematics that they wanted to do, they needed this very expressive framework.

所以，依赖类型理论的特点是，它非常强大，也极具表达力。不过我喜欢引用——你知道的——《蜘蛛侠》系列中的话。So the thing about dependent type theory is that it's very powerful, and very expressive. But I like to quote, you know, the Spider Man franchise.

你知道，能力越大，责任越大。你知道，这种语言功能非常强大，也很难实现。You know, with great power comes great responsibility. You know, the very powerful language. It's also very hard to implement.

它可能更难使用。有很多容易踩的坑，也有一些特殊边界情况。因此，这是一个更庞大、复杂且难以驾驭的框架。It can be more difficult to use. There are a lot of gotchas and kind of corner cases. And so it was a more weighty and complicated and difficult framework.

Leo刚开始这个项目时，追求的是简洁，你知道，就是一个非常简单、规范的基础。所以，他需要有人说服他，让他相信这种权衡是值得的。我想，你知道，最后他还是接受了。And when Leo first started the project, he was aiming for simplicity, you know, a very simple, formal, you know, foundation. And so he needed convincing there that the trade off was worth it. I think, you know, in the end he came around.

我的意思是，他现在是依赖类型论最有力的倡导者之一。你知道，没过多久他就会说，这真的很美妙。所以他认识到了它的好处。I mean, now he's one of the biggest proponents of dependent type theory. He, you know, you know, soon after, he would say that, you know, it's it's really beautiful. And so he recognized the benefits.

不过话说回来，作为一个外来者，而且你知道，他对灯丝也不熟悉，所以一开始确实需要有人说服他。But again, coming coming from the outside and, you know, without the filament familiarity, yeah, he needed convincing at first.

但最终，在 2013 年夏天，Leo 给 Jeremy 回了封邮件，告诉他：“我决定采用依赖类型论。”Jeremy 当时在匹兹堡的家里简直高兴得手舞足蹈，因为他知道，Lean 现在已经具备了让它在数学领域发挥作用的基础，也有望以他一直期待的方式成为一款有用的交互式定理证明器。作为开发者，这事挺有意思的。戴上开发者的帽子时，你通常会倾向于选择实现起来更简单的方案，却忘了自己有时也会成为这个工具的用户。But ultimately Leo emails Jeremy back during that summer of 2013 and tells him, I've decided to go with dependent type theory and Jeremy basically does a dance at home in Pittsburgh because he just knows the seeds are there now for Lean to be useful in math and the way he's always wanted an interactive theorem prover to potentially be useful. It's funny as a developer. When you're using the developer hats, usually, you want to go to whatever it's simpler to implement, and you forget that you sometimes will be the user of this tool too.

我总是在开玩笑，亲爱的。如果我戴着用户的帽子，我就想要这个功能；如果戴着开发者的帽子，我就不想要它。I always joke, honey. If I'm using my user hats, I want this feature. If using the developer hats, I don't want it.

哦，对。Leo 就是特别自我批评。我的意思是，在 Lean 的发展历程中，有很多这样的时刻：他有一些用户，他们很喜欢 Lean，而他说它糟透了。Oh, yeah. So Leo is like extremely self critical. I mean, just there there are many moments in the story of the development of Lean where he has some users and they love it and he says it's shit.

我的意思是，他只是觉得它糟透了。他看到的全是它的缺陷。他特别执着地想把这些缺陷修好。I mean he just thinks it's terrible. He all he sees is its flaws. He wants to very doggedly fix those flaws.

在微软，Leo 担心年度评级不佳会危及他的研究。他的经理从未给过他评级，但这种恐惧一直挥之不去。At Microsoft, Leo feared a poor annual rating would jeopardize his research. His manager never gave him one, but the fear persisted.

一位研究人员与不断扩大的用户群体One researcher versus a growing user base

Leo 只是一名研究员，是微软研究院的一名计算机科学家。他不是项目经理，也不是产品经理，没有一支工程师团队与他共事，只有他和一个想法。通过 Jeremy，Lean 很快就吸引了一批想要开始使用它的数学家。Leo is just a researcher, a computer science at Microsoft Research. He's not a project manager, he's not a product manager, he doesn't have like a team of engineers working with him, it's just him and idea. Through Jeremy, suddenly Lean very quickly gets a number of mathematicians who want to start using it.

他们很喜欢它，不觉得它烂；他们觉得它比 Leo 认为的好得多，但他们也提出了各种额外的功能需求。要是我们能做到这个，不是很棒吗？要是能做到那个，事情就会容易得多，不是吗？They love it, they don't think it's shit, they think it's way better than Leo does but they also have all these additional feature requests. Wouldn't it be great if we could do this? It would be much easier if we could do that?

我们能不能做一个更丰富一些的界面？Leo 想让用户满意。他在这方面特别以用户为导向。Can we have like a richer UI? Leo wants to please the users. He's extremely like users oriented in that way.

对他来说，要接收一条反馈尤其困难，特别是当他意识到这条反馈从根本上说是正确的，却还要忽视它。因此，他发现自己会迅速回应所有这些用户，而这些用户甚至不是他原本打算为其打造产品的对象；他们所做的事情，也根本不是他计划让 Lean 发挥作用的领域。It's very hard for him to receive a piece of feedback especially if he recognizes it's kind of fundamentally correct and ignore it. So he finds himself kind of responding rapidly to all these users who are not even the users he intended to be building for who are doing something that's not even what he planned lean to be useful for.

但他开始着手满足这些请求。我觉得他后来先是被邮件轰炸，接着又被 Slack 消息狂轰滥炸。他实在很难拒绝他们，但他因此变得非常沮丧，因为他觉得他们把他的付出当成理所当然。他觉得他们以为他比实际有更多时间，而最重要的是，他对 Lean 的发展方向有自己的愿景。But he starts fulfilling the request. I think he's like barraged by emails ultimately later by Slack messages. He can't really say no to them but he comes intensely frustrated because he feels like they're taking him for granted. he feels like they think that he has more time than he does and most importantly, he has like a vision for where he wants lean to go.

最终，Lean 有四个版本。我们现在用的是 Lean 4，但多年来一直用 Lean 2。Leo 看到了他希望它发展的方向，但他觉得自己很难抽出时间去实现，因为他一直在回答数学家提出的各种问题和咨询，这些基本上都属于用户支持问题。There ultimately are four versions of lean. We're currently on lean four but for years, you know, we're at lean two and Leo saw where he wanted it to go and he felt inhibited in his ability to find the time to do it because he was answering all these essentially like user support questions and queries from mathematicians.

Kevin Buzzard 的纸牌屋Kevin Buzzard's house of cards

最早采用 Lean 的人之一，也是 Lean 最热情的推广者之一，是伦敦帝国理工学院的一位数学家，名叫凯文·巴扎德。我叫凯文·巴扎德，是一名在伦敦帝国理工学院工作的数论学家。本世纪初，我花了一些时间抚养三个孩子。等这段时间过去，孩子们也能更多地照顾自己之后，我想重新投入艰深的数学研究。one of the earliest adopters of lean and kind of most enthusiastic evangelist for lean is a mathematician at Imperial College in London named Kevin Buzzard My name is Kevin Buzzard. I'm a number theorist working at Imperial College London. I spent some time at the beginning of this century bringing up three kids. when that was sort of over and they were able to look after themselves a lot more, I wanted to get back into doing hard research mathematics.

我意识到，有大量的材料需要我去补上。那段时间我好像经历了一场中年危机，因为我试着去读这些材料，却没法全部理解。我还会发现一些我认为是文献中的错误。后来我开始想，等等，我们究竟在做什么？这些东西非常抽象，看不出有什么直接的实际应用，所以我们似乎没有什么可以在现实中用来检验这些想法的东西。And I realized that there was a huge amount of material that I was gonna have to sort of catch up I had some kind of midlife crisis around that time because I was trying to read it, and I couldn't understand all of it. And I would find what I thought were mistakes in the literature. then I started thinking, well, wait a minute. Like, what are we like, what this is very abstract stuff, it's not immediately clear there's any sort of concrete applications, so there's nothing that we can sort of test these things on in reality.

如果它们不正确，那几乎……你知道，这些东西到底有什么意义？所以我经历了某种危机，开始思考：你知道，机器能不能用来验证数学？毕竟，技术发展得非常快。于是我就一路深入探索，看看外面有哪些软件声称能以超越人类的准确度验证数学。And if they're not right, then almost, you know, what is the point of this stuff at all? So I had some kind of crisis, and I started thinking, you know, would it be possible check mathematics using machines? Because, you know, technology is moving very fast. and so I went down some kind of rabbit hole, just kind of exploring the software that was out there that was claiming, you know, that it could check mathematics at superhuman accuracy.

它确实能够以超人的准确度检查数学内容，但问题在于，它检查的数学内容中有百分之九十九都是非常非常基础的知识，几百年、甚至可能几千年前就已经为人所知了。不过到了那个阶段，我有点着迷了，因为我意识到这是一种奇特的新数学方法，我以前真的从未见过类似的东西。And it absolutely could check mathematics at superhuman accuracy, but the problem was the mathematic ninety-nine percent of what it was checking was really, really basic material known hundreds or maybe even thousands of years ago. So the but by that stage, I kind of got hooked, cause I realized that there was this weird new way of doing mathematics, I'd never really seen anything like it before.

我开始意识到，实际上，在软件里做数学——尽管只是非常基础的数学——也特别有意思，和在纸上用笔做数学完全不一样。于是我就这么沉浸其中，突然间，最初那些问题都被抛到脑后了。我当时只想着：哦，这软件真棒。And I started to realize that actually, doing mathematics in the software, even though it was very basic mathematics, was a huge amount of fun very different to doing it on paper and pencil. And so then I was in this hole, and then suddenly the original questions just went out the window. Then I was just like, oh, this software is really great.

你知道吗？我们到底能让这个软件做些什么？当时，我们几乎只能让它做本科水平的数学题。You know? What can we actually get this software to do? And at the time, it was just like we could barely get it to do undergraduate level mathematics.

但因为用起来实在太有趣了，你知道，我最终就是这样转向的。到了2016年，凯文·巴扎德有时间重返 p-adic Langlands 纲领。一个名叫彼得·舒尔策的年轻才俊用完美空间改变了几何数论，而巴扎德也想成为这场革命的一部分。But because it was great fun using it, You know, that was how I ended up switching. By 2016, Kevin Buzzard had time to return to the p adic landlins program. A young talent named Peter Scholze had transformed the geometry of numbers with perfectoid spaces, and Buzzard wanted to be part of the revolution.

但在阅读了后续关于 Scholze 工作的论文后，他的热情逐渐变成了担忧。Buzzard 喜欢把每个细节都阐述清楚。他不喜欢含糊其辞，也不喜欢权威人士的保证——他称之为“长者们的意见”。而这种观点可能会在有前景的想法尚未得到充分定义之前，就认可它们。But as he read the papers that followed Scholze's work, his enthusiasm gave way to concern. Buzzard liked to see every detail spelled out. disliked vagueness and assurances from authority, what he called the opinion of the elders. And that perspective could bless promising ideas before they were fully defined.

但在他审阅的论文中，Buzzard认为，这种做法已经成了敷衍草率的通行证。他批评的并不是Scholze的工作——他实际上认为那项工作才华横溢、严谨扎实——而是建立在其基础上的研究成果。他在一些论文中发现了错误，在另一些论文中发现了逻辑漏洞，而专家们只是把他的话一带而过，向他保证，尽管具体论证不够严密，但大方向是正确的。But in the papers he reviewed, Buzzard thought that it had become a permission slip for sloppiness. His critique was not of Scholze's work, which he actually found brilliant and rigorous, but of the results built on top of it. He noticed mistakes in some papers and logical gaps in others, and experts just brushed him off, assuring him that the thrust was correct even if the particular arguments were loose.

Buzzard明白，在数学家理清各个部分如何相互契合的过程中，新兴领域可能还不够严谨。他看到一篇篇草率且不完整的论文层层叠加，担心自己的数学领域正在变成一座纸牌屋。Buzzard understood that young fields can be inexact while mathematicians work out how all of the pieces fit together, He saw one sloppy incomplete paper building atop another and worried that his area of mathematics was turning into a house of cards.

所以，对他来说，Lean 的吸引力就在于，他想把自己所在领域里发展出的这些论文形式化，也就是把它们转换成这种计算机编程语言，确切地判定它们是否正确；如果不正确，就把它们修正；如果正确，那就能让他重拾信心，继续在这一领域开展研究。下面是一个简单的例子。ring 策略利用 Mathlib 中的工具来构造这个代数恒等式的证明。So to him that was the draw of Lean, was he wanted to take these papers that had developed in his field, formalize them, like convert them into this computer programming language, determine with complete certainty whether they were correct and if they weren't fix them but if they were then it would just kind of give him renewed confidence to kind of proceed in research in this area. So here's a small example. The ring tactic constructs a proof of this algebraic identity using machinery from Mathlib.

然后 Lean 会检查这个证明，并显示“没有目标”，这意味着任务已经完成。Lean 启动时，它并不懂任何数学。它配备了一些基本的数学公理和规则，因此它对数学逻辑有某种、就像是某种理解。那你需要做的就是为它配备一个定义库。Lean then checks the proof, and it says no goals, which means the task is complete. When Lean, when you boot up Lean, Lean does not know any mathematics. It's equipped with basic axioms and rules for math, so it has some kind of just like some understanding of mathematical logic, What So you need to do is equip it with a library of definitions.

Mathlib：一场众人协力搭建谷仓的活动Mathlib as a barn raising

这也是我书中的一条平行故事线。书里有两条关键故事线，几乎可以说是两个梦想，它们彼此高度依存，有时又相互冲突。其中一条是 Leo 对 Lean 的愿景——这是他想要打造的软件。And this is the parallel story in my book. There are kind of two key stories, two dreams almost that are very dependent on each other, sometimes in tension with each other. So one is Leo's vision for Lean, the software he wants to build.

另一个方面是后来被称为 mathlib 的项目的发展。mathlib 是一个数字数学库，由书中的几位主要人物牵头。像 Kevin Buzzard、Johan Commelin、Patrick Massot 这样的人都参与其中，Jeremy Avigad 也非常投入；Mario Carneiro 则是 mathlib 发展过程中另一位非常重要的人物。这个项目的愿景是通过众包协作，用 Lean 语言从头开始定义数学中的基本概念。The other is the development of what comes to be called mathlib, a library of digital mathematics which is spearheaded by several of the main characters in the book. People like Kevin Buzzard, Johan Commelin, Patrick Massot, Jeremy Avigad is very involved, Mario Carneiro is another figure who's very important in the development of mathlib. The vision for that is it will be a crowdsourced effort to define in lean language basic concepts in math from the ground up.

所以，先从高中水平乃至大学水平的数学学起，这样你之后就具备了进一步编码更复杂数学形式所需的基础。So starting with even just like high school level math to college level math so that you have the ingredients to then later encode more sophisticated forms of math.

这大概就是 Lean 超越四色定理和开普勒猜想这类组合数学成果的方式：它成了一个可以用来表达非常深奥、处于前沿的抽象数学的地方。这要归功于 mathlib 的发展。其实，早在 2020 年，我就因为受命为《Quanta Magazine》撰写一篇关于 mathlib 发展的文章而对这个故事产生了兴趣，那时它还处于相当早期的阶段。在那篇文章里，我说——我当时说，mathlib 有一种大家齐心协力搭建谷仓的精神。That's kind of the that's how lean breaks beyond just these combinatorial results like the four color theorem and Kepler's conjecture and becomes a place where you can express very deep kind of frontier level abstract math. It's through the development of mathlib and actually I got in interested in this story back in 2020 when I was assigned an article for Quanta Magazine on the development of mathlib when it was still quite early days. In that article, I say I said that mathlib had the spirit of a barn raising.

这完全是一项社区协作，大家在没有任何中央权威、也没有中央资源的情况下，把这件大事做成了。于是，这个数字数学库逐渐建立起来——mathlib 是 Lean 的数学库。它诞生的时间，差不多正好是我开始进入这个领域的时候。It was just like this like community effort to get this massive thing done without any central authority, no central resources. And so slowly, this library of digital mathematics is created mathlib is Lean's mathematics library. so it was born about the same time that I started working in the field.

那是三万行代码，里面包含一大堆关于有限集的极其基础的定理，以及一些非常基础的本科数学定义，就这些而已。我刚开始时，它甚至连实数的定义都没有，或者说，它刚有了实数这个概念——这可是古希腊人和巴比伦人就已知的东西，你知道，已有几千年的历史了。它还没有复数的概念；我想，复数大约是五百年前才出现的。it was thirty thousand lines of code containing a bunch of completely basic theorems about finite sets, and some very basic undergraduate level mathematical definitions, and that was it. It didn't even have a definition of the real numbers when I started, or it just got this concept of the real numbers, which is something known to, yeah, known to the ancient Greeks and the Babylonians, you know, is, you know, thousands of years old. And it didn't have the complex numbers, which are, I guess, from about five hundred years ago.

所以显然还有很多工作要做，你知道，我花很多时间教学。对吧？这是我工作的一部分。So there was clearly a lot of work needed you know, I spend a lot of time teaching. Right? That's part of my job.

我教这些本科生。他们走进来。大学数学系的运作方式大概就是，你会说，好吧。I teach these undergraduates. They come in. And the way it works at university in a mathematics department is you kind of say, okay.

这些内容你在学校都学过，不过实际上，我们会从基础重新开始，然后快速地把所有内容过一遍。You learn all this stuff at school, but actually, we're start again from the basics and just work through everything quite quickly.

我们教他们的内容之一，就是如何定义复数。复数是一种基础数系，可以追溯到笛卡尔。我当时想，哦，这东西不懂复数。我们来教它复数吧。And, one of the things we teach them is how to define the complex numbers, which are these basic number system that goes back to Descartes. I kind of thought, oh, this thing doesn't have the complex numbers. Let's teach it the complex numbers.

就这样，我们定义了复数，证明了它的一些基本性质，效果很不错。我还提交了一个拉取请求。So there we go. We define the complex numbers, prove basic things about it, and it was great. And I made a pull request.

你知道，这是一个免费的开源数学库。所以我向这个数学库提交了一个拉取请求，之后它被合并进了主分支。突然之间，我们就有了版权归属为 Kevin Buzzard（2017 年）的复数。You know, this is a free open source maths library. So I made a pull request to this maths library, and then it got merged into the main branch. And suddenly, we've got complex numbers copyright 2017 Kevin Buzzard.

我只是在想，太好了。那接下来我们教他们什么？因为我现在在想，你知道，我们到底教本科生什么？I'm just thinking, great. Now what's the next thing that we teach them? Because I'm now I'm thinking, you know, what do we actually teach our undergraduates?

缺少什么？这个库里应该包含什么？我们为什么不直接为这个库做贡献呢？What's missing? And what should be in this library? Why don't we just contribute to this library?

不过，当然，事情实在太多，一个人根本忙不过来。所以我写信告诉本科生们，这件事绝对至关重要。我们刚刚才到了这样一个阶段：我所有的孩子都能自己去上学了。But, of course, there's so much stuff that one person can't do it. So I wrote the undergraduates it was absolutely critical. We'd just got to the point where all my kids could make their way to school by themselves.

他们可以自己往返学校，你可以把他们留在家里，而且他们不太可能，你知道，放火什么的，或者，你知道，那样是违法的。所以我可以晚点下班。比如每周有一个晚上，我会晚点下班，就让孩子们自己凑合着过。They could make their way to and from school, you could leave them in the house, and they were unlikely to, you know, set anything on fire or, you know, it'd be illegal. So I could stay late at work. Like, one evening a week, I'd stay late at work and just let the kids muddle on by themselves.

而且，我会教本科生如何使用这款软件，然后让他们开始，你知道，把他们本科阶段学到的东西转录下来，就是把这些内容教给这台机器。所以图书馆只是——我的意思是，当时世界各地还有很多其他人，不，不能说很多，但有不少人在做同样的事。你知道，那时候我把这东西当作一个本科生来对待。And, and I would teach undergraduates how to use this software, and then I would get them to start, you know, transcribing what they were learning in their in their undergraduate degree, just just teaching it to this machine. So the library just I mean, there was lots of other people around the world well, not lots, but there were plenty of other people around the world doing the same thing, you know, I was treating this thing as an undergraduate at the time.

所以当时是2017年，问题是，你知道，咱们就假设你已经注册了我们的学位课程。你知道，我们能不能真的按教本科生的进度来教你？这事勉强算是办得到。So it's 2017, and the question was, you know, let's just imagine you've enrolled on our degree. You know, can we can we actually teach you at the same rate as we teach the undergraduates? And it was it was just about possible.

你知道，那东西当时的学习速度和我们的学生一样。不过，三年后，我们可以稍微退后一步说，嗯，实际上，你基本上已经掌握了我们教本科生的大多数内容。是啊，那差不多就是我爱上它的时候，你知道，因为我一直想教它。但一个新的数学思想什么时候才适合成为数学知识库的一部分呢？数学是一个有趣的对象。You know, the the thing was learning at the same rate as our students at the time. But, you know, three years later, we could sort of step back and say, well, actually, you do basically know most of the things we teach our undergraduates And, yeah, that was sort of when I fell in love with it, you know, because I'd wanted to teach it. But when is a new mathematical idea ready to become part of the library? mathematics is an interesting object.

这是人类创造出的一个巨大抽象对象。而在边界处，有些东西还没有——你知道，还没有完全成形。It's this gigantic abstract object that humans have created. And at the boundary, there are things that haven't you know, they're not quite fully formed.

有些想法算是能用，或者在某些情况下能用。嗯，我们需要思考这些想法应该如何成熟，它们真正应该是什么样子。数学需要逐渐成熟，有时是在边界领域；它不是适合放进库里的材料。嗯。There are ideas which sort of sort of work or work in some cases, and, yeah, we need to think about how these ideas should mature what they should really look like. Mathematics needs to mature, sometimes at the boundary, it's it's not material that's ideal for the library. Yeah.

我们希望库中收录的是那些真正理解透彻、并且处于恰当一般性层次的想法。你知道，我们想要的是经过打磨的、经过打磨的数学。那些还有点混乱的东西，你知道，我们可以试着把它教给软件，但不一定非要把它加入库中。库希望收录的是已经成形、经过深思熟虑、你知道，而且很有概念之美、也清楚自己该处于什么位置的想法。基本上，现在库里的内容都是经过深思熟虑、优美的想法。库里的有些内容其实是过去几年才出现的，但其中很大一部分是更基础的东西，我们觉得自己已经理解得很好，因为你知道，只有到了这种时候，才适合把它提交进去。What we want in the library is ideas which are really well understood and that exist in the correct generality. You know, we want polished we want polished mathematics. stuff which is still a bit chaotic, you know, one can attempt to teach it to the you know, we can teach it to the software, but we don't necessarily want to add it to the library. The library wants to take sort of fully formed, well thought out, you know, beautiful conceptual ideas, which sort of know their place. essentially, all of the library now is is well thought out, beautiful ideas some of the things in the library are actually stuff that happened in the last few years, but a lot of it is much more basic stuff that we feel like we understand well because that's, you know, that's when you want to commit.

对吧？这是我们社区工作的一部分：试图理解人类已经做了什么，并把它整理成正确的、你知道的、最抽象、最有用的形式，以供未来工作使用。因为你肯定不想把某个概念放进库里，后来它被泛化、简化了一番，结果不知怎么的，你又得把整个东西重新做一遍。我们努力避免这种情况。Right? this is part of the work of our community, trying to understand what humans have done and to get it into the correct, you know, most abstract, most useful form for future work. Because you don't really want to put some concept in the library, and then it gets generalized and simplified a bit, and then somehow you need to rework the entire thing. This we try and avoid this.

我们喜欢一次就把事情做好。We like to get things right first time.

完美空间的噱头The perfectoid-spaces stunt

有时，我们不得不去修改一个基本定义，这可能会带来大量工作，因为你知道，之后成千上万个文件都会出问题，需要修复。Kevin Buzzard 有种表演家的直觉。他简直天生就是个营销高手，会想出几个本质上算是计策或噱头的办法来做这件事。Occasionally, we have had to go through and change a fundamental definition, can be a huge amount of work because then, you know, many thousands of files then break and need to be fixed. Kevin Buzzard has like the instincts of a showman. He's like a natural marketer and he comes up with a couple essentially schemes or stunts for doing this.

其中一项实际上就是在 Lean 中形式化一种名为概形的数学对象，它属于代数几何领域。这一概念由亚历山大·格罗滕迪克于二十世纪中叶提出。他心想：如果我们能在 Lean 中形式化概形，并把这件事告诉全世界，那么数学家就会突然开始相信，这对他们自己所关心的那类前沿数学是有用的。And one of them actually is to formalize a mathematical object called schemes which is an algebraic geometry. It comes from Alexander Grothendieck in the mid twentieth century. He says to himself, if we can formalize schemes in lean and I can tell the world about it then mathematicians will suddenly start to believe that this is useful for the types of type of like frontier math that they themselves care about.

他这么做，结果大家集体打了个哈欠，因为人们告诉他，Kevin 的方案都是老掉牙的数学。对吧？都六七十、八十年前的东西了。He does it and he's met with like a collective yawn because people tell him, Kevin schemes are old math. Right? Sixty, eighty years old.

我读研究生时就知道这一点。这不是什么前沿数学。凯文就说，好吧。I knew this when I was in graduate school. This is not frontier math. And Kevin's like, okay.

没错。什么是前沿数学？在这一时期，也就是大约2018年，前沿数学指的是一种叫作完美拟完备空间（perfectoid spaces）的对象。它由德国数学家彼得·舒尔策提出；当时和现在，他都被认为可能是当今最伟大的在世数学家。That's true. What is frontier math? And in this period, around 2018, frontier math is this object called perfectoid spaces which is something that was created by a German mathematician named Peter Scholze who is today and then as well considered maybe the greatest living mathematician.

完美拟空间是数学中真正处于前沿的对象。Kevin 说：“好吧，如果我们能把它们形式化，如果我们能证明 Lean 有能力表达完美拟空间，那就能确凿无疑地证明它无所不能。”于是，他和 Massot、Commelin 开始了这项工作，只有他们三个人，基本上是要制定一份蓝图，或者说一份指南，列出他们需要定义并在 Lean 中实现的东西，这样才能写出完美拟空间的定义。这本质上就像建筑项目中的一份待办清单。Perfectoid spaces are truly state of the art objects in math and Kevin says, alright, if we can formalize them, if we can show lean is capable of expressing perfectoid spaces, we'll have indisputable proof that it can do anything. And so he and Massot and Commelin start this effort, just the three of them to create a blueprint essentially, a kind of a guide to the things they would need to define and lean in order to be able to write the definition of a perfectoid space. It's essentially a punch list like a construction project.

你知道，我们需要你找到这个、这个、这个和这个，最终得到 perfectoid 空间。他们成功做到了，而我认为需要强调的一点是：mathlib 汇集了所有使用 Lean 工作的人都可以借助的数学知识。目前，它的水平大致相当于研究生一年级的数学。You know, we would need you to find this and this and this and this and ultimately we get perfectoid spaces. They succeed at that and what that I think an important point to emphasize is mathlib is all of the math that anyone working in lean can draw on. At the moment it's essentially maybe first year graduate level math.

他们掌握了几乎所有本科数学知识，只差一些零零散散的内容；也掌握了所有一年级研究生水平的数学。然后，他们的知识中还会出现一些极端的跃升，从研究生数学一路跃升到该领域最前沿——而那与研究生数学相距甚远。They have all of undergraduate math modulo a few things here and there. They've got all of first year graduate level math. Then there are these extreme spikes from grad math to the far frontier of the field which is like extremely far from graduate school math.

完美拟空间是我们拥有这一基础的最早几个例子之一。现在，我们要以此为基础，建起一座直通前沿的狭长摩天楼。完美拟空间就是这类做法的第一个例子。这个绝招确实如 Buzzard 所希望的那样奏效。Perfectoid spaces is one of the first examples of we have this foundation, now we're gonna build this like narrow skyscraper to the frontier. Perfectoid spaces is the first example of that. That stunt works the way Buzzard hopes it will work.

这吸引了很多人的注意，提升了 Lean 的知名度，也算是开始说服人们。它开启了书中所描述的那个过程，让人们相信 Lean 可以用于真正的数学。那时我才刚开始做这件事——很久以前了，嗯，早在 2017 年，我正经历一场中年危机，试图弄清楚计算机证明定理这个领域到底是怎么回事。It captures a lot of people's attention, it boosts Lean's profile and it kind of starts to convince people. It starts the process described in the book of convincing people Lean can be used for real math. So I was just beginning this was back back so back in 2017, I was having this midlife crisis and trying to work out what was going on in the area of, you know, computers proving theorems.

令我觉得好笑的是，我发现剑桥附近有一场大型会议，两年后才举行，可我已经错过了报名时间。不过，这场会议是在剑桥的牛顿研究所举办的，他们走在了前面。这是在新冠疫情之前。And I discovered, to my amusement, that there was a big conference in the area that I was far too late to register for in Cambridge taking place in two years' time. But came this was at the Newton Institute in Cambridge, and they were ahead of the game. This is pre COVID.

但他们已经在互联网上录制并直播演讲了。因此，尽管我无法去参加会议，仍然可以观看这些演讲。But they were already recording and live streaming their talks on the Internet. So, even though I couldn't go to the conference, I could still watch the talks.

第一场报告是汤姆做的，我原以为报告人会是汤姆——汤姆·黑尔斯。我以为他会谈论他对开普勒猜想的证明。但事实上，这只占他报告内容很小的一部分。And the first talk was given by Tom, and I imagined, that he would be, by by Tom Hales. And I imagined that he would be talking about his proof of the Kepler conjecture. But in fact, that only formed a very small part of his talk.

他谈到的，正是我一直担心的事情。他谈的是将现代数学形式化，也许是将所有现代数学都形式化。他提出的一个想法是，也许是时候让数学家们学习一些计算机定理证明语言，但不必学到足以把所有证明都输入进去的程度，而只需逐字输入他们定理的陈述。He was talking about, you know, exactly the thing that I've become worried about. He was talking about formalizing modern mathematics, you know, perhaps all of modern mathematics. And one of the things he suggested was that perhaps it was time, that we got mathematicians not to learn enough about these computer theorem proving languages to actually type in all their proofs, but just to literally type in the statements of their theorems.

因为那是容易得多的一项工作，只是这么说而已。我声称自己证明了这一点，这是它用英语表述时的样子。但定理的陈述用形式语言写出来是这样的，而证明则长达一百页。Because that's a much easier job, just saying, okay. I claim that I proved this, and here's what it looks like in English. But here's what the statement of the theorem looks like in a formal language, and then the proof is a hundred pages long.

而要把这个证明翻译成这种语言，你知道，那得花上写一篇博士论文那么多的工夫，是个极其庞大的难题。不过，也许我们应该开始劝数学家用这种形式语言陈述他们在做什么，因为这样就不会有歧义。你看，实际上，人们可能会以为数学是一种完美的语言，一切都能用它以完全没有歧义的方式表达出来。And translating the proof into this language would be, you know, would be like a PhD thesis worth of work, you know, a gigantic problem. But perhaps we should start persuading mathematicians to state what they're doing in this formal language because then there's no ambiguity. You see, in reality, you would imagine that maths was this sort of perfect language where everything can be expressed, you know, in a in a completely unambiguous way.

但实际上，事情并非如此，并非如此。实际上，你读了，你读了论文的第 3 节。第 3 节中说，从这一点开始，p 将是一个至少为五的素数。But in practice, this is not this is not what happens. In practice, you read you read section 3 of the paper. In section 3, it says, from this point, p will be a prime number which is at least five.

然后你读到论文第 7 节的内容，里面只是在谈论一个叫作 p 的数。你知道，读过很多数论论文后，你会知道 p 是一个素数。And then you read something in section 7 of the paper, and it's just talking about a number called p. And you know from reading lots of number theory papers that p will be a prime number.

但是，p 至少为五这一事实，是在第3节里顺带提到的。如果你从第7节开始读，就不会注意到这个假设。于是看起来定理好像在说些什么。But this this fact that p is at least five, that was sort of slipped in to section 3. If you start reading in section 7, you don't notice this hypothesis. And so it looks like the theorem says something.

你知道，如果你通读整篇论文，定理的表述就是正确的。但如果你只是想弄清楚第7节到底在讲什么，就可能会出错。Hales当时就说，我们得把这些错误改正过来。You know, the theorem isn't the theorem if you read the whole paper, then the theorem is correctly stated. But if you're just trying to work out, you know, what's going on in section 7, then you might make an error. And Hales was like, we need to fix these errors.

我们现在有工具可以做到这一点了。我当时就想，这真是个好主意。你正试图、试图翻译所有内容……我……我才进行到两周，就意识到这些系统一无所知。We've got tools that can do this now. And I just thought, this is a great idea. You're trying to trying to translate all the I'd I'd I was two weeks in, and I'd realized that the systems knew nothing.

但不知为何，教系统基本的数学定义似乎比教它那些长达一百页的定理证明可行得多，因为许多数学定义都相当简短。But somehow, the idea of teaching the system's basic mathematical definitions seemed to be much more viable than teaching it, you know, a hundred page long proofs of theorems because many mathematical definitions are quite short.

事实上，这就是这个库在2017年的样子。里面包含了一些数学定义，本科生觉得相当难懂。你知道，就是二、三年级会学到的那些高深内容，比如拓扑空间，还有理论、环之类的东西。In fact, that was what the library looked like in 2017. It contained some some definitions that mathematic that, you know, undergraduates find quite difficult. You know, second year and third year, fancy things like topological spaces and, you know, theory and rings and things like this.

但实际上，只把定义写下来，在计算机里不过是几行代码。真正费工夫的是证明所有相关定理。所以，只要你能把定义写下来，我们就可以开始陈述定理了。But actually, just writing the definition down is only a few lines of code in the computer. It's proving all the theorems about it where all the work is. So if you can just write down the definitions, then we can start stating the theorems.

而且，在我看来，这似乎是一种可行的推进方式，同时也能接触一些有趣的材料。所以这完全是我自己的想法：看看这些现代论文，然后指出这完全不可能。相比之下，Hales 的想法是可行的。And, this just seemed to me like a viable way to move forwards whilst engaging, you know, with interesting material. So it was just a completely my idea was just like, let's check these modern papers, remark that's completely impossible. Whereas Hales' idea was viable.

事实上，当时不知怎么回事还不太可行。你知道，Hales当时力主——Hales力主在2017年开展这件事，而2017年做起来不知怎么就太难了。但实际上，七年后，我写了一份资助申请，正是要做Hales所说的那件事，你知道，就是做同样的事情。In fact, it was somehow not quite viable at that moment. You know, Hales pushed for Hales pushed for it to be happening in 2017, and it was somehow too difficult to do in 2017. But, actually, seven years later, I wrote a grant proposal to do exactly what Hales had said, you know, just to do the same thing.

而且，我们现在已经花了一年时间做这件事，现在它似乎开始变得可行了。我们选取本十年发表于顶尖纯数学期刊的定理，尝试只把定理陈述翻译成软件语言。而且，我们现在才完成了百分之二十。And, and we've spent a year working on this now, and it now is sort of it's becoming viable. We're taking, theorems published in, you know, the top pure maths journal, this decade, We're trying to translate just the statements of the theorems, into the language of the software. And, again, we're twenty percent through.

所以，这至少在一定程度上表明，你知道，这个梦想正慢慢成为现实。我想，一年后，我们的进展会远远超过百分之二十。And so that's some indication, that at least, you know, this dream is slowly becoming a reality. And I would imagine that in a year's time, we're gonna be far more than twenty percent through.

所以，呃，Hales 提出的这些想法，花了很多年才得以实现；但现在，你知道，它们正在逐渐成为现实。是的，我会说，Hales 当时的演讲确实很有远见，而如今他的愿景正在实现。把证明形式化，或者用这种形式语言写数学，对吧，确实相当繁琐。你必须把每一个细节都交代清楚。So some so Hales had these ideas which have taken years to become real, but now, you know, now they are becoming so, yeah, I would say that Hales was really of you know, this was a visionary talk, and now his vision is coming to fruition. Formalizing a proof or writing math in this formal language, right, is very kind of tedious. You have to spell out every little detail.

即使是那些对数学家来说多少有些琐碎或显而易见的事情，你也得设法让计算机相信它们是正确的。书中有几处提到，数学家读到一份 PDF 上用非正式方式写成的证明，想要把它形式化并整合进去，对吧？他们想用 Lean 将其形式化，而他们发现，往往恰恰是那些对人类来说最琐碎、最显而易见为真的陈述，最难让 Lean 相信它们是正确的。Even things that are kind of trivial or obvious to mathematicians, you need to kind of convince the computer of their correctness. There are a few moments in the book where a mathematician is reading a proof that's written informally on a PDF and they want to formalize it, incorporate it, right, they want to formalize it in lean and what they discover is often it's the most trivial statements that are most obviously true to humans are the hardest to convince lean are correct.

诸如此类的事情，比如一加一等于二。Kevin Buzzard 在刚开始使用 Lean 的头几周里，就遇到了形式化简单陈述的困难：他只是想让程序相信一加一等于二。这是件很难做到的事。Things like one plus one is two. Like Kevin Buzzard confronts the difficulty of formalizing simple statements in just the first few weeks he's using lean where he wants to just convince the program that one plus one is two. That is a hard thing to do.

比如说，你会怎么说服我一加一等于二？我们都知道这是对的，可一旦你真的开始思考该怎么让一个不……不……的人信服，就会发现这很难。后来，陶哲轩在 Lean 中形式化自己的一些工作时，也遇到了一个类似的初等事实：它对数学家来说显然正确，但要让 Lean 相信它是正确的却很困难。Like how would you convince me one plus one is two? It's like, know, it's we all know it's correct but once you actually start to think about how you would, you know, impress someone who's not not it's hard. Terry Tao much later when he is formalizing some of his own work in Lean, he confronts a similarly elementary fact that is just obvious on its surface to mathematicians but convincing Lean it's correct is difficult.

所以关键在于，用这种形式化语言书写数学时，有很多很多步骤，会变得有些繁琐和困难。So the point is there's a there are lots of lots of steps when writing math in this formal language that become kind of tedious and difficult.

莱昂纳多·德·莫拉对 Lean 的一个设想是加入一些名为 tactics 的小型辅助程序，用来自动完成某些重复步骤。在证明中经常会遇到这类步骤。比如，你不必每次都向 Lean 解释为什么一加一等于二，而是可以调用某个 tactic，让它处理这类算术问题，证明数值等式，这样你就不必亲自完成这些步骤了。于是，Leo 扩展了 Lean 的这项能力：他编写了一些对 Lean 很有用的特定 tactics，同时也为社区成员——Lean 用户——提供了编写自定义 tactics 的能力。One of Leonardo de Moura's ideas for Lean is it would have these little helper programs called tactics which will automate some of those repeated steps. Those kind of things, steps that happen regularly in proofs instead of having to explain to lean why one plus one is two, you can invoke a certain tactic that just does those type of arithmetic guarantees that kind of proves the qualities, numerical qualities and then you don't have to do it yourself. So Leo builds out the capability, he writes some specific tactics that are useful for lean but he also builds out the capability for people in the community, lean users to write their own tactics.

这就成为 Lean 变得更加强大的一种方式，也让在 Lean 中编写证明的痛苦开始减轻。That becomes one way in which Lean becomes much more powerful and this pain of writing proofs in Lean starts to diminish.

施尔策那份无人读过的证明：液态张量Scholze's proof nobody had read: Liquid Tensor

朔尔策是其他数学家需要有人检查证明时会求助的数学家。因此，2020年11月，菲尔兹奖得主彼得·朔尔策联系了我。那时，这个库在某种意义上刚刚算是“毕业”。Scholze was the mathematician others turn to when they needed their proofs checked. So in November 2020, I was contacted by, the Fields Medalist, Peter Scholze. This was back when the library had just basically graduated in some sense.

你知道，我们当时有那么一个东西，它懂很多本科水平的数学，但其他方面懂得不多。Scholze问我有没有读过——有没有仔细读过他最新的预印本。我的回答当然是：绝对读过。You know, we had sort of it it knew a lot of undergraduate level mathematics, but not too much else. And Scholze asked me if I'd read I'd carefully read his latest preprint. And the answer to this was, well, absolutely.

你知道，我们大学当时有个关于这篇论文的学习小组，是个覆盖整个伦敦的学习小组。伦敦其他大学也有人参加。我们每周都会见面，花两个小时读这篇论文的另一部分。You know, we'd had a study group on it at my university, a London wide study group. There were people from other universities in London. We would meet every week, and we would read another section from this you know, spend two hours reading another section from this paper.

而在学期期间，我们会读完整篇，我们会读完整篇论文。And during the term, we'd read the entire we'd read the entire paper.

那是在彼得联系我之前的那个学期。于是我说，是的。他说，你知道，我们之前看过这件事。That was the term before Peter got in touch with me. And, so I said, yes. He said, you know, we'd looked at it.

非常有意思。你知道，恭喜你。然后他说：“你有没有仔细读过这篇论文中某个定理的证明？我想是定理 8.4。”Very interesting. You know, congratulations. And, he said, did you carefully read the proof of I think it was the theorem 8.4 and, one of the theorems in this paper.

所以，这是他发来的第二封邮件，你知道，他专门询问这篇论文中某个论证的细节。我于是回去看了看这篇论文。它篇幅很长，而我们之前并没有读过这部分的细节，只读了定理的陈述。So this was a second email from him, you know, asking specifically about checking the details of one of one of the arguments in this paper. So I went back and looked at the paper, which is a big paper, and, and, we had not read the details of this. We'd read the statement of the theorem.

我们明白它想表达什么，也明白它的意义何在、在整个大局中处于什么位置。至于证明，不过是六页技术计算，我们顶多也就草草浏览了一遍。你懂吧？Understood We what it was trying to say until, you know, the point of it, where it fitted into the grand scheme of things. And the proof was just sort of six pages of technical calculations that we had skimmed through at best. You know?

哦，这样你就能大致了解事情是怎么回事了。所以我们根本没看那些细节。于是我给他回了封邮件，说：“你知道，我们看过了。”Oh, it's you get the hang of the general idea of what's going on. So we had not read the details at all. So I emailed him back, said, you know, we looked at it.

我们没看细节。他说，大家都这么说。他还问过普林斯顿和哈佛的人。We didn't read the details. And he said, that's what everybody says. And he'd asked people at, you know, at Princeton and at Harvard.

大家都这么说。比如，还有就是，他已经深信没人真正读过他的作品。你知道，人们只是草草浏览了他的作品。That's what everybody says. Like, that and, he'd become convinced that nobody had actually read his work. You know, people had skinned over his work.

但是，当然，数学的关键在于细节。他说，说到底，这些材料看起来有些技术性，但其中很多内容其实是本科 स्तर的材料。所以，也许你的系统可以检查这些材料。But and, of course, the devil is in the details in mathematics. So he said, at the end of the day, this material is it sort of looks technical, but at the end of the day, a lot of it is undergraduate level material. So maybe it would be possible for your system to check this material.

而且我觉得这会是一个很好的测试，因为这很有意思。And I thought that would be a great test because this is interesting.

我们手头的东西都只是本科水平的。突然间，有位菲尔兹奖得主建议我们可以检查他最新论文的一部分。当时我只是，你知道，参与其中的一员，没人把这款软件当回事。All we have is undergraduate level stuff. And all of a sudden, I've got this Fields medalist suggesting that we could check part of his most recent paper. And I was just, you know, part of at at the time, nobody was taking this software seriously.

也许人们才刚开始认真对待它。前一年，我们当时……我们采用了他的一个定义。正如我所说，定义比那些长达一百页的定理证明容易得多。Maybe people were just beginning to take it seriously. The year before, we'd we'd taken one of his definitions. As I said, definitions are much easier than proofs of a hundred page theorems.

前一年，我们把他给出的一个定义教给了机器，也取得了一些进展。你知道，人们开始注意到，这款软件能够处理更复杂的内容。但这确实是一个复杂定理的复杂证明。The year before, we'd taken one of his definitions and taught it to the machine, and we got a certain amount of traction. You know, and people are beginning to notice, the software was able to do more complex material. But this is, yeah, this was a complex proof of a complex theorem.

它只有——它只有六页长，但当时的社区规模很小。It was only it was only six pages long, but the community at that time was small.

我们确实想过，我们确实想过，能不能真的把这六页内容看完。于是我问了几个人，他们就说：“嗯，我们能不能把这封邮件公开？”所以我问彼得愿不愿意为我的博客写一篇博文。we did wonder we did wonder whether it would be feasible, to, to actually plow through these six pages. And I asked various people, and they were just like, well, could we make this email public? So I asked Peter if he would write a blog post for my blog.

我当时开了个博客，算是在推广这个软件。于是彼得在我的博客上发了一篇文章，把这件事作为一项挑战提了出来。随后，社区里开始有人站出来说：“其实，我愿意投入大量时间来做这件事。”当时，我们以为这大概要花一年的时间。但后来我们开始阅读了。I'd started a blog that was sort of promoting the software so Peter wrote a blog post on my blog putting this as a challenge, and then people started popping up in the community saying, actually, I'll be prepared to spend a substantial amount of time doing this. And at the time, we imagined it would be about a year's worth of work. But then we started reading.

我们不得不开始阅读这些材料，真正开始仔细阅读。我们可能是最早读这些材料的人，也可能是第一批没有草草浏览的人。于是，我们开始逐字逐句地仔细检查，发现了一种简化方法。We had to start reading the material, and we had to start reading it. We were really the first people to be reading it possibly, the first people not to skim through it. And, we started going through it with a fine tooth comb, and we found a simplification.

尤其是 Johan Commelin 找到了一种简化方法。然后，六个月后，这就把所需时间缩短了一半。又过了六个月，我们核查了关键的一点，也就是 Peter 担心的那个东西可能有问题。Johan Commelin in particular found a simplification. And, six months so that cut the that cut the time down by a factor of two. And six months later, we'd we'd checked the key thing that Peter was you know, Peter was worried that the thing was wrong.

彼得就说：“不。”我觉得这是对的。我的合著者达斯汀·克劳森也觉得这是对的。And Peter's like, no. I think it's right. My co author thinks it's right, Dustin Clausen.

没有其他人读过它。也许它是错的。所以六个月后，我们会通过他来读它。No one else has read it. Maybe it's wrong. So six months later, we'd read it through him.

他就说，没关系。没错。机器说没错。He like, it's okay. It's right. The machine says it's right.

彼得变得特别兴奋，这就像，嗯，好吧。所以这些系统确实有用，因为它们让我了解了证明是如何成立的。你知道，我们已经找到了一种更具概念性的论证方式，至少针对其中一部分，而且现在终于真的有人读过它了。And Peter got very excited, which is like, okay. So these systems are actually useful because they taught me something about how the proof works. You know, we've we've found a more conceptual argument a part of it, and something has now actually finally read it.

于是我们兴奋起来，又写了第二篇博客文章，结果这篇文章随后、随后就在社区里走红了。So we got excited and wrote a second blog post, which then which then went viral in the community.

然后转眼间，你知道，Quanta就上了那个，你知道，你知道，而我也内急了。所以在那一刻，我意识到我们已经有所成就了，因为你知道，现在那些算是大人物的人开始关注我们了。然后事情就这么，你知道，继续发展下去了。And the next thing we know, you know, Quanta was on the you know, you know, and nature was calling me up. And I so at this point, I realized that we had arrived now that, you know, now the sort of the big league people were taking an interest. And then it sort of, you know, it went on from there.

当然，一旦我们有了一些知名度，就会有越来越多的人加入这个社区，专业数学家也会说：“嗯，我们能不能在我这个领域做点事情？”对。然后会有一位专家过来，首先就问：“我们能不能做我的最新定理？”Then, of course, once, you know, once we have some visibility, more and more people start coming into the community, professional mathematicians, saying, well, can we actually do some stuff in my area here? Yeah. An expert would come along, and their first question would be like, can we do my latest theorem?

答案是否定的，不过我们可以做一些基础工作，比如你所在领域的基础内容，所以可以从这里开始。于是，图书馆开始以快得多的速度发展起来。当然，那段时间发生的另一件事就是新冠疫情。And the answer was no, but we can do, you know, the basics in your area, and so here's where to start. And so the library started growing much more quickly then. The other thing, of course, that happened around that time was COVID.

所以人们当时算是被困在家里，玩电脑游戏也就成了一种挺有吸引力的消遣。你知道，一边玩电脑游戏，一边接触有趣的数学。对一些数学家来说，这是一种非常吸引人的消磨时间的方式。So people were sort of stuck at home, and, playing computer games was sort of an appealing way. You know, playing computer games while simultaneously engaging with interesting mathematics. It was some mathematicians found that a very appealing way to spend their time.

因此，库的增长速度出现了一次相当大的跃升。当你在 Lean 中有一个完整展开的数学证明时，你可以点击其中的元素进行探索，看看论证的不同部分实际上是如何相互关联的。So there was a sort of a big sort of jump in the rate of growth of the library, When you have a mathematical proof in lean fully spelled out you can kind of click into elements of it, investigate and see how different parts of an argument really relate to each other.

AI 能学会寻找证明吗？AlphaProofCan AI learn to find proofs? AlphaProof

这种与证明进行交互的能力，是 Lean 提供而静态 PDF 不具备的。那么，同样的机制能不能教会 AI 找到证明呢？最近，我在《代码中的证明》的新书发布派对上，和几位数学家聊了聊。到了晚上比较晚的时候，我们开始讨论，能不能把 AlphaZero 的方法，也就是零知识方法，应用到让一个 LLM 在只给它一些基本公理的情况下重新创造数学上。我们当时讨论的问题是：LLM 会不会重新发现人类基本上已经发展出来的数学？或者它能走到哪一步？This ability to interact with the proof is something that lean provides that a static PDF does not. And could that same machinery teach an AI to find proofs? so I was recently talking with some mathematicians at a book launch party for Proof in the Code. And kind of late into the evening we start talking about whether you could apply the AlphaZero approach, the zero knowledge approach to like having an LLM recreate mathematics if you just give it kind of the basic axioms. question we were talking about was would an LLM rediscover essentially kind of human mathematics or how far along would it get?

我交谈的这三位数学家之间大致达成的共识是，它未必会发现有理数之外的东西。如果把人类对数学的理解看作从有理数开始逐步推进，那么他们几乎从一开始就预期，计算机数学会偏离后来成为人类所发现的数学。And there was the kind of the consensus among these three mathematicians I was talking with was that it would not necessarily discover more than the rational numbers. If you were kind of advancing along the kind of the human understanding of math starting at the rational, so almost at the very very beginning they expected computer math would diverge from kind of what has become human discovered math.

我觉得原因在于，我们对恰当的抽象有一种直觉。那些令人满意的概念和定义，对我们来说感觉是对的、完整的，而且很有拓展性；当你开始把它们应用到不同情境中时，你会发现它们能发挥各种作用。我觉得你说得对：计算机要是以某种严格、具体的标准来搜索正确的东西，它的搜索就不会受到同样价值观的指引。我觉得它也就不会偶然发现那些最终对我们变得意义重大的数学概念。比如说，如果你在做一个证明，中间会有很多阶段，你会回头审视整个证明，然后心想：“哦，这不对，但当时感觉是对的。”And I think the reason is like we have this feel for the right abstractions. These kind of like satisfying concepts and definitions that feel right to us, that feel complete, that feel expansive in what they can in the kind of the work they can do when you know when you start applying them in different scenarios. And I think you're right to say that a computer doing this kind of search for things that are just like correct in some strict sense, some concrete sense would not be its search would not be informed by that those same kind of values and I think it would not stumble on the same things that the same mathematical concepts that have ultimately become meaningful to us. if you're working on a on a proof say, there are a lot of intermediate phases where you go and look at the whole thing and you're just like, oh, this is wrong, but it felt right.

我觉得那不只是数学推理过程中的某种奇怪副产物。那种「感觉是对的」的感觉，我认为大概是认知本身固有的。所以在你的书里，你讲了 AlphaProof 的故事。Like, I don't think that's just like a weird artifact of, the reasoning about mathematics process. The idea that it felt right, I think that's probably native to cognition. So in your book, you told the story of AlphaProof.

这还是在 2024 年的时候，他们确实把 Lean 用作架构的一部分。从背景来看，这也很有意思，因为较新的版本并不使用 Lean——至少目前可能还没有。不过，给我们讲讲 AlphaProof 的故事吧。So this was back in 2024, and they actually used lean as part of that architecture. It's very interesting in context as well because the newer versions don't don't use lean, possibly not yet. But tell tell us the story of AlphaProof.

很早以前，人们就对用人工智能做数学感兴趣。人工智能能解数学题吗？这在某种程度上显然是一种测试，因为数学嘛，你知道，是人类思想的巅峰。Very early on, there's this interest in using AI to do mathematics. Can AI solve math problems? It's a it's both kind of just like an obvious like tests because math is, you know, the pinnacle of human thought.

如果 AI 能做到这一点，也许它几乎无所不能。此外，数学对 AI 来说是一个非常有效的训练环境，因为最终你能得到清晰的奖励信号。If AI can do that, perhaps it can do almost anything. Also, math is a very effective training environment for AI because you get a clear reward signal at the end.

它是否正确解出了这道题？这就能实现强化学习：让 AI 系统解决问题，获得反馈信号，判断它是否答对；快速重复这个过程，不断迭代，从而大幅提升能力。接下来，你需要在数学领域确定一些目标，让 AI 挑战这些目标；早期确立的目标之一就是国际数学奥林匹克竞赛。Has it done the problem correctly or not? That enables reinforcement learning where you can have an AI system solve a problem, receive signal, did it do it correctly or not, do that very quickly, iterate a lot, get a lot better. You need then to identify certain targets in math to set your AI against and early on one of the targets that's established is the International Mathematical Olympiad.

这是世界上顶尖的中学数学竞赛。参赛者都是高中年龄段的学生，解题只需要用到高中数学知识。竞赛题目考查的就是这些内容，只不过题目设计得极其精妙复杂。It's the premier pre college math competition in the world. These are high school age students doing things that only require high school math. Those are the problems on the competition but extraordinarily sophisticated versions of those questions.

因此，早在初期，他们就提出了这个问题：AI 能否在国际数学奥林匹克竞赛中取得金牌级别的成绩？Google DeepMind 亲自开启了这项探索。So early on it set out, can AI achieve a gold medal level score on the International Mathematical Olympiad? Google DeepMind picks up this quest themselves.

书中我谈到了 2024 年国际数学奥林匹克竞赛（IMO）。在这次竞赛相关的工作中，DeepMind 设计了一个名为 AlphaProof 的系统，它几乎沿用了十年前 AlphaGo 的同一套架构。他们让它开始做 IMO 的题目训练：先从初中基础题开始，逐步训练它解答竞赛数学水平的题目；再通过强化学习慢慢提升奖励，直到它的能力达到 IMO 题目的水平范围。然后，他们基本上让 AlphaProof 参加了 2024 年的考试。为了避免机器抢了人类参赛者的风头，他们等人类选手完成答题后才把题目交给 AlphaProof。In the book, I talk about the 2024 IMO which is where DeepMind designs a system called AlphaProof which is based on the same architecture as AlphaGo from a decade earlier almost. They set it to work on the IMO, they train it to answer competition math level problems starting with basic middle school level things, they do reinforcement learning to like slowly reward climb until it is within range of IMO level problems and then they essentially administer the 2024 exam to AlphaProof. They receive the questions after the competitors have finished their work to there's a kind of concern about the machine upstaging the human participants so it receives the questions after the human competitors complete their work.

它比人类竞争者拥有更多时间，也拥有海量算力。It has more time than the human competitors. It has massive amounts of compute.

最终，它取得了银牌水平的成绩，解决问题的方式是输出 Lean 证明，然后用 Lean 验证这些证明。DeepMind 在强化学习阶段以及 IMO 竞赛阶段的实际解题过程中都使用了 Lean。AlphaProof 无法读取它本应解决的题目。Ultimately, it gets a silver medal level score and the way in which it solves the problems is by outputting lean proofs and then using lean to verify them. DeepMind used lean in both the reinforcement learning stages and then the actual problem solving in the competition stages of for the IMO. AlphaProof could not read the problems it was meant to solve.

它接收用 Lean 表述的命题，并用 Lean 构造证明，但竞赛题是以自然语言呈现的。DeepMind 需要的训练题可能多达数百万道。逐道手动形式化会造成一个无法克服的瓶颈。It took statements expressed in lean and devised proofs in lean, but competition problems arrive in natural language. DeepMind needed potentially millions of training problems. Formalizing each one by hand would create an impossible bottleneck.

因此，团队必须找到一种方法，将竞赛数学自动翻译成 Lean。翻译本身有其结构。代数和数论相对容易，因为它们的自然语言表述中本来就包含方程和符号。So the team had to find a way to translate competition mathematics into lean automatically. The translation itself had structure. Algebra and number theory were easier because their natural language statements already contained equations and notation.

DeepMind 最终几乎完美地自动形式化了这些领域中约百分之八十的问题。组合数学更难，因为其中的问题读起来像故事，充满自然语言，而符号却相对较少。数学内容可能是离散且可计算的，但人类的表述方式使形式化变得困难。DeepMind eventually auto formalized about eighty percent of questions in those areas nearly perfectly. Combinatorics was harder, its questions read like stories, full of natural language and relatively little notation. The mathematics could be discrete and computational, yet the human presentation made the formalization difficult.

尽管存在这一限制，DeepMind 还是生成了数千万个用 Lean 表述的问题。只有在此之后，AlphaProof 才能开始搜索证明。Despite that limitation, DeepMind produced on the order of tens of millions of problems stated in Lean. Only then could AlphaProof's proof search begin.

2026年的人工智能数学与陶哲轩的实验AI mathematics in 2026 and Tao's experiment

截至2026年9月，AI系统已开始攻克尚未解决的研究问题。在Epoch AI的固定预算测试中，一款尚未发布的OpenAI模型证明了埃尔德什问题126，并通过找到反例推翻了问题74。两项结果都在Lean中得到了验证。By September 2026, AI systems were tackling open research problems. In epoch AI's fixed budget test, a pre release OpenAI model proved Erdos problem 126 and disproved problem 74 by finding a counterexample. Both results were checked in Lean.

它解决了六十八个问题中的两个，而另外四个模型一个也没解决；9月8日，OpenAI 还发布了一份声称解决了纳维–斯托克斯千禧年难题的成果，并附上了 Lean 形式化证明，但遗憾的是，发布时机并不理想。It resolved two of sixty-eight problems the other four models resolved none and, on September 8, OpenAI also published a claimed resolution of the Navier Stokes Millennium Problem alongside a lean formalization, but unfortunately not under the best circumstances.

等式理论项目（Terence Tao）The Equational Theories Project (Terence Tao)

但这超出了本视频的讨论范围。早在 2024 年 9 月，Terence Tao 就启动了「等式理论」项目，这是一个开放协作项目，旨在梳理哪些代数定律能够推出其他定律，并由 Lean 验证结果。不到一个月，等式理论小组就将两千两百万个问题缩减到了两百三十八个。But that's outside the scope of this particular video. Back in September 2024, Terence Tao launched Equational Theories, an open collaboration mapping which algebraic laws imply others, with Lean checking the results. Within a month, the Equational Theories group had narrowed twenty-two million questions down to two hundred and thirty-eight.

到十一月下旬，他们的人数降到了138人。到三月底，连续好几个星期都只剩下4人。但从一开始，彻底处理好所有影响就从来不是目标。By late November, they were down to a hundred and thirty-eight. By the end of March, they'd been stuck for several weeks on just four. But settling every implication had never really been the goal.

陶认为，等式理论是探索一种全新数学研究方式的试点项目。就这一点而言，它无疑取得了成功。他设想了一门实验数学分支，类似于现代物理学：大规模协作产生海量数据，不是取代理论，而是与理论相辅相成。Tao viewed equational theories as a pilot project for a fundamentally new way of doing mathematics. And in that regard, it was an unqualified success. He imagined an experimental branch of mathematics, analogous to modern physics, massive collaborations generating huge volumes of data, not replacing theory, but complementing it.

代数定律的空间是一颗广阔而基本未经探索的星球。交换律和结合律等熟悉的岛屿早已得到深入研究，但大多数可能存在的定律仍不为人知。它们之中或许隐藏着奇异的结构，与数学迄今见过的一切都截然不同——陶有时称之为“来自火星的数学”。The space of algebraic laws was a vast, largely unexplored planet. Familiar islands such as commutativity and associativity had been thoroughly studied, but most potential laws were unknown. Hidden among them might be structures strange and unlike anything mathematics had seen before, what Tao sometimes calls math from Mars.

当团队从那张庞大的表格中逐项划掉各种蕴含关系时，意外发现了一些真正新颖的构造，其中包括 magma 上同调。约翰·贝兹是一位上同调专家，他起初曾称这个项目是浪费时间的庞大工程，但后来承认自己从未见过这种东西。对陶哲轩来说，这正是重点。As the team crossed implications off its immense table, it stumbled onto genuinely new constructions, including magma cohomology. John Baez, an expert in cohomology who had initially called the project a colossal waste of time, admitted that he had never encountered it. To Tao, that was exactly the point.

该项目证明了一种新型数学机器的有效性。2025 年 7 月，Google DeepMind 和 OpenAI 报告称，他们使用自然语言证明在国际数学奥林匹克竞赛中取得了金牌级成绩。The project had demonstrated the efficacy of a new kind of mathematical machine. In July 2025, Google DeepMind and OpenAI reported gold level scores on the International Mathematical Olympiad using natural language proofs.

Google 的结果由 IMO 官方评分，而 OpenAI 的结果则经过了单独评估。两者都没有依赖 Lean 来验证这些竞赛答案。Google's result was officially graded by the IMO, and OpenAI's was separately evaluated. Neither relied on Lean to verify those competition answers.

Lean 在人工智能数学中的地位Lean's place in AI mathematics

这会在某种程度上消除对这类验证的需求吗？毕竟现在我们已经有了用自然语言写成的证明。我认为显然两者都会有。Lean 和在那个环境中的强化学习会打造出这些引擎，这对模型训练至关重要。does that in any way negate the need for this kind of verification when we now have proofs that are just written in natural language? I think it's clearly gonna be elements of both. That lean and reinforcement learning in that environment is gonna create these the engines, is gonna be like essential for model training.

我认为，它对于探索各种可能的证明也极其有用。我的意思是，这某种程度上正是大型语言模型的价值所在：它可以生成数百万个潜在证明，但你需要迅速从中筛选出可信或正确的证明。Lean 可以告诉你哪些证明符合条件。I think it's also extremely useful for exploring a wide variety of possible proofs. I mean that's kind of the value of an LLM that it can output millions of potential proofs but you need to then quickly sort among them to the ones that are plausible or correct. Lean can tell you which ones those are.

与此同时，模型的表达能力大幅提升，以至于无需将所有内容都输出为 Lean 代码来验证其正确性。At the same time, the expressive power of the models is getting so much better that you don't need everything to be outputted in Lean code to verify its correctness.

AI 的蛮力方案与恰当的抽象AI brute force versus the right abstraction

因此，这个库的理念一直是：找到恰当的抽象，并在正确的普遍性层次上开发一切。人工智能的出现相当有意思，因为我们一直坚信，找到恰当的抽象，今后就能让我们的生活轻松一些。而现在似乎正在发生的是，你可以有一个 AI 工具，它看到书里的某个东西，完全不加思考，只是盲目地把人类写下的数学内容翻译成 Lean——也就是软件所使用的语言——而它并不怎么在乎这样做是否方便。So the philosophy of the library has always been find the right abstraction and develop everything in that correct generality. And the advent of AI has been quite interesting because we always firmly believed that finding the right abstraction would just make our lives easier later. And what seems to be happening now is you can have an AI tool which just sees something in a book, doesn't think about it at all, just blindly translates that human written, mathematics into, you know, into Lean, the language, you know, the language that the software uses, and, doesn't really care about making things easy.

如果现在要在它本该适用的普遍性层面之外，硬着头皮啃这些东西变得有点折磨，那事情就复杂得多了。作为人，当你觉得“我本来应该能轻松应对这些”时，你不会想硬撑着把它们做完。If now it becomes kind of grueling to just kind of bash through this stuff in not really the generality it should be working in, things are much more complicated, and it's as humans, you don't want to plow through stuff when you kind of feel, I should be sailing over this.

你知道，为什么，为什么一切都这么拖沓？也许我该考虑重新设计。但以目前的状态，AI其实并不在乎重新设计，它倒是很乐意就这么一路硬闯过去。know, why why is everything so bogged down? Maybe I should think about redesigning. But AI in its current state doesn't really care about redesigning, and it's very happy to just plow through.

所以，你知道，举个例子，如果我们现在真想改动库里的某个基本定义，AI 就很擅长做这件事。AI 会到处折腾根基，你知道，把一切都弄坏，然后再一路推进，把所有东西都修好。所以现在我们有了这些新工具，你知道，人们现在可以质疑这样一个基本设计原则：我们是否必须找到恰当的抽象层次？作为数学库的维护者，维护着这个所有东西都构建于其上的基础数学库，我们仍然坚信，要进入我们的库，在概念上就必须是正确的做法。So, you know, as as an example, if we did want to change a fundamental definition in the library now, AI would be great at that. AI would just it would fiddle around the roots, you know, break everything, and then it would just plow through and fix everything. And so now we have these new tools, you know, one can now question this fundamental design principle that, you know, do we do we have to find the right level of generality? the math lib maintainers, you know, this fundamental math library, which everything is building on, we are still absolutely of the opinion that to get into our library, it needs to be it needs to be, you know, conceptually, the right the right way of doing things.

但当然，现在数学领域还有很多其他发展。五年前可不是这样。你知道，世界上规模最大的 Lean 代码库，或者至少是公开可用的 Lean 代码库，就是 Lean 的数学库。But there are, of course, plenty of other developments in mathematics now. This wasn't true five years ago. You know, the largest amount of Lean code in the world was or at least publicly available Lean code was Lean's maths library.

而且这大概还算说得过去，不过你知道，一年之后，可能就会出现一些 AI 开发的库，在这些方面考虑得糟糕得多，因为不知为何，设法把事情做得简单似乎没那么重要了。如果你准备好只管往问题里灌 token，那我们未必需要找到理解这些事情的正确概念框架。我们可以随手拼凑出点东西，再把上周刚发表的一篇论文形式化。And that's probably still just about the case, but, you know, in a year's time, there will be AI developed libraries that will be much more poorly thought out in those terms because somehow trying to make it easy seems to be less of an issue. If you're prepared to just pour tokens into the problem, then we don't necessarily need to find, you know, the correct conceptual way of thinking about these things. We could just bash something out and formalize a paper that came out last week.

确实，事情就是这样。你知道吗？像 OpenAI 和 Anthropic 这样的公司在做数学，然后只是把它翻译成 Lean，却没有真正考虑这些内容是否都以恰当的普遍性完成。Indeed, this is what's happening. You know? Companies like OpenAI and Anthropic are doing mathematics and then just translating it into Lean and not really thinking about whether this is all done in the correct generality.

所以世界正在变化，而这种变化是否会让一切变得更好，还不完全清楚。它只是会变得不一样。So the world is changing, and it's and it's it's not entirely clear it's gonna be better. It's just gonna be different.

自动形式化的特洛伊木马Autoformalisation's Trojan horse

你觉得 LLM 真能帮助人们使用 Lean 这样的工具吗？如果 Lean 的难点只在于理解 Lean 语言的工作方式，以及知道该用哪些基本构件之类的，那它能让这件事变得更容易吗？这体现在两个方面。And do you think LLMs could actually help folks use things like lean? Because if the problem with lean is just understanding how the lean language works and knowing what primitives to use and whatnot, could it make that better? It's in two ways.

啊，对，我提到过，这种繁琐的 Lean 语法对数学家来说确实是一道门槛。显然，有了智能体编程，你不必学会所有那些 Lean 语法，基本上可以像写 JavaScript 一样编写代码。大家都认为，AI 会让 Lean 代码更容易编写，也可能有助于吸引更多数学家使用这个程序。大家对此很感兴趣。A, right, I mentioned that kind of writing the fiddly lean syntax as a real barrier to entry for mathematicians. Obviously with like agentic coding, you don't need to like learn all that lean, can just kind of code it the way you would write, you know, JavaScript. there there's an understanding that AI will make writing lean code a lot easier and help probably bring more mathematicians into using the program. There's enthusiasm about that.

其次，我提到你需要这个数字数学库 mathlib。而这些内容都是经过人工精心整理、非常手动地定义出来的。And then second, I mentioned that you need this library of digital mathematics, mathlib. And all of that is very hand curated material defined very manually.

有一种设想：把一本完整的数学教材交给 AI，让它自动翻译成 Lean 代码。这就是自动形式化的过程。到了 2025 年 5 月，人们希望自动形式化能大幅加快新数学内容加入 mathlib 的速度。There's a dream that you could take a full math textbook, show it to an AI and have it automatically translate it, convert it into lean code. This is the process of auto formalization. There is hope in May 2025 that auto formalization will dramatically accelerate the rate at which new math is added to mathlib.

这本书出版以来，有件事很有意思：它今年六月在美国出版，本月晚些时候将在欧洲出版。有意思的是，自动形式化如今已经开始实现了。你现在可以把一篇数学论文交给大语言模型，它就能在远远少于一组人类完成同样工作所需的时间里，生成对应的 Lean 代码版本。What's been interesting since the book came out, it came out in The States in June of this year, it's going to come out in Europe later this month. What's been interesting is auto formalization is now happening. You can now give an LLM a math paper and it can spit out the lean code version of it in, you know, a fraction of the time it would have taken a team of humans to do the same thing.

mathlib 社区其实发现，这里面有点像特洛伊木马：LLM 自动形式化有一个弊端，那就是最终会产生大量 Lean 数学内容，而这些内容的定义未必总能达到我们希望 mathlib 中这些规范对象所具备的那种精确性和简洁性。The mathlib community actually finds that there is a little bit of a Trojan horse like there's kind of a downside to LLM auto formalization and that is you just end up with this profusion of lean mathematics that are is not always defined with exactly like the precision, the economy with which you want these canonical objects in mathlib to be expressed.

因此，他们在某种程度上正面临着全世界各地都在面对的同一个挑战：AI 生成内容的海量涌现。就这个例子而言，你可能会承认，被纳入 mathlib 的 Lean 代码并不总能达到社区自身期望的标准，因此他们必须想办法从这些新材料中筛选甄别。And so they're kind of confronting in a certain way the same challenge that the rest of the world is confronting everywhere which is the volume of AI generated everything. In this case, lean code you might admit to mathlib is not always at the standard the community itself wants and they have to figure out how to kind of sift through all of this new material.

形式化鸿沟The formalisation gap

所以现在我们真的遇到了一个严重的问题：意大利面怪物。对吧？我们正在编写一些自己都看不懂的代码。So we have a real serious problem now with the spaghetti monster. Right? We are writing code that we no longer understand.

我们已经无法理解自己的代码库了。我们需要某种方式来构建可由计算机检验的规格说明。但经过检验的证明仍然可能证明了错误的东西。当 AI 给出一个著名猜想的 Lean 证明时，仍然必须有人确认，这个形式化陈述是否通过恰当的定义和假设准确表达了预期的猜想。We don't understand our code bases anymore. And we need to have some kind of way of building specifications which are computer checkable But a checked proof can still be a proof of the wrong thing. When an AI produces a lean proof of a famous conjecture, someone must still establish that the formal statement captures the intended conjecture with appropriate definitions and assumptions.

检查器会验证推导，但不会验证人类对目标的选择。这就是形式化鸿沟。信任基本上已经转移到了上游。The checker certifies the derivation, but it doesn't certify the human choice of target. This is the formalisation gap. The trust has basically moved upstream.

数学是一种，你知道，定义明确的形式语言，而这正是我们能够编写理解这种数学的计算机程序的原因。你知道，这些程序能理解人们用数学术语表达时的意思。Mathematics is a, you know, is a well specified formal language, and that's exactly why that's exactly why we can write computer programs that understand this math you know, that understand what humans mean when they speak in mathematical terms.

所以数学应该完全不存在任何歧义。因此理论上，理论上，数学的定义是完全明确的，所以非常适合这种游戏，你知道，就是把它写进形式系统，用计算机程序来表达。但在实践中，读读近期的数学论文，我们确实会发现其中有一定程度——确实有一定程度是人们在和其他专家交流，并且大家都知道，专家们大概明白人们说这些话时是什么意思。So mathematics should contain no ambiguities at all. So in theory in theory, mathematics is completely well specified and thus perfect for this kind of game, you know, writing it down in a formal system using a computer program. But in practice, reading recent mathematical papers, we do see that there's a certain amount there is a certain amount of people speaking to other experts and just knowing experts sort of know what humans mean when they say things.

所以，有时候最终写在纸面上的东西，或许能代表人类所说的数学的百分之九十九，但并非百分之百。几年前，我不会这么说。几年前，我会说人类非常出色。So sometimes what ends up on paper is sort of ninety-nine percent, but not a hundred percent representative, of what humans mean by mathematics. And a few years ago, I would not have said that. A few years ago, would have said humans are excellent.

人类是完美的。你知道，专家们，他们写下——他们总是准确地写下自己想表达的意思。Humans are perfect. You know, the experts, they write down they write down exactly what they mean at all times.

但因为我一直在做这个……仔细……的项目，所以我想告诉你一个……这是一个故事，目前还没有公开，但我会告诉你这个故事。我们把这本顶尖纯数学期刊《数学年刊》上的五十个——五十个定理的陈述写了下来。我们这周就要公开这些内容，但在公开之前，我们先把它们交给 AI 处理，并请 AI 检查了一下。But because I've been doing this project of carefully, so I'll tell you a this is a this is a story, that's not been made public yet, but I'll tell you I'll tell you a story. So we wrote down statements of fifty, fifty theorems from this top pure maths journal, the annals of mathematics. And we're going to make them public this week, but before we made them public, we ran them we ran them through an AI and asked an AI to check them.

而且 AI 发现了，AI 发现了错误，这些错误有两种。一种是我的团队犯的错误。你知道，我们没能把页面上的内容正确地翻译成软件所使用的语言。And the AI found and the AI found errors, and the errors were of two forms. There were errors that my team had made. You know, we'd, we'd failed to correctly translate what it said on the page, into the language of the software.

但还有一些更有意思的错误：我们明明忠实地照着论文里的说法翻译，可论文里的说法本身就是错的，因为那不过是他们一时的疏忽。But there were more interesting errors where we had faithfully translated exactly what it said in the paper, but what it said in the paper was just not true because they were just they were just slips.

他们是那些人类，显然没费心提到这一点：n 必须至少为 3，否则这个集合就应该是非空的。那里有……有一些东西，这是菲尔兹奖章。对吧？They were the humans hadn't bothered to mention that, obviously, n had to be at least three or, this set should be nonempty. There there were there were things that this was Fields medals. Right?

我们发现，我们发现有四位菲尔兹奖得主实际上在《数学年刊》上证明了定理。而如果你真的读一下定理的表述，那么严格来说，该定理并不成立。对吧？We found we found four Fields medalists have actually proved theorems in the annals of mathematics. And if you actually read the statement of the theorem, then strictly speaking, that theorem is not true. Right?

严格来说，他们写的内容是错误的，事实上显然不是真的。如果你是这一领域的专家，你会说：“嗯，他们显然是这个意思。”所以，你知道，我觉得这个过程挺让人谦逊的。It's strictly speaking, what they've written is false, and it is obviously not true, in fact. If you're an expert in the area, you would say, well, obviously, they mean this. So the process of you know, I think this is quite humbling.

我认为，作为一个社区，是的，我们应该审视一下，退一步想想：其实，我们说自己拥有一种精确的形式语言，能够准确表达我们的意思。I think as the as a community, yeah, we should take a look and we should step back and think, well, actually, you know, we say we've got this precise formal language where we can express exactly what we mean.

但实际上，我们的利用率只有百分之九十九左右。机器能提供的一项功能，就是让你把利用率提升到百分之百。你知道，机器会说：“嗯，你写的这个定理其实并不成立，对吧？”But in practice, we're only using it at sort of ninety-nine percent capacity. And one of the things that machines will offer you is the chance to upgrade that to a hundred percent capacity. You know, the machines will say, well, this theorem as you've written it isn't actually true, is it?

然后人类会……嗯，显然不会。大家一直都知道我们指的是这个。但现在，我们为什么不直接把它写下来呢？And then the human will well, obviously not. Always everybody knows that we mean this. But now but why don't we just write that down now?

所以你知道，这是软件让数学变得更好的方式之一。它能帮你从百分之九十九提升到百分之百。So, you know, this is one of the ways in which the software is making mathematics better. It's getting you from ninety-nine percent to a hundred percent.

证明不等于理解。A proof is not understanding

你知道，人类并没有我们自以为的那么聪明。在交互式证明助手发展的早期，正如我所说，人们的论点是，我们需要这些工具，因为它们能检查正确性、确保细节无误。但这种说法在数学界并没有得到认可。数学家们对此提出质疑，说，听着。You know, humans are not as smart as we think we are. in the early days of interactive proof assistants, like I said, the argument is that we need these because they're gonna check correctness and get the details right. That got no traction in the mathematics community. Because mathematicians, they push back and they say, look.

数学并非关乎形式主义。它不关乎公理和规则，也不关乎检查细节。Mathematics isn't about formalism. It isn't about axioms and rules. It's not about checking the details.

关键在于想法，在于理解。而且，你知道，你会想出一些点子。It's about the ideas. It's about the understanding. And, you know, you come up with ideas.

你知道，当你试图把它形式化或证明出来时，数学就会变得举步维艰。我的意思是，你就是得去做，得检查。You know, when you go to formalize or prove it, that's where the mathematics just is just just dying. I mean, it's just you gotta do it. You gotta check.

你知道，你得仔细检查。但那不是我们真正关心的。我们关心的是这些想法。You know, you gotta check carefully. But that's not what we really care about. We care about the ideas.

而且，这些想法往往是关于提出新的表征方式、新的思考事物的方式，从而让你能够解决更难的问题并走得更远。And often, the ideas, they are about coming up with a new representations, ways of thinking about things that will let you solve harder problems and get further.

所以，我的意思是，话虽如此，数学的一个特点就是它的严谨性和精确性。也就是说，我们能够对一个证明是否正确达成共识，而这取决于对细节和底层规则的检查。所以，我喜欢这样看待它：数学，以及它所具有的那种精确性和严谨性，就是媒介。So, I mean, that said, one of the things that characterizes mathematics is the level of rigor and precision. The fact that, you know, we can come to consensus about whether proof is correct or not, and that's a matter of checking the details and the rules at the bottom. So, you know, the way I like to think about it is mathematics and that level of precision and rigor, that's the medium.

那就是数学家们工作的语言，对吧？而在这种媒介中，你知道，你就有了这样一个平台，可以在上面构建这些极具创造性的想法、表达方式和理解。所以我们真正热爱的其实是这些想法，只不过它们被置于这样一个框架之中，让我们能够做到非常精确。That's the language, right, in which, you know, mathematicians work. And within that medium, then you have this, you know, you have this platform on which to build these incredibly creative ideas and modes of representation and understandings. So what we really love are the ideas, but they're couched in this in this framework where we can be very precise.

那么我想问，在形式主义之后，你究竟又多了解了些什么？And I suppose after formalism, what exactly do you know more of?

而且，而且谁知道呢？仅仅从检查正确性的角度为形式化辩护，并没有引起很多数学家的兴趣。令我惊讶的是，大约在2000年之后，你知道，Kevin Buzzard 开始写博客，他的博客迅速走红，很多非常优秀的数学家因此接触到这个领域，并对形式化感到非常兴奋。我认为他们喜欢它的原因是，你知道，当你重新审视一段自认为已经理解的数学内容，却必须把它形式化地表示出来，也就是以计算机能够理解并检查每个细节的方式表示出来时，你会发现自己在表示概念并将它们组合起来时变得非常高效。尤其是在构建一个包含许多相互关联部分的库时，你会希望这些部分能够彼此协作。And and who knows it? just arguing for formalization in terms of checking correctness didn't get a lot of mathematicians interested. To my surprise, you know, around 2000 after, you know, Kevin Buzzard started blogging and, you know, his blog went viral, a lot of very talented mathematicians came to the subject and got really excited about formalization. And I think what they liked about it was, you know, when you go back to a piece of mathematics that you think you understood, but now you have to represent it formally, you have to represent it in a way that the computer can can understand and check every detail, you find yourself getting very efficient about how you represent concepts and put them together, and especially when you're building a library with lots of moving parts, want them to interact.

你开始从计算机科学家所说的 API 的角度来思考它们。对吧？你知道，你掌握着信息，会把一些东西封装起来，也会把一些东西暴露出来；你知道，你会考虑向其他使用者公开哪类信息，以及哪些属于内部实现。You start thinking about them in terms of what computer scientists call the APIs. Right? You know, you have information, and you encapsulate things, and you expose things, and what, you know, what kind of information you're kind of making public for other people using it, what's the kind of the internals.

所以我觉得，数学家发现，用这种软件工程式的思维方式来思考数学很有用。你知道，就是想想，好吧，都有哪些不同的模块？都有哪些组成部分？And so I think mathematicians found it useful to think about mathematics in this kind of software engineering, you know, kind of way of thinking about, okay. You know, what are the different modules? What are the pieces?

它们如何相互作用？接口是什么？我认为他们发现，这为他们提供了一种回过头来理解数学的方式，你知道，以全新而有趣的方式。How do they interact? What are the interfaces? I think that they found that this gave them a way of coming back and understanding, you know, the mathematics in in new and interesting ways.

所以这其实就是在探索数学的结构，以及各个部分是如何组合起来的。So it's really just, yeah, exploring the structure of mathematics and how the pieces get put together.

我的意思是，我们正是基于这些、这些、这些非常复杂的体系搭建起来的，而这些体系又建立在非常精确的规则之上。理解这种复杂程度是如何从最底层极其简单的规则中产生的，确实令人惊叹。除了围绕项目展开的具体战术讨论外，Commelin 和 Scholze 还探讨了形式化的哲学层面。Commelin 认为 Lean 是一种更好的工作方式。I mean, we built up these these these very complex edifices on top of these, you know, kind of very, very precise rules and understanding how you get that level of complexity, you know, down to the very simple rules at the bottom, is really remarkable. Alongside concrete tactical discussions about the projects, Commelin and Scholze debated philosophical aspects of formalization. Commelin saw lean as a better way to work.

Scholze 则没有。这种不同的取向，体现在 Commelin 和 Scholze 关于数学定义应如何书写的 Zulip 交流中。如何知道用 Lean 写下的定义忠实于数学家通常所理解的对象定义？Scholze did not. These different orientations came through in Commelin and Scholze's Zulip exchanges about what it meant to write definitions in math. How do you know that a definition written in lean is faithful to the definition of an object as mathematicians conventionally understand it?

在很多方面，为一个对象找到恰当的定义，就是数学的全部关键所在。In many ways, coming up with the right definition for an object is the whole game in mathematics.

数学家定义新的对象、新的框架和抽象概念，是在为这个领域提供新的工具和视角。Scholze担心，如果这些定义在 Lean 中有误，就没人能看出来。即使证明实际上并不正确，Lean 也可能会验证它是正确的。When mathematicians define new objects or new frameworks and abstractions, they are equipping the field with new tools and perspectives. And Scholze worried that if the definitions were wrong in Lean, nobody could tell. Lean might verify the proof is correct even when it wasn't.

他在 Zulip 上总结了这个难题。我目前只是觉得，数学仍然是一项人类活动。因为如果我真的要确认计算机做对了，就得在脑海中梳理整个证明，并检查它是否确实成立。He summed up the conundrum on Zulip. I'm just currently feeling that mathematics remains a human activity. Because if I were to truly check that the computer did the right thing, I would have to unravel the whole proof in my head and check that it really adds up.

Lean 可以验证证明，但无法检查定义，因为从逻辑上讲，定义无所谓对错。定义就是你说它是什么，它就是什么。因此，Commelin 和 Topaz 寻求另一种安心的方式。Lean could verify proofs, but it couldn't check definitions because, logically speaking, definitions aren't right or wrong. They're just what you say they are. So Commelin and Topaz looked for another form of reassurance.

他们创建了一个包含具体示例的文件，并为最重要的定义编写了单元测试。They created a file of concrete examples, unit tests for the most important definitions.

如果这些定义所导出的对象看起来像鸭子，叫起来也像鸭子，那么它们或许真的就是在定义鸭子。这些例子并非无懈可击的证据，但科梅林认为，它们至少和阅读数学论文中的定义一样可靠，甚至可能更可靠，因为数学家在审阅彼此的作品时，很容易只看到自己预期看到的东西。If the definitions yielded objects that looked like a duck and quacked like a duck, perhaps they really were defining a duck. The examples were not watertight evidence, but Commelin thought they were at least as reliable as reading definitions in a mathematical paper, perhaps even more so, given how easy it is for mathematicians to see what they expect to see when reviewing one another's work.

集成噩梦与 zlib 规范Integration hell and the zlib specification

而且，选择往往并非唯一。纸面上看似等价的概念，可以用多种形式上都成立的方式来表示。某种选择在局部可行，但随着围绕它构建的库不断扩展，可能会变得脆弱，甚至难以辨认。And the choice is rarely unique. Concepts that look equivalent on paper can be represented in several formally valid ways. A choice that works locally can become brittle or even unrecognizable when a library grows around it.

数学也有自己的集成地狱，而且每个看起来似乎可行的贡献，都会给别人带来审查负担。我记得凯文的书里有一段，他说有一次你把一大批人踢出了 Slack 频道。你说：“听着，我现在得、我现在得专心了，因为这实在是、这已经越来越离谱了。”Mathematics has its own integration hell, and every plausible looking contribution creates a review burden for somebody else. 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. You said, look, I just need to I just need to focus now because it's just it was getting ridiculous.

我当时想做出一个能用的东西。有些人也在这个，呃，频道里玩得很开心，随便抛出各种想法。对吧？I was trying to build something that works. Some people were there in this, like, channel having fun throwing ideas on the wall. Right?

我的意思是，这成本很低。你可以不断抛出各种想法，而对方只能不停地告诉你：不行。I mean, it's cheap. I mean, you can throw ideas on the wall, and the other side has to keep telling you, no.

这行不通。这是让我很沮丧的一种情况。你提出一个想法。This doesn't work. Something 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 ten minutes to find the hole the next hole. It keeps taking exponentially longer to find the holes on the half-baked idea.

对想出这些点子的人来说，这很有趣。但对接收这些点子的人来说，就没那么有趣了，对吧？For the person coming up with them, it's fun. I mean but it's not fun from your receiver. Right?

你现在必须开始工作。You have to do your work now.

lean-zip（zlib 证明）lean-zip (the zlib proof)

你花时间告诉人们为什么这不是个好主意，为什么现在不是做这件事的时候。所以我们应该在这里举一个具体的例子。显然，Kim Morrison 使用 Claude agents 编写了压缩格式 zlib 的 Lean 实现，并证明了它的一些特定性质。You spend time telling people why this is not a good idea, why it's not the time you should do it. So we should come up with a concrete example here. So, apparently, Kim Morrison used the Claude agents to produce a Lean implementation of the compression format zlib and and prove some specific properties of it.

那么他们究竟证明了什么？AI 成功地把 C 代码翻译成了 Lean 代码，然后不断修正 Lean 实现，直到它通过了 C 版本自带的测试套件。接着，它证明了：对于任意压缩级别和任意数据，压缩后再解压，都能还原出原始数据。So what exactly did they manage to prove? But the AI managed to translate from C to Lean, the code, then managed to keep fixing the Lean implementation till it passed 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.

我把它比作盲人摸象：这些盲人分别摸着大象的不同部位。他们了解大象的一部分，却不了解全貌。I liken it to the blind men and the elephant, which is that you have all of these blind men feeling different parts of the elephant. And they understand parts of the elephant, but they don't understand the whole.

我不知道 zlib 这件事是不是也类似：它究竟涵盖了整体，还是只涵盖了其中某个视角。不过我想，当你看到的只是一个更大、更复杂整体的某个视角时，就会遇到一些问题。比如，我们谈到奖励投机、古德哈特定律，以及各种各样的退化行为——如果你只优化系统的一部分，这些情况都可能发生。那么，这是不是这里讨论的一部分？And I don't know whether it's a similar thing with this zlib, whether it actually encompass the whole or just some perspective of it. But I suppose the problem when you only have a perspective of a bigger complex whole, you get problems in terms of, know, we're talking about reward hacking and, you know, like, Goodhart's law and all all kinds of, you know, degenerate behavior can happen if you optimize only part of a system. So is that is that part of the story here?

它实际上涵盖了整个 Zlib 算法吗？是的。是的。What was it actually encompassing the whole Zlib algorithm? Yes. Yes.

例如，在这种压缩与解压任务中，一种奖励黑客行为是：假设我们要求 AI 展示给我们看、以证明任务已完成的唯一属性就是这一点，那么 AI 就可以钻空子：所谓压缩，只要把数据原样返回就行。For example, one way to do reward hacking in this compression decompression. Suppose that's that's what's the only property we ask is the AI to show, to demonstrate to us that was achieved. The AI could hack by saying compression, you just return the data.

这是恒等函数。你只需原样返回。解压缩时，也把它原样返回。It's the identity function. You just return. Decompression, you return it back.

你证明这个性质，对吧？但之后你还可以添加更多性质，比如要求输出小于输入。You prove the property. Right? But then you can put more properties like saying you the outputs should be smaller than inputs.

对吧？那你也应该告诉 AI。你必须证明，在测试套件中，你的压缩效果和 Rust 实现一样好。Right? Then you should also tell the AI. You have to show that you compress as much as the Rust implementation in the test suites.

但你说得完全对。很容易给出的属性并不能涵盖整个对象，对吧？But you're completely right. It's really easy to give properties that do not cover the whole thing. Right?

如果你把 AI 看作辅助工具，也会亲自参与其中、查看代码，那么我认为你提出的这个问题并没有特别令人担忧。但如果你放任 AI 自由发挥，甚至连代码都不想看，那么全面覆盖所有方面就非常重要。And if you want to do if you see the AI as an assistance to you, that's you're in the loop looking at the codes. I think this is not super concerning this problem you raised. But if you let once you let the AI go wild and you don't even want to look at the codes, It's really important to cover all aspects.

对吧？否则，你可能会有一个满足所有属性的实现，但却没有完整说明你想要什么。Right? So otherwise, you can have implementation that satisfies all your properties, but you do not fully specify what you wanted.

你并没有真正得到自己想要的东西。You're not really getting what you want.

AI 软件生命周期中的验证Verification in the AI software lifecycle

有些人怀疑，正是因为这个原因，形式化验证是否能广泛用于验证所有这些 AI 生成代码的正确性。对于复杂程度达到大多数程序这种水平的程序，根本不可能为它们编写规格说明。你觉得，随着代理式工程的发展，未来会是怎样的？there's some skepticism that formal verification is gonna be broadly useful for verifying the correctness of all of this AI generated code precisely for that reason. There's just like no way to write specifications for programs that are operating at the level of complexity as most programs are. And how do you see this panning out in the future with agentic engineering?

那么，你觉得我们会不会想出某种规范、约束体系、新的工作方式和工程方法，从根本上解决这种分歧问题？我想，你可以把它称为“理解债”，对吧？问题在于，我们正在构建一些自己已经无法理解的东西。So do you think we will come up with some kind of, yes, specifications, systems of constraints, new ways of working, new ways of engineering to essentially solve this divergence problem? I guess you could call it understanding debt, right? There's this problem of building things we no longer understand.

我们没法验证它们。说实际点，你觉得我们怎么才能从工程层面解决这个问题？目前，智能体编程的效用完全卡在审查和验证这一阶段。We can't verify them. Like, practically, how do you think we can engineer this problem away? the utility of agentic coding is completely bottlenecked right now on this review and verification phase.

我认为，AI 本身会让软件验证变得强大得多，因为你可以用 AI 来编写这些规范，而不必手动编写。我认为，软件程序的形式化验证将在新型 AI 驱动的软件开发生命周期中发挥越来越重要的作用。像 Harmonic 这样的公司就相信，如果能训练 AI 模型编写数学证明，那么同样的智能也能用于编写关于软件的证明，以验证 LLM 的输出。I think that AI itself makes software verification kind of much more powerful because you can use AI to write these specifications themselves. They don't have to be written by hand. Basically, I think kind of formal verification of software programs will like increasingly have a role to play in the new AI powered software development life cycle. there are places like Harmonic which believe that if you can train an AI model to write math proofs, that same intelligence will be useful for writing proofs about software for verifying the output of LLMs.

所以我也不清楚。这种赌注已经开始了。So I don't know. That kind of bet is underway.

精益背后的人文故事The human story behind Lean

至于最终能否成功，我也不知道。因此，在这一切软件的背后，是一个非常人性的故事：关系的破裂、创新，以及令人难以置信的坚持。而这一切催生了某种彻底改变数学世界的东西，而且它至今仍在每天持续推动着变革。Whether or not it pans out, I don't know. So underneath all of this software was a very human story of fracturous relationships, of innovation, of incredible persistence. And it has led to something which has just revolutionized the world of mathematics and is continuing to do so on a daily basis.

所以，人工智能正在向数学发起挑战。这一点毫无疑问。至于它会给数学带来什么，没人真正知道。So AI is coming for mathematics. This is absolutely clear. And what it's gonna do to it, nobody really knows.

我们所知道的只有一点：它正在以极快的速度变得非常出色，而没有人知道它究竟还能变得多好。因此，数学家对此有各种不同的反应，从只能称之为悲痛的情绪——因为这个学科正在发生变化，他们不得不适应，否则就会被淘汰——到兴奋不等。而我非常偏向兴奋这一端。我认为，这款软件将极大地加速数学的发展，因为别忘了，它已经能做出一些很有意思的事情了。All that we know is it's getting really good really quickly, and no one has any understanding of how much better it's gonna get. So mathematicians have had various different reactions to this ranging from, you know, what could only be described as grief, that the subject is changing and that they're gonna have to adapt or or die. So ranging from grief to excitement, and I'm very much excitement end of the scale, I think mathematics is gonna be hugely accelerated by this software because, remember, it's already doing interesting things.

而你必须记住的是，它现在是最糟糕的。你知道，今天已经是它最糟的一天了，对吧？And the thing you have to remember is it's it's it's worst. You know, today is the worst it will be. Right?

今后情况会好得多。现在已经很棒了，而一年后的今天，它会比现在好得多。所以我认为，AI 为数学打开了巨大的新可能性。Going forward, it's gonna be much better. It's already awesome, and it's much worse than what it will be this time next year. So I think AI opens up huge new possibilities for mathematics.

它会改变数学的许多方面，但归根结底，我们会获得更多理解，证明更多定理，也会对数学究竟是什么有更全面的认识，并拥有强大的工具，让我们能够探索那些未知的角落，照亮它们，也照亮我们的社群。展望未来，前景令人振奋。我们的目标之所以特别，是因为它们是我们自己的。It will change many things about it, but at the end of the day, we're gonna end up with more understanding. We're gonna end up with more theorems proved, and we're gonna end up, you know, with just a better overview of what mathematics is and and great tools where we can explore new dark corners and enlighten them and enlighten our community. So going forward, things look very exciting. what makes our goals special is that they're ours.

它们是目标。我是说，你我正在进行这场对话。They are goals. I mean, you and I are having this conversation.

对吧？而我们要讨论的是：我们该怎么做？我们该如何看待 AI，又该如何应对 AI？Right? And the conversation is what should we do? What should we make of AI, and how should we respond to AI?

我们该拿 AI 怎么办？对吧？我们正在进行这场对话，我是说，我很乐意让 AI 在一旁讨论它的目标是什么，以及它应该努力做些什么。What should we do with AI? Right? We're having this converse I mean, I'm happy to let AI have its discussion on the side about what its goals are and what it should be trying to do.

对吧？我对那个不感兴趣。对吧？Right? That doesn't interest me. Right?

我的意思是，你告诉我角落里有台服务器，它在做它该做的事、证明定理之类的。你知道，我再说一遍，我关心的是我要怎么跟它交互？所以，嗯，不是说我不知道。I mean, you tell me that there's some server in the corner, and it's doing whatever it's doing and proving theorems and so on. You know, again, what I care about is how how am I gonna interact with it? So, yeah, it's not that I don't know.

我想，我们再次应该关注的问题是：我们的目标是什么？我们应该做些什么来实现这些目标？我不知道。我的意思是，它只是在这一点上才属于人类中心主义。It's, again, the questions I think that we should be interested in are what are our goals, and what should we be doing to achieve them? I don't know. So, I mean, it's anthropocentrism only in that.

我们就是这样的人，对吧？That's what we are. Right?

所以，没错，我觉得我们应该处于这场辩论的中心，毕竟参与辩论的人就是我们。所以，如果这是我们的——既然这是我们的辩论，我们难免会把它变成关于……呃，应该说，是关于我们想要什么的讨论。我开始写这本书后，花了很多时间和莱昂纳多·德·莫拉在一起；那其实是我第一次以某种方式理解自己正在做的事情有多重要。So, yeah, I think we should be at the center of the debate just because we're the ones having the debate. And so if it's our and so far as it's our debate, we can't help it make it about help but make it about what, you know, what we want. Once I started writing the book, spent a lot of time with Leonardo de Moura and that was actually kind of the first moment in which I understood in a certain way the significance of what I was doing.

并不是说要面向全世界，而更像是我和消息来源之间的一种伦理契约：这是 Leo 一生的事业，他对此非常在乎。我的书很可能是唯一一部从头到尾讲述 Lean 开发历程的作品，所以我开始觉得，把这个故事讲好极其重要。后来，一个叫 Kevin Hartnett 的人联系了我。他当时在《Quanta》杂志工作，想为《Quanta》写一篇关于 Lean 及其数学库的文章。Not like for the world, but just like as a kind of an ethical contract almost between me and the sources which is this was Leo's life work and he cared a tremendous amount about it. And my book was likely to be the only kind of start to finish story of the development of lean and just started to feel extremely important to tell the story well. And I was contacted by a guy called Kevin Hartnett, who at the time worked for Quanta magazine and wanted to run a piece on on Lean's Lean and its mathematics library, for Quanta.

所以我那时候碰到了凯文，你知道，我们就成了朋友。他就各种事情采访了我好几次，后来决定这个故事很有意思，值得写成一本书。你知道，我觉得这个决定挺有意思的，不过他还是决定这么做了。So I ran into Kevin around then, and, you know, we became friends. And he interviewed me several times about several things, and then later on decided that this was such an interesting story that it was sort of worth writing a book on. You know, a decision which I thought was quite an interesting one, but he went for it.

在那段时间里，他又多次采访我，试图大致弄清楚事情是怎么发生的。你知道，他想把故事背后的人物和当时发生的事情串联起来。所以，我的中年危机——我开始担心人类创造的数学，并思考机器是否能以某种方式做得更好——在凯文决定讲述的故事中也起到了一定作用。And during that time, he interviewed me many more times and tried to get some kind of idea as to sort of how it happened. You know, he wanted to put together, you know, the people behind the story and what was going on. And so my midlife crisis, where I started worrying about human generated mathematics and asking whether machines could do it better somehow played a role in Kevin's in the story that Kevin decided to tell.

随着我在书中接触到越来越多的人物、越来越多的数学家，我也逐渐明白这对他们有多重要。As I met more and more figures in the book, more mathematicians, I similarly understood how important it was to them.

我花了很多时间研究这本书的六七个关键核心资料来源。这群人留下了大量关于他们所有工作的数字记录，这对我也非常有帮助。他们最初经常通过电子邮件交流，并与我分享了大量私人邮件。I spent a lot of time with the six or seven key core sources for the book. It was also very useful to me that this group of people left a tremendous digital record of all of their work. They were initially very active over email and they shared a large number of their private emails with me.

后来，他们又转到了一个名为 Zulip 的聊天平台，在那里，他们的大量工作都是在公开讨论串中开展的，也会通过私信交流，并把这些内容分享给我。因此，我得以重构他们的大量工作，仿佛自己就在现场，亲眼目睹事情发生的那一刻。这对写这本书帮助极大。They also then later migrated to this chat platform called Zulip where they conducted a lot of their work in these public threads and then also in private DMs which they shared with me. And so I was able to kind of reconstruct a lot of the work as if I was like there observing it and in the moment it was taking place. So that was like a tremendous benefit to writing the book.

显然，凯文写这本书的时候，我想你给了、给了他查看那些邮件的权限。凯文有没有漏掉什么有意思的内容？Obviously, Kevin, when he was writing the book, I think you gave you gave him access to those emails. Were there any interesting bits that Kevin left out?

你知道，你不想把家丑在大庭广众之下抖出来，对吧？我的意思是，参与 Lean 项目的人，大家就像一家人一样，真是不可思议。你懂吧？you know, you don't wanna air your dirty laundry, you know, in public. I mean, the thing about the people working on Lean, it's just a wonder it's like family. You know?

那是一个很棒的社群，里面都是好朋友。参与这个项目的每个人都还很年轻，充满理想，也对项目兴致勃勃。你知道，我们都觉得自己正在做一件有趣而重要的事。不过，就像很多家庭里的事一样，有时候家人也会让你抓狂。It's just a wonderful community of good friends, and everybody working on the project was kind of young and idealistic and excited about it. And, you know, we all felt that we were doing something interesting and important. But, you know, like a lot of things with family, sometimes family drives you crazy.

你知道，你到了家庭聚会，那里有个疯疯癫癫的，啊，他们全都……所以，最初凯文采访我们的时候，你知道，过程中有些磕磕绊绊，也有一些……你知道，有这些紧张关系。不过我们不想老揪着这些不放，对吧？You know, you get to the family get together, and there's the crazy ah, and they're all the and so, you know, initially when Kevin interviewed us, you know, there were there were the bumpy spots along the way, and there were the you know, there were these tensions. And but we don't wanna dwell on them. Right?

于是，一位外部记者，你知道，一名记者走了进来。And so an outside reporter, you know, journalist comes in.

所以一开始我们非常谨慎。但我想，后来我们开始信任凯文，是因为我们终于明白，他并不是在寻找什么好人和坏人，也不是想做揭露性报道、讲什么丑闻，或类似的东西；他真正想做的，是以尊重所有相关者的方式，向我们讲述这个故事。既然如此，我想，他确实和很多人交谈过，而且我认为他很好地捕捉到了参与这个项目时的感受和兴奋之情。And so we were very guarded at first. But I think we came to trust Kevin when it really became clear that he wasn't looking for, you know, good guys and bad guys or an expose or a scandal story or anything like that, that he was really trying to tell us tell the story in a way that was respectful to everyone involved. So when that when that was the case, I think I mean, he really spoke to a lot of people, And I think he really did a good job of capturing the feel and the excitement of working on the project.

而且当时也存在一些紧张关系，某种程度上，你知道，得把这种情况呈现出来。再说，这并不是好人和坏人的问题，只是人们想要的东西各不相同。我在报道这件事时有过这样一段经历：大约在 2018 年那段时间，Leo 离开去开发 Lean 4，与此同时，所有数学活动以及 Mathlib 的工作仍在稳步推进，而在那几年里，我始终觉得自己好像并不明白究竟发生了什么。And when there were tensions involved, sort of, you know, making them making it come across it. Again, it wasn't a matter of good guys and bad guys, but just people looking for different things. there was this experience I had reporting it where for a period around 2018 Leo goes off and builds lean four and simultaneously all the math activity and mathlib is still continuing apace and it just never felt like kind of like I understood what was going on in those years.

我当时完全搞不清楚 Leo 有没有在和数学家们交流。这有点像有人给你讲了个故事，你觉得哪里不太对劲，却说不出原因。最终我了解到，Leo 和数学界之间发生了一次颇为决绝的决裂；他说：“我要自己单干，开发 Lean 4。”It was very not clear to me if Leo was talking to the mathematicians or not. It was kind of a situation where someone has told you a story, it doesn't quite make sense to you but you don't know why. Ultimately what I learned is there had been a somewhat decisive fracture between Leo and the math community where he says, I'm gonna go off on my own and build lean lean four.

请明确地告诉我，别来烦我。然后他们多少、他们多少确实明白了这个意思。他们有点担心惹恼这个他们敬佩的人，而这对他们来说实在、实在太重要了。Please leave me alone in so many words. And they kind of they kind of actually they get the message. They're a little wary of like angering this guy who they admire and it's so it's so important to them.

书里我谈到过一些具体的人格冲突，发生在 Leo 和一个叫 Mario Carneiro 的人之间。他们俩都对这个正在兴起的世界应该是什么样子有着强烈的设想。Mario 的设想，就是他希望 mathlib 成为什么样子。There's some particular personality conflicts that I talked about in the book between Leo and this guy Mario Carneiro who both are just have strong visions for what they want this kind of emerging world to look like. Mario's vision is what he wants mathlib to look like.

他是个坚定的开源信仰者。Leo 对 Lean 的愿景大致是这样的。两人经常发生冲突；在某种程度上，2018 到 2022 年间，这种摩擦以这样的方式让 Leo 逐渐疏远了数学家们。He's very much a big open source believer. Leo's vision is for like lean. The two of them clash quite a lot and in certain ways kind of that friction pushes Leo away from the mathematicians in this way, in this 2018 to 2022 period.

不过，对我来说有意思的是，我意识到自己一直在听这个故事，却觉得它不太说得通，也不太明白为什么。然后几乎就在一瞬间，我接触到的那些人物、那些消息来源就像是突然说：“哦，事情实际上是这样的。Leo 生气了，而且有一阵子离开了这个圈子。”当然，一旦你让一个人讲出他那一方的说法，其他人也就更愿意讲自己的了。Anyway, what was interesting for me though was realizing I've been like hearing this story, it didn't quite make sense to me, I didn't quite know why, and then almost in like in a rush, the various figures, the sources I was working with kind of said, oh, this in fact is what's going on. Leo was mad and kind of had left left the sphere for a little while. And of course once once you get one person to explain their side of the story, others are kind of more forthcoming about theirs as well.

生日漫步The birthday walk

所以我觉得，到了最后，我至少在人际关系层面上，算是彻底理解了 Lean 这件事背后发生的情况。如果你读过那本书，就会知道有段时间 Leo 对用户——其实是对所有用户，但尤其是数学用户——感到很沮丧。而他在开发 Lean 4 时，有点抽身出来了；你知道，他当时需要保持一些距离。So I think that's how I felt like by the end, I had understood at least kind of interpersonally fully what was going on with Lean. So so if you read the book, there was a period where Leo was just kind of frustrated with with well, really all users, but especially the mathematical users. And while he was working on Lean 4, he kind of pulled off and, you know, he kind of needed his distance.

而且，你知道，偶尔我会给他发封邮件，也能很快收到回复，但很明显，他想保持些距离。这挺难受的。你知道，我很想念他，因为他是——他是个非常好的朋友。我也怀念那种随时都能和他交流想法、碰撞思路的感觉。And, you know, every once in while, I'd send him an email and get a quick response, but it was clear that he wanted some distance. And that was hard. You know, I missed him because he's he's a very good friend, and I missed just kind of constantly being able to bounce off ideas and so on.

于是我联系了他。当时，正如书里所解释的，我要去西雅图参加联合数学年会，也就是你知道的，美国每年举办的大型数学会议。于是 Leo 安排了晚餐。And so I contact him. So I was in, as the book explains, I was coming to Seattle for the joint mathematics, the big American you know, big US math meeting every year. And so Leo arranged the dinner.

是的，当时镇上还有其他人是来参加会议的。It was, other people were in town for the conference.

他决定借此机会召集一些顾问，参与精益聚焦研究。所以那并不是、并不是一场生日晚宴。实际上，他只是把一些对精益感兴趣、支持精益的人聚到一起。He decided to take the opportunity to bring together advisers for the Lean Focused Research. So it wasn't it wasn't a birthday dinner. It was it was really just bringing together people, you know, interested in Lean and, supporting Lean.

不过我告诉他，那周是我的生日，于是他决定把这件事安排在我生日那天。我真的很期待。不是那顿晚餐，而是第二天。But I told him that my birthday was that week, and he decided to make it coincide with my birthday. I really was looking forward to it. Was not that dinner, but the next day.

他刚从工作中请了一个下午的假。我也从会议上请了一个下午的假。然后我们就在派克那儿碰面，就这么走啊走啊，走了好久。He just took an afternoon off from work. I took an afternoon off from the conference. And we just met at Pike's place, and we just kinda just walked and just walked and walked.

而且，嗯，那真是、真是、真是很棒，能再次和他聊聊天。是啊。我们聊了 Lean，也聊了些与 Lean 无关的事情。And, yeah, it was it was just it was just it was great talking to him again. Yeah. We talked about Lean, but we talked about things that were not Lean.

是啊。我是说，对我们俩来说，过去这几年都像梦一样。Yeah. I mean, for both of us, it's been I mean, the last several years has been surreal.

我是说，我们只是回忆一下 Lean 的早期岁月，你知道。是啊。我还记得那时候只有我和几个学生，也记得我去微软拜访 Leo、参与这个项目的那段时光。I mean, we just remember the early days of Lean, you know. Yeah. Again, I can remember when it was just me and some students, and I remember my time visiting Leo at Microsoft and working on the project.

所以回顾这一切，几乎让人觉得不真实。And so looking looking back on all that, it almost seems surreal.

告别Farewell

我是说，我们走到今天这一步，感觉真的很不真实，你知道吧。凯文·哈特纳确实让这个故事鲜活了起来。我想，他花了好几年研究这个故事，也采访了所有这些人。I mean, it seems very surreal, you know, how far we've come. Now, Kevin Hartner really brought this story to life. He spent, I think, years researching this story, speaking of all of these guys.

所以我强烈建议你阅读凯文的书。下次再见，干杯。So I highly recommend you read Kevin's book. And until the next time, cheers.