Lean's de Moura Says AI Eliminates Software Proof Overhead

Lean创始人de Moura表示AI消除了软件形式化证明的开销 语言模型的自动化证明生成消除了形式化验证以往高达十倍的人力代价，使工程师能够用经机器检查的数学规范取代传统测试。 Leonardo de Moura深入解析了Lean的架构与理念，阐明其兼具交互式定理证明器和完备函数式编程语言的双重属性，如何弥合数学证明与现实软件工程之间的鸿沟。他探讨了现代AI模型如何通过根据高级规范自动合成优化实现及机器可验证的正确性证明，从根本上降低形式化验证以往高昂的维护成本。此外，de Moura还将Lean与Z3等“一键式”SMT求解器进行了对比，回顾了凝聚张量实验（Liquid Tensor Experiment）和国际数学奥林匹克（IMO）解题等里程碑事件，并分享了随着该项目在工业验证领域不断拓展影响力，Lean 4在实现自举过程中所经历的工程艰辛。 Lean将函数式编程与依值类型论相结合，使开发者和数学家能够编写代码，并依托仅约5,000行代码且绝无差错的验证内核来证明正确性不变量。 (0:00) 大语言模型与Lean的结合消除了形式化验证以往高达10倍的额外开销，能够自动合成代码实现、生成证明，并在代码重构时维持这些证明。 (5:21) Peter Scholze的凝聚张量实验以及DeepMind在IMO上取得成果的AlphaProof等里程碑表明，形式化证明助手既可作为协作引擎，也能充当机器可检查的强化学习沙箱。 (24:11) 将Lean 4转变为自举语言需要跨越1,000多个文件手动编写约100,000行代码的底层证明，这为完全的编译器可扩展性和大规模工业验证铺平了道路。 (49:13)

Lean creator Leonardo de Moura argues that coupling formal proof assistants with large language models eliminates the historic engineering bottlenecks of software verification and fundamentally alters how mathematics is practiced. AI Overcomes the Manual Verification Bottleneck (7:45) Historically, formal verification was economically impractical for mainstream software development. Leonardo de Moura notes that verifying a program previously required roughly ten times the effort of writing the original code ($10X$), creating an unsustainable maintenance burden whenever refactoring broke brittle proofs. Projects like the seL4 microkernel and infrastructure at Amazon Web Services (AWS) relied on tedious, manual proof construction. Specification-Driven Synthesis and Safe Optimization (5:21) Rather than verifying existing code retroactively, de Moura highlights an emerging workflow where developers define mathematical specifications and rely on AI to synthesize both implementation and machine-checked proofs. In an experiment led by Kim Morrison, an AI ported the C library zlib to Lean and formally verified its round-trip compression invariant within a single week. Once proofs are established, developers can aggressively optimize code for performance because the proof assistant guarantees functional equivalence without manual auditing. Architectural Foundation: Kernels and Dependent Types (17:49) To maintain absolute trust despite a rapidly evolving compiler, Lean isolates correctness inside an independent, minimal trusted kernel of approximately 5,000 lines of code. Under the Curry-Howard correspondence, the kernel simply validates that proof terms match theorem types. Independent checkers, such as Mario Carneiro's verified Lean4Lean, ensure that bugs in the primary compiler do not compromise soundness. De Moura emphasizes that Lean relies on dependent type theory rather than higher-order logic (HOL) because modern abstract mathematics requires types that depend directly on values. While HOL was easier to implement, prominent mathematicians including Terence Tao and Kevin Buzzard required dependent types to treat abstract algebraic structures as first-class citizens. Interactive Collaboration and Mathematical Frontiers (24:11) Lean gained widespread credibility in pure mathematics through the Liquid Tensor Experiment in 2020, where Johan Commelin's team formalized and simplified complex condensed mathematics concepts for Fields Medalist Peter Scholze. Lean's real-time InfoView provides immediate deductive feedback, allowing collaborators to construct and refactor arguments without needing complete prior understanding of the entire proof. Automated reasoning pipelines treat Lean's interactive tactic mode like a game board, using reinforcement learning to discharge proof obligations. Systems developed by DeepMind, Harmonic, and ByteDance have achieved medal milestones on International Mathematical Olympiad (IMO) benchmarks. Furthermore, OpenAI researcher Boris Alexeev formalized a million-line Lean proof for a unit distance conjecture variant within two weeks. SMT Solvers Versus Interactive Proof Assistants (38:55) De Moura contrasts Lean with the Z3 SMT solver he previously co-developed at Microsoft Research. While Z3 acts as an automated, push-button constraint solver designed to find bugs in decidable theories, it struggles with proof instability and undecidable universal quantifiers. Lean avoids these heuristic failures by decomposing proofs into modular, step-by-step tactics, providing the structural granularity that modern language models need to verify total bug absence. De Moura maintains that while automated formalization will reshape research and software engineering over the next decade, human mathematicians will not become obsolete. He forecasts a hybrid future where machines verify correctness and synthesize low-level code, while humans continue writing artisanal, explanatory proofs to communicate mathematical intuition.

Lean 创始人 Leonardo de Moura 指出，形式化验证与大语言模型的结合正在重构软件工程与前沿数学，通过将规范作为真理标准，AI 能够自动合成代码并生成机器可检查的证明，从而消除传统形式化方法极高的维护成本。 规约驱动与 AI 代码综合 (1:30) 传统软件测试遵循迪杰斯特拉的格言，仅能证明缺陷的存在而无法证明其不存在。de Moura 指出，在 Lean 中编写程序和数学性质能够提供绝对的机器检查保证。针对 C 或 Rust 等现有语言，工程师可采用浅嵌入（将代码翻译为 Lean 等价结构）或深嵌入（在 Lean 中对目标语言操作语义建模）进行验证。以往编写形式化验证所需工作量通常是编写程序的十倍，且代码重构时证明维护极为痛苦。 当前 AI 与形式化系统的结合扭转了这一经济成本。开发者只需给出精确的数学规约或简单的天真参考实现，AI 即可自动合成生产代码与证明。de Moura 举例称，Kim Morrison 团队在短短一周内利用 AI 将 C 语言压缩库 zlib 移植至 Lean，并自动生成了压缩后解压无损还原的往返不变性证明。这种模式将形式化验证转化为“零风险优化”的安全护栏：开发者允许 AI 大胆优化运行时性能，定理证明器则确保任何微调都不会破坏功能正确性。 系统架构与极小受信任内核 (13:15) Lean 4 不仅是交互式证明助手，还是一门自托管的通用纯函数式编程语言，其构建工具 Lake、文档系统 Verso 乃至包含 50 万行 Lean 代码的 AWS AI 加速器编译器均采用该语言实现。用户通过 VS Code 的 InfoView 界面进入交互式“策略模式”（如使用 by 关键字、simp 简化器和改写规则），实时查看待解决的目标与假设状态，这种即时反馈循环被部分用户比作解决极度引人入胜的计算机游戏。 在底层信任机制上，整个编译器和展开器虽然庞大复杂，但系统的正确性仅依赖于一个约 5,000 行代码的极小受信任内核。基于柯里-霍华德同构，Lean 将证明检查等同于类型检查。为消除单一实现的缺陷风险，社区构建了多个独立内核，例如 Mario Carneiro 使用 Lean 语言编写并在其自身语义下通过验证的 Lean4Lean，以及 Rust 编写的第三方内核，通过多内核冗余交叉验证确保数学结论的可靠性。 从 SMT 启发式到逐步交互推理 (38:55) 对比自身此前开发的 Z3 SMT 求解器与 Lean，de Moura 阐述了二者的本质差异。Z3 是全自动的一键式约束求解器，在算术与数组等受限理论中通过搜索反例寻找漏洞，但面对复杂系统的全称量词时会遭遇理论上的不可判定性。其实际应用经常受困于“证明不稳定性”，例如仅将逻辑与条件的顺序由 A 且 B 颠倒为 B 且 A，启发式搜索就可能失效并超时中断。 这种自动化瓶颈促使 de Moura 启动了 Lean 项目。Lean 将粗暴的一键求解拆解为细粒度的逻辑推理步骤，不仅允许人类将大目标分解为引理，也契合了大语言模型逐步生成中间步骤的工作机制。在理论基础的选择上，Lean 放弃了工程实现更容易的高阶逻辑（HOL），采用依值类型论（Dependent Type Theory），使得类型能够依赖于具体运行时的值与前置条件证明，从而具备完整表达现代高度抽象代数结构的能力。 前沿数学突破与手写数学的未来 (24:11) 在纯数学领域，Lean 已从基准测试工具演进为前沿研究平台。国际数学奥林匹克（IMO）竞赛题曾被视为机器证明的禁区，如今 DeepMind AlphaProof、Harmonic 和字节跳动等团队已通过强化学习配合 Lean 摘得奖牌。在极高难度猜想上，OpenAI 的 Boris Alexeev 仅用约两周时间就将单位距离猜想变体的证明形式化为百万行 Lean 代码；而菲尔兹奖得主 Peter Scholze 在液体张量实验（Liquid Tensor Experiment）中，依靠 Johan Commelin 团队在未完全领会全局逻辑的情况下借助 InfoView 逐步推进，完成了对其未发表开创性成果的机器验证与化简，直接促成了陶哲轩等顶尖学者的深度采纳。 针对“手写数学是否会在未来十年消亡”的疑问，de Moura 认为人类手写证明永远不会完全消失。他将手写数学比作手工木工：尽管工业机械可以高效制造家具，工匠依然会为了传达优雅、温度与直觉而进行手工打磨。未来的数学研究与软件工程将演变为人类与 AI 协作的混合模式，人类负责界定抽象层、系统接口与真实意图，而繁重易错的推导验证工作则交由形式化验证工具完成。 Lean 目前正通过其非营利组织 Lean FRO 及 AWS 等产业资助，全力向大规模软硬件形式化验证拓展。尽管 AI 显著降低了证明合成的边际成本，但应对庞大软件状态空间的架构可扩展性，以及如何将尚未完全形式化的现实工程边界转化为严谨数学命题，仍是该技术由前沿数学迈向通用软件工业界必须直面的长期挑战。

[0:00] Leonardo de Moura: Lean is a programming language. You can write code, but you can also write proofs. You can reason about your code. [32:03] Leonardo de Moura: Anybody that went through the process of formalizing something understands the subject way better after that.

[0:00] LLMs paired with the lean proof [0:02] assistant have led to breakthroughs in [0:04] competition math and more recently the [0:07] verification of frontier math results. [0:10] Lean is a critical part of this process [0:12] because it helps validate the candidate [0:14] proofs the LLM spits out. In this [0:16] conversation, I asked the creator of [0:18] LEAN about how it works [music] and how [0:20] it will affect the future of math and [0:22] software verification. Could that be the [0:24] end of handwritten math? Here's the full [0:28] episode. [0:32] There's this famous Dysterra quote I [0:34] want to start the conversation with. [0:36] It's that, you know, program testing can [0:38] be used to show the presence of bugs, [0:41] but never to show their absence. And in [0:44] my understanding is that lean and [0:46] formalizing proofs can be used to show [0:49] the absence of bugs. And so in your [0:52] words, what is lean and how do people [0:55] use it to show bugs can't occur in [0:58] programs? [0:59] L is a programming language. You can [1:01] write code, but you can also write [1:03] proofs. You can reason about your code. [1:05] You can write state properties about [1:08] your code and prove them. LIN gives you [1:10] machine checkable proofs. You can check [1:13] your proofs and get absolute assurance [1:15] they are correct. You have uh many [1:18] checkers, independent checkers. But you [1:21] should view LIN as a platform. You can [1:24] write code. You can write properties [1:26] about your codes and you can prove them. [1:30] >> So could you give a concrete example? [1:32] Because when I think of a proof, I think [1:35] of what I learned in math. But then how [1:38] do you couple that with the software [1:40] that we write? [1:42] >> Yeah, it's a great question. It's not [1:44] that different from math proof. L is [1:46] actually very popular for math. But for [1:49] for software verification, right? uh [1:53] there are two [1:55] very different use cases. You can reason [1:58] about lin programs. LIN is a programming [2:00] language. You can write programs in ling [2:02] itself. [2:03] Then [2:05] a link program is not that different [2:06] from a definition you have in math. The [2:10] techniques are very similar. But when [2:13] you if you want to verify programs [2:15] written in a different programming [2:16] language that basically two different [2:18] approaches. [2:20] One of them they translate it's called [2:22] shallow embedding. They translate for [2:24] rust. This happens today. We have a tool [2:26] called that maps rust into ling and you [2:30] can verify the ling translation right. [2:35] uh and there's another technique called [2:36] jeep badging where you have the [2:38] semantics you you write a semantics of [2:41] the programming language of C in ling [2:44] and now you have a you have a data [2:46] structure that represents a C program [2:49] and you can state properties about it is [2:52] almost like your programs become lean [2:55] objects right that you can reason about [2:58] >> to make it really concrete to give [3:00] someone a sense of you know here's this [3:02] thing I want to prove about a simple C [3:04] program maybe like no buffer overrun or [3:08] something like that. [3:09] >> What's a step by step where we could use [3:11] lean to prove that? [3:13] >> Yeah. Yeah. Let's get array. You're [3:17] trying to access an array in C. You want [3:19] to make sure the index is in bounds. [3:22] You're not accessing elements that your [3:24] array for example has 10 elements. [3:26] You're not trying to access elements 11. [3:30] Right? [3:31] uh basically can you can write that you [3:33] can write in link that uh the value of i [3:37] at this point in your program is going [3:40] to be greater than or equal to zero and [3:42] less than 10 right you you can write [3:45] that as a mathematical statement right [3:49] uh another way to view is that if you [3:52] can express in math what you care about [3:56] your program you can verify using l [4:00] Right? That's another way to view it. [4:02] >> So I have my my C source files and then [4:05] somehow there's an equivalent lean proof [4:08] that's almost like metadata on top of [4:10] the C program. [4:11] >> Yes. [4:12] >> And that's a line by line proof and lean [4:14] will go [4:15] >> yes and check. [4:16] >> Exactly. People will build automation [4:19] for automating the process. uh they're [4:22] going to use techniques like triples [4:25] that says like uh we have a precondition [4:29] some mathematical facts that should be [4:31] true before executing that statement the [4:34] statement and what is true after right [4:37] and then we will have a lot of [4:39] automation to to process makes your [4:42] proof modeler right I mean uh complexity [4:45] is a challenge in software verification [4:48] handling the complexity is a big deal [4:51] And there were all all these frameworks [4:53] for very fine programs. They're trying [4:55] to manage the complexity make your [4:57] proofs modeler [5:00] even with AI now AI can prove things [5:02] automatically for us but they have to be [5:05] modeler to the proofs if you want them [5:07] to scale [5:08] >> and what you're saying sounds similar to [5:10] in software where you have to write it [5:12] cleanly. It needs to be easy to edit and [5:15] reason about. So it's almost like a [5:18] second software layer on top of the [5:20] software. Yes. Yes. You can view this [5:23] way. You can also flip and imagine a [5:26] future where you're writing the what you [5:30] want mathematically precisely and AI [5:33] synthesizing the codes and approve that [5:37] the code that was synthesized meets your [5:40] specification right. [5:42] >> Oh interesting. So you could start by [5:45] writing what you want to be true and [5:48] then [5:49] >> ask the AI please. AI is going to just [5:51] go and hammer at it till the lean proof [5:54] says you're good. [5:55] >> Yes. Yes. It feels like science fiction. [6:00] Six months ago I would say this is [6:01] science fiction but for example now a [6:04] colleague of mine Kin Morrison [6:07] she a few months ago she started a [6:09] project I thought was was six months ago [6:12] I would say it's not possible at all. [6:14] She said uh we have Z lib this s this [6:18] compression library written in C and she [6:21] said she creates a very complicated [6:24] prompt for AI saying I want you to [6:26] translate to ling [6:28] ensure the lan version passes the test [6:32] suite for for zib then I want you to [6:35] prove that if you compress data and you [6:39] decompress you get the original data [6:42] back it's a really strong property right [6:46] a and believe it or not they after one [6:49] week succeeded doing the whole thing and [6:52] now it's just asking to optimize the [6:54] codes [6:56] but you cannot break the proofs I mean [6:58] you have to keep still proved all the [7:01] properties you care about I mean [7:03] compressing and decompressing getting [7:05] the data back is a really important [7:08] property for a compression engine right [7:12] yeah This is enrich now. I mean, it's [7:15] surreal. I mean, [7:17] >> it's I mean, it's crazy. And I hear in [7:20] the industry a lot of people, they use a [7:24] really comprehensive test suite coupled [7:26] with AI to do some really amazing [7:30] rewrites cuz they have some more [7:33] confidence that the rewrite is accurate [7:35] and the AI can check itself. And it [7:38] sounds like a specification is even [7:42] better than a comprehensive test suite. [7:45] >> Yes. Yes. Because with well your quotes [7:48] from Dystra captures perfectly, right? [7:51] With a test suites you can show the [7:53] presence of bugs but not the absence. [7:56] It's almost like with the a good test [7:58] suite is you you may say well probably [8:00] there are no bugs here but is you you [8:05] may have a really corner case that's not [8:07] covered by your test suite but with a [8:10] proof you're covering all possible cases [8:14] a and it connects so property based [8:18] testing is really popular now people are [8:20] writing properties they want to to [8:24] ensure they are true but they are [8:26] checking with testing, right? But now we [8:29] can prove them and you say, "Look, [8:31] there's no point testing anymore. I [8:33] prove it." [8:34] >> It seems like having a a well-written [8:38] specification is a superset of a test [8:41] suite. But in terms of the human labor [8:45] required to create a a reasonable test [8:49] suite versus a reasonable specification [8:52] um you know how much more work is it to [8:55] come up with a great specification [8:58] >> varies a lot I mean uh the programs [9:04] in many it's not uncommon for someone to [9:07] start developing a piece of software and [9:09] they don't know exactly what the spec is [9:12] right but you know properties property [9:15] usually their properties are very clear [9:17] in your mind another thing that I tell [9:19] people to keep in mind that inefficient [9:22] program can give you this specification [9:25] usually writing in efficient program is [9:29] way easier than writing the super [9:31] efficient one that does has many clever [9:34] tricks you can write a very this is what [9:38] I want in a very naive way and you Ask [9:41] the AI look generate efficient version [9:45] and optimize and prove that it's [9:46] equivalent to my inefficient one. [9:51] There are many scenarios. I mean I will [9:53] not say this specifications are always [9:55] easy to come up with but properties [9:59] usually the developers have good ideas [10:01] about properties they care about. [10:04] uh as inefficient programmer is a spec [10:08] rights you can view as a specification [10:11] and the technology form of verification [10:14] complements testing rights I think your [10:18] code from extra captures perfectly [10:21] >> and I think I saw this on Twitter [10:23] because uh Jane Street was more heavily [10:26] investing in formal verification [10:28] >> yes [10:29] >> and I read their post and they talked [10:30] about this I think it was a sell for [10:33] some software that was entirely formally [10:37] verified. [10:38] >> Yes. [10:38] >> And the main drawback to why it wasn't, [10:42] you know, how much more time would it [10:44] take writing a program versus verifying [10:47] it? [10:48] >> Your example cell 4 is a great example. [10:51] This was a major milestone. It's a micro [10:54] kernel. They verified done manually was [10:57] before AI. This project was done before [10:59] AI was a big deal. [11:02] And it's a lot. The cost is super [11:04] expensive, right? At AWS, we have been [11:07] using formal verification for a decade, [11:10] but only for the super safety critical [11:13] components because it's expensive until [11:16] now, right? With AI, it changes the [11:19] game. [11:21] You have to come up with the spec. But [11:23] this is not not the most painful part. [11:26] The most painful part is to develop the [11:29] proofs manually if you have to before. [11:31] for AI and maintain the proofs as you [11:34] change the codes. Imagine your [11:37] I I've seen people complaining that oh I [11:40] I change the program right now I have a [11:43] bunch of failures in my test suite and I [11:46] have to patch go one by one imagine with [11:49] proofs you is the same process you have [11:51] to fix the proofs uh sometimes you don't [11:54] remember anymore why [11:57] the pro what what's the story behind [11:59] this proof is a lot but we AI is [12:03] extremely good at proving [12:06] uh writing formal proofs, maintaining [12:09] formal proofs. For example, yesterday I [12:13] was [12:15] changing something. I want to modify [12:18] some proofs for technical reasons and I [12:21] I didn't even know what the proofs were [12:22] about. Someone else wrote then I said, [12:24] "Look, I want you to I asked the write [12:28] these proofs without using this feature [12:30] because I'm going to change it. I don't [12:31] want to break the libraries [12:34] instantaneous. It came up with the new [12:36] proofs for me. I mean it's really good [12:39] [snorts] and this is crucial for making [12:42] formal verification mainstream because [12:45] otherwise maintaining the proofs. It was [12:48] almost like if your program took x [12:52] amount of time to do the formal [12:54] verification in the past would take 10x. [12:57] That would be normal. [13:00] But imagine if your program is changing. [13:02] That's something that's really common. [13:05] Now you have to keep maintaining the [13:07] proofs too. It's a lot of work. But AI [13:12] eliminates uh this pain for us. [13:15] >> You mentioned that lean is because I I [13:18] hear it as a proof assistant. But [13:20] >> and then you also said it's a [13:22] programming language. Yeah. [13:23] >> Is that typical for proof assistants to [13:25] be both a programming language and a [13:29] proof assistant? Some of them especially [13:31] the ones that are based on dependence [13:33] type theory [13:35] uh they are like rock and le are [13:37] programming languages and proof [13:39] assistance right I mean uh uh you can [13:42] write definitions [13:44] uh like uh when we're defining concepts [13:47] in math but some of these definitions [13:49] can be programs I mean and you have [13:52] types you have structures [13:55] is a programming language but is in that [13:58] the family of called functional [14:00] programming language I mean is a [14:02] specific kind of programming language [14:04] for people that are familiar with [14:05] programming languages like Haskell ling [14:09] is close to Haskell I mean but with the [14:11] support for proofs that that's a way to [14:14] to view ling [14:16] >> are there major use cases where people [14:17] use it as programming language but not [14:19] as a proof assistant [14:21] >> well the first big use case is link [14:23] implemented in l we have many of our [14:26] tooling is implemented in l like the the [14:29] documentation authoring system called [14:31] vers is implemented in ling. The build [14:33] system that's called lake. It's like [14:36] ling make lake is implemented in ling. [14:39] Uh at AWS we have a compiler for AI [14:43] acceler accelerators. [14:46] It's half million lines of ling and it's [14:48] using ling as a programming language. [14:50] They're proving some properties about [14:52] the program using ling. But the main [14:55] goal is choose ling use ling as a [14:57] programming language in this project. [14:59] The proofs are like a a bonus right that [15:02] you can get the proofs and find problems [15:04] in the design. [15:06] >> I think most people are familiar with [15:08] programming languages and the tool [15:10] chains they have and but um what are all [15:14] the major components that you would need [15:17] for a proof assistant? [15:19] >> This is not that different. I mean if [15:21] you're used to modern programming [15:23] language like Rust the tooling for [15:25] example lake is is our cargo right I [15:29] mean uh you're going to open v visual [15:31] studio codes same way and you're going [15:34] to get all the intellisense [15:36] one big difference is that we have [15:38] something called the info view in ling [15:41] your screens usually is going to be [15:42] split in two you have your your file on [15:47] the right hand side you have the info [15:49] view that tells you information about [15:50] your proofs, about your codes, uh is [15:56] giving you constant feedback about your [15:59] developments. That's basically the main [16:01] difference, but the tooling, VS code, [16:04] everything works the same way. I mean, [16:07] >> it seems like a programming language is [16:09] the the fundamental layer and then [16:11] there's some additional layer on top [16:12] that keeps [16:13] >> track. Good question. uh uh in L you [16:18] have definitions that are your program [16:19] but you have theorems statements like [16:22] you're going to say for example uh [16:24] factorial is always greater than or [16:27] equal to zero or something like that or [16:30] if you add two even numbers you get even [16:33] number you can write statements like [16:35] that and immediately you can write [16:39] actually a program that's the proof [16:42] but most people don't do that they go [16:44] into something called tactic modes. You [16:47] can view as a domain specific language [16:49] for writing proofs in ling. When you [16:52] write by it switches to this domain [16:54] specific language and you can you have [16:57] steps like simplify my goal [17:01] the state of my proof. You can say oh [17:04] apply this writing step apply for [17:07] example we know that x plus 0= x. You [17:10] can ask ling apply this writing and [17:13] you're going to see in the info view the [17:15] state of the proof changing you you get [17:18] immediate feedback and you get this [17:20] feeling that you said you you keep [17:23] telling applying transformations to your [17:26] proof step by step you can see what's [17:28] happening until you get no goals left [17:32] and you are done the proof's complete [17:34] and some people view this process as a [17:37] game I I have users that told You built [17:40] my favorite computer again for me. [17:43] [laughter] [17:45] >> That's funny. Is lean itself verified in [17:49] lean? [17:49] >> Lean is a massive program. You only have [17:52] to trust the kernel. The kernel is where [17:54] the proofs are checked. Lean itself is [17:57] the kind of program that because there [18:00] are so many new things we are adding. [18:02] It's not even clear what is the [18:03] specification. For example, what is the [18:07] specification of a simplifier? You you [18:09] can write general ideas but users they [18:12] want to be able to customize the [18:14] behavior. They keep asking they keep [18:16] changing the specification all the time. [18:18] I want this, I want that. No add this [18:22] knob here. So it's really hard to have a [18:25] full specification of L. But the kernel [18:27] is possible to have a specification. We [18:30] have a kernel. The kernel that comes [18:32] with ling is not verified. But there are [18:35] other kernels that you can use. One of [18:38] them is implemented by Mario Kanedo. [18:41] It's called Ling for Ling and it's [18:44] implemented in ling and he's very fine [18:46] is proving that this this kernel has [18:48] been verified with respect to the [18:50] semantics of ling. This is a cool [18:53] project but for us having multiple [18:57] kernels is the best way to ensure that [19:00] your results are correct. I mean uh some [19:03] users implemented their own kernels. We [19:05] have kernels implemented in rust uh in [19:08] different programming languages. Uh [19:10] >> and when you say kernel what's what's [19:12] the responsibility or what's the inputs [19:15] and outputs of that portion? [19:16] >> Yes. And l proof checking is type [19:20] checking. This kernels they are type [19:22] checking your programs. I mean basically [19:25] you can export your lan developments. [19:28] You got a big blob and you read this [19:31] blob and they're going to check if [19:35] when you say we have a proofing link [19:37] basically you have a thumb that has a [19:39] type and you're checking if the type of [19:41] this T matches the type that you claim [19:45] it has. For example, the example of the [19:47] even numbers. This is a typing link [19:50] saying that's uh uh the sum of two even [19:53] numbers is a even number. [19:56] You can write you can view that it is [19:58] exactly a typing link and the proof what [20:01] the kernel is checking is whether the [20:03] type of the proof matches the type you [20:06] claim this thumb has I mean and the the [20:09] console will check you do this type [20:11] checking [20:13] uh the kernels vary between [20:18] high performance kernel should it's like [20:20] 5,000 lines of code I mean the goal of [20:23] the should be something you can write [20:26] yourself. [20:27] Uh of course sometimes people put bells [20:30] and whistles like uh one thing concern [20:34] people have is like okay [20:37] but how do I know that I wrote fas [20:41] in ling how do you know that when you [20:45] exported it's really theorem it's not 2 [20:48] plus 2 equals four I mean uh and people [20:52] some external kernels they write print [20:55] printers I mean they will print the [20:57] statements that has been proven all the [20:59] dependencies [21:01] you can have all the these fancy tools [21:03] to make sure you're not being misled. [21:07] >> Lean obviously it's so powerful and I [21:10] see on social media all these amazing [21:13] results from formal verification want to [21:16] know you what are the top ones that you [21:18] think of or top examples more recently [21:21] that have impressed you that lean was [21:23] able to accomplish? Well, there are so [21:26] many I mean that I thought were was [21:28] impossible for for example getting a [21:30] gold medal in the international [21:32] mathematical olympiad. [21:35] A few years ago everybody thought was [21:37] impossible. Now everybody they use it as [21:40] a benchmark of a easy problem. They say [21:42] oh this is like a IMO problem. I mean [21:45] this is easy but it's not. I mean these [21:48] are really challenging problems. Uh the [21:51] other conjectures that people close [21:54] using ling AI with ling also impresses [21:58] me. Uh there's this unit distance [22:02] conjecture for others. First open AI [22:05] prove it using formal right was not [22:10] formal and we have a system now in ling [22:14] is a website where we call ling where we [22:16] collect challenges. [22:18] uh the same Kim Morrison saw this this [22:21] this this [22:23] proof open AI and she puts on Lo as a [22:28] challenge say okay I want to see someone [22:30] formalizing we knew it was huge to [22:33] formalize [22:34] it's serious math it depends on [22:38] and Boris Alexi from openi he did his [22:42] swim it's a one million line proof for [22:44] for for whole proofing link for this [22:46] conjecture uh We estimate I mean the the [22:50] the ground math that is needed for the [22:53] proof we knew it take months I mean for [22:56] experts to do by hands. I mean [22:59] >> uh how long did it take in that case [23:01] like the time from when the proof came [23:03] out to when the challenge was solved on [23:05] the lean? [23:06] >> I think what was one month? [23:08] >> Yeah. And after Kim was a few I think [23:12] less than two weeks after Kim puts as a [23:15] challenge only vow I took I think two [23:18] weeks to get the the or or less I mean [23:21] >> that's that's insane. [23:22] >> Yes. Yeah. Yeah. [23:24] >> We talked about verifying programs but [23:26] also there's using it just directly for [23:29] mathematics like in this case. [23:31] How popular is lean in in terms of um [23:35] when you look at the users of lean? What [23:38] percent are using it for software [23:40] engineering? What percent are using it [23:42] more for just direct math? Well, [23:45] historically lean be got popular first [23:48] with math, right? I mean know with the [23:52] beginning of the le mathematical library [23:54] in 2017 [23:56] we we had like a big project called [23:59] liquid stencil experiments. [24:01] Uh it started beginning of 2020. It was [24:06] a big deal because it was to verify a [24:09] result from a fields medalist. Per shows [24:11] it is a result he was unsure about. He [24:14] has not published it. uh uh he felt like [24:18] this was one of the most important [24:20] results in his career. He wanted to be [24:22] sure it was correct. It was done [24:25] manually. The verification [24:28] uh was a big deal because the team that [24:30] formalizes led by Yuan Kling [24:34] they not only formalized the results [24:37] without fully understanding they do not [24:39] fully understand the the proof. [24:42] uh but having this info view helped them [24:44] guides them step by step [24:47] they formalized and simplify the proof [24:50] without fully understanding the proof is [24:53] mindboggling right I mean how can you [24:55] simplify a proof from one of the [24:58] greatest living mathematicians without [25:00] fully understanding it I mean but you [25:02] you they manage to simplify it's almost [25:05] like when people do factoring coding you [25:07] start changing the codes [25:10] is faster now But the program doesn't [25:13] really know why. I mean, it felt like [25:15] that. It's like you have a gut feeling. [25:18] I mean, that's you're going the right [25:19] direction. [25:21] And this for us at the time, lots of [25:24] people got excited about link the math [25:26] community because of this project. it [25:29] like it's shown that's not about [25:31] verifying but enabling people to work [25:34] together in large numbers because you [25:36] can trust you don't need to trust [25:39] someone else's proof right they can fill [25:42] holes for you [25:44] uh this was [25:47] I mean what attracts a lots of attention [25:49] from the math community then came Terren [25:51] St. He starts using after this project. [25:54] He has really cool projects with and [25:57] without AI and he got addicted actually. [26:01] I think the first time he used it said I [26:04] don't think I'm going to do it again. [26:06] The for proof one week later he had [26:08] another project using ling and he did a [26:12] new result he had. [laughter] [26:13] >> When you say addicted you mean because [26:15] that game that like completion engine. [26:17] >> Yeah. Some people I I feel we feel like [26:20] when I talk to professors that use link [26:23] for teaching [26:25] they tell me the class is more or less [26:27] split. Some people love it, some people [26:30] don't like. But people that like to [26:33] problem solving, people that get medals [26:36] in the IMO, they love because you get [26:38] this excitement of solving. It's like a [26:42] solving millions of really hard pseudoc [26:44] problems, right? [laughter] And you can [26:47] keep solving one and it's easy to get. I [26:50] mean I'm a lean developer not a lean [26:52] user but when you're developing ling I'm [26:54] coding in ling and sometimes I have [26:56] prove things is really easy to get [26:59] addicted it gets lost proving things you [27:03] get this bus every time you prove [27:05] something [laughter] [27:07] >> you mentioned the II gold medals how is [27:11] lean used in that kind of uh I think [27:14] maybe referring to alpha proof by deep [27:16] mind or maybe something else [27:18] >> yes deep mind because they got in 2024 [27:21] was a big surprise in 2024 they got a [27:24] silver medal and now we have gold medals [27:28] from startups like a harmonic by dance [27:32] got a medal I never imagined by dance [27:36] they they they're behind tick tock right [27:40] I didn't even know they care about form [27:42] math but they have a for math team they [27:45] got medals also the approver is really [27:47] good [27:48] >> so how's it work let's say I mean [27:49] there's a series of math problems lean [27:52] is just used for verification right so I [27:56] imagine there's other components there [27:58] >> yeah there's the AI you can view it's [28:00] like uh we have go that was very popular [28:03] with AI the AI is playing the game I [28:07] told you that many people see lens again [28:11] it's the same I mean the AI is viewing [28:13] lens again they have the statements of [28:15] what you want to prove you have the buy [28:18] keyword words. Now you have a blank [28:21] fill. Make sure that you have no goals [28:23] left, right? It keeps applying steps in [28:26] this game and seeing the trans the state [28:28] of the boards, right? That's the info [28:31] view changing [28:33] and the AI they use reinforcement [28:35] learning for for for trying to get to to [28:39] no goals left. They it's a single player [28:42] game. Some people play together these [28:45] days but yeah the AI is learning to play [28:48] the game. [28:49] >> So before we were talking about that [28:51] game it kind of starts with the [28:53] specification. So in that case then the [28:56] problem is kind of the specification and [28:59] then it [29:00] >> the problem yeah you have basically for [29:01] each problem in the international [29:03] mathematical olympiad someone translates [29:05] to ling the statements. It's super [29:08] important to have the mathematical [29:10] library because you want to be able to [29:11] talk about the problems, right? For [29:13] example, the problems uses the real [29:16] numbers. You need a definition in ling [29:18] and we have it inside of math lib the [29:20] ling mathematical library. So the first [29:23] thing you have to be you have to be able [29:25] to write the problems in lane and this [29:29] now because of math li it's easy part uh [29:33] and after that you have to provide the [29:35] proofs I mean sometimes some problems [29:37] you have to come up with a definition to [29:40] some objects you have to to create that [29:43] has some property but yeah that's how it [29:46] is. I remember you said one of the first [29:50] use cases of lean was um this fields [29:53] medalist had this novel mathematics and [29:56] then we use lean to verify it but can [30:01] lean be used with LMS to generate novel [30:04] mathematics or just verify existing is a [30:08] good question I mean we don't see lots [30:11] of evidence we see now evidence it can [30:15] find novel proofs [30:17] Right? But coming up with new [30:21] mathematical concepts is still [30:24] at the limits. Right? I mean right now [30:28] in this line of all we have challenges [30:29] where the AI has to come up with the [30:31] objects [30:33] uh themselves right I mean but this is [30:36] people will keep investing in this area. [30:39] I I do not batch against AI here. I [30:42] mean, but we we right now we don't have [30:44] evidence they can come up with new math. [30:47] >> Open AAI, Enthropic, Cursor, and [30:50] Verscell all use this product to make [30:52] their lives better. And the problem it [30:55] solves is when you're building SAS or an [30:57] AI product and you want to sell to other [30:59] companies, there's all these [31:01] requirements you need to meet. There's [31:03] SSO, there's SKIM, there's arbback, [31:06] there's audit logs. These are all things [31:08] that take time to integrate but aren't [31:10] the main focus of your app. Work OS is [31:12] an API layer that lets you meet all of [31:14] these requirements in just a few lines [31:16] of code. So let's say you have a new SAS [31:19] product and you want to sell to other [31:20] companies. Work OS will solve all of [31:22] these critical feature gaps for you. You [31:25] can check them out at workos.com to [31:28] learn more and get started. And I [31:30] appreciate them for supporting my work [31:32] and sponsoring this podcast. when I see [31:34] on Twitter this, you know, major [31:36] conjecture, they made headway on it, [31:38] it's that they made headway on [31:40] confirming something [31:42] >> or or disproving. They also have uh uh [31:45] this 1 million lines, they shown the [31:47] conjecture was false. They have a proof [31:49] showing that it's false, [snorts] but [31:51] but it's a formal proof. They did not [31:55] came up with a new [31:58] theory or anything like that. They're [32:01] coming up with a proof, right? I mean, [32:04] >> at what points would you say someone [32:06] should evaluate formalizing something in [32:09] lean? [32:11] >> I I I think if if it's safe if it's [32:15] critical or if you don't understand [32:18] really well, I mean this is important [32:20] part. I don't really understand. Anybody [32:23] that went through the process of [32:25] formalizing something understands the [32:28] subject way better after that. I I [32:30] almost feel like I remember when I was [32:33] in college people would say wow after I [32:35] implement this algorithm now I [32:38] understand it much better. [32:41] The next level is that you implement the [32:43] algorithm you prove the properties you [32:46] expect [32:48] your level of understanding grows. [32:50] Right? I mean, uh, another cool thing is [32:53] that it enables you to to be much more [32:58] bold on on your optimizations [33:01] because sometimes [33:02] I I've seen that all the time people [33:05] fear implementing optimization because [33:07] they don't really understand why the the [33:08] piece of software works. They feel like [33:12] if I do that still works and is faster, [33:15] but they are not confident with proofs. [33:18] you eliminate this discomfort, right? [33:21] You you can prove it's again or the AI [33:23] can prove for you or find a counter [33:25] example. They're good at both things. [33:29] But if you were to speculate or draw [33:31] into the future, maybe 3 to 5 years from [33:34] now, if the cost of formalizing things [33:38] goes down, how does that change [33:40] software? How does that change um you [33:44] know, handwritten math? Oh, I think [33:46] we've changed dramatically, right? Uh, [33:49] we have to keep in mind the big labs, [33:52] they only start training for formal [33:54] verification lean very recently, right? [33:58] Seriously, before that was like, oh, is [34:01] in the data sets. I mean, you don't [34:03] really have the the enforcement learning [34:06] pipelines to to optimize. [34:09] The behavior we see today that is [34:11] already amazing will get way better in [34:14] the future. [34:15] uh the costs will reduce programming [34:19] languages like ling and rock will become [34:22] more mainstream because of that [34:25] uh many people are not so in the past [34:28] people say oh functional programming h I [34:31] don't like it [34:33] but if I'm not the one that's writing [34:35] most of the codes anyway [34:38] it doesn't really matter what matters [34:40] are the specification level right [34:43] doesn't really matter how the code has [34:46] been written. Yeah, I think it will [34:48] change a lot because of that. At least [34:50] that's the direction we are pushing [34:52] into. [34:53] >> What about let's say you know 10 years [34:56] from now lean is everything's going [34:58] really well with lean. Is that the could [35:02] that be the end of handwritten math or [35:05] handwritten proofs? [35:07] >> I think there will be always aspects [35:09] that is handwritten. The [35:12] some people like to make a proof look [35:17] they they want to use the proof as an [35:21] artifact. You communicate ideas to [35:23] others. I can't imagine there will [35:26] always be people polishing making them [35:29] super easy to understand for for another [35:32] human to communicate ideas to other [35:35] people. There will always be people like [35:37] that. The same way today we have people [35:40] that uh we have machines that build [35:43] furniture but people they like to to [35:47] create them by hands and polish them [35:50] make them perfect. This will always [35:53] exist but it will be a mixture. I I [35:56] would be surprised as if there's someone [35:58] that's completely [36:01] AI is not in their workflow somehow [36:05] right I mean you'll be hybrids many [36:08] hybrids some people don't like feel this [36:11] uncomfortable about this future but for [36:14] me super exciting because I view [36:17] developing software is super painful [36:19] process [36:21] and with AI it's crazy how it bring you [36:26] awareness of how many steps are just uh [36:32] repetitive [36:34] and there's no creativity you're just [36:36] patching things and AI automates removes [36:40] lots of this pain right I mean [36:44] I cannot go back to [36:47] I'm looking forward to this future you [36:49] describe [36:50] >> yeah I guess the thing that gives people [36:52] I mean I'm guessing The discomfort is [36:56] the worry that if it kept going then you [36:59] know then we need less mathematicians or [37:02] less computer scientists or something [37:04] like that. [37:06] People don't see that AI can bring more [37:08] people. Uh uh there's also the [37:10] specification. I mean some I've see [37:13] people saying oh we are going to leave [37:16] AI we'll come up with new math. But if [37:19] there's no connection to our world, [37:24] this is some alien thing that's going by [37:27] itself. You need an interface. Uh for [37:30] example, we want to build programs [37:32] because you want to accomplish [37:33] something. Uh just something whatever it [37:37] is has an specification. There will be [37:39] always humans in the loop saying this is [37:41] what we need. This is what we want. [37:44] Right? writing this interface [37:47] interacting with the AI. [37:49] The AI will have math libraries and [37:52] everything to prove things about these [37:56] these programs we are writing these [37:57] artifacts this this whatever we are [38:00] trying to build [38:03] but we have to be able to interact these [38:06] libraries we have to understand the [38:08] abstractions that are there [38:12] I I don't see humans being eliminated we [38:14] are always going to be there in the [38:16] interface [38:17] righth uh we are telling them what we [38:21] want right I mean uh specifications will [38:24] be there I can see people always writing [38:27] codes [38:29] uh even another thing a lot of people [38:32] like to write they say I love coding my [38:35] interpretation is they love to write [38:37] prototypes [38:38] I this is fun this is the fun part to [38:41] try a new idea but to transform it into [38:44] a product is never fun I can tell you [38:46] it's never fun [38:49] and I can take over these parts and [38:51] nobody really likes doing [38:54] >> outside of lean. I I know you worked on [38:56] the Z3 SMT solver [38:59] >> and that sounds like a really difficult [39:02] thing to build. So first, what is that [39:05] solver in your words? And um yeah, how [39:08] does it differ from a SAT solver? [39:10] >> Yeah, I s long is going to be yes 20 [39:15] years ago. I started history. I mean [39:17] when I joined Microsoft research [39:20] uh yeah this is a semmit to solver is [39:23] like a set solver but you have [39:24] backgrounds theories like you [snorts] [39:27] have support for arithmetic [39:29] for arrays uh these are not random [39:33] choices right this is because we use for [39:36] doing test case generation in software [39:38] for doing software verification [39:41] link fully Z3 is fully automated is a [39:44] push button although lens Z3 are called [39:47] ton provers. They are completely [39:49] different beasts. Z3 is fully automatic. [39:52] Ling is interactive. Has automation but [39:55] it's interactive. [39:58] Tree is not a programming language. It's [40:00] like you can do is more like a [40:02] constraint solver. [40:04] It turns out you can prove simple things [40:06] about it. Not you cannot do advanced [40:09] math with abstract math. you can solve [40:13] constraints with with Z3. [40:16] >> What's an example of the the inputs to [40:18] this SMT solver and what you get out [40:21] from it? [40:22] >> Oh, I I can give you one. I mean that's [40:24] even in the Z3 manual. Uh you can encode [40:28] a sudoko problem as a set of constraints [40:31] and you can ask Z3 to solve and will [40:34] give you back the answer [40:35] instantaneously. [40:37] For real applications, Z3 was used very [40:40] successfully for finding bugs in [40:42] software. Uh people would convert for [40:45] example suppose that you have a path in [40:47] your code you know that's has a security [40:51] vulnerability but you don't know which [40:53] inputs to the program allow you to [40:56] execute this path. you can convert that [40:59] into a set of constraints that you send [41:02] to Z3 and it will say unsatisfiable [41:06] which means is impossible to execute [41:08] this path and you are happy or it gives [41:11] you back an example saying look with [41:13] this inputs you're going to be able to [41:15] do it I mean and people use it for doing [41:19] software verification [41:21] uh but because the problem becomes [41:24] undecidable [41:26] at that level you have many universal [41:28] quantifiers for stating properties about [41:30] your program, your pre and post [41:33] conditions. [41:35] The server has heristics [41:38] and this was all before AI. The [41:40] heristics were handcoded and they will [41:43] always fail and for simple things people [41:46] would be very happy with the push the [41:48] fact that Z3 is push button. But when [41:51] the property is not trivial, they would [41:53] come back saying come on I know the [41:55] proof. I mean why is it we can't find it [41:58] that's why ling started I started ling [42:01] to make sure that we would have a system [42:04] that's really good for software [42:05] verification right for Z3 was successful [42:09] for finding bugs but not so much for [42:13] software for proving the absence of bugs [42:16] it was never super successful there but [42:20] len uh was born to fill this gap [42:25] >> you that undecidable but in practice in [42:27] the real world if you run it does it [42:31] typically terminate? [42:32] >> Yeah. Yeah. Great question. Uh uh Z3 [42:36] goes the whole complexity level, right? [42:38] You you have sets uh uh you have NP [42:42] complete, P space complete, XP complete. [42:46] You have the whole undecidable, right? I [42:48] mean uh surprisingly even for sets you [42:53] can write really tiny set problems that [42:56] are really hard to solve. No set solver [42:58] will solve them. But in practice, the [43:02] problems we get for hardware [43:04] verification, [43:06] uh, uh, especially if you bound [43:08] everything, you say, "Oh, I'm trying to [43:09] look for a bug in the first 10 steps, [43:13] right? Everything's bounded. You're not [43:15] trying to prove, but you're trying to [43:18] capture a class like a space of [43:22] scenarios, right? [43:24] They are very effective than there. I [43:27] mean there I I I think the lesson there [43:30] is that programs and hardware [43:33] they're not correct by esoteric reasons [43:36] right they they are correct for very [43:39] simple reasons I mean that's why these [43:41] tools are super effective they [snorts] [43:44] um yeah but when you get to undecidable [43:48] and you're trying to prove even if the [43:52] property is not trivial there I mean it [43:55] runs out of team I mean and they time [43:58] out frequently and [snorts] sometimes [44:01] the there's a here a colleague of mine [44:04] here at Amazon I mean like chooses the [44:08] name proof instability [44:11] because sometimes if you change the [44:13] problem you just flip I mean you have A [44:16] and B you write B and A where B and A [44:18] are complicated formulas you may fail to [44:21] prove and when she was just trying to [44:24] maintain things proof would break if [44:27] using this kind of technology. But with [44:29] lean, she she switches to lean and super [44:33] smooth, right? Because you're [44:35] controlling uh the proof [44:38] >> in the lean case. Why is it so much more [44:41] efficient? [44:43] >> Your proof is basically you can view the [44:45] sequence of steps for solving the [44:47] problem. [44:50] In in Z3, you can view that you have [44:51] only one proof step. solve, right? I [44:56] mean, you're saying you have options to [44:58] solve flags, but you have very you don't [45:03] you cannot influence what Z3 is going to [45:06] do. It's much harder to influence this [45:08] kind of system. [45:11] In in ling you can if you want to give a [45:13] step super detailed stepbystep proof you [45:17] can you can use proof automation like is [45:20] available in Z3 but you can also break [45:22] it down step by step and the fact you [45:26] can do that humans can do it but the [45:29] happy surprise is that AI can do it [45:32] because now you can say step by step why [45:35] something is true. the AI can convince [45:39] lean that [45:41] it can provide a proof. I mean [45:44] >> when you were working on Z3 and lean, [45:47] what was the most technically [45:49] challenging [45:51] part that you had to build for for [45:53] either project? [45:55] >> I understand how much harder ling is in [45:58] comparison of Z3 this is or of a [46:01] magnitude harder. I mean uh one explan I [46:05] I talked to many colleagues about that [46:08] why I felt like L was so much harder I I [46:12] think it's the surface the interface [46:14] with humans is way [46:17] for the tree you have defined as a [46:20] language for it's called SMT lib it's [46:24] very simple language it's not meant for [46:27] humans it's meant for tools I mean it is [46:30] uses just the back ends of many [46:31] different tools [46:33] Someone's gener some program is [46:34] generating input for Z3 and people [46:38] expect a counter example or saying it's [46:41] impossible is unsatisfiable to come up [46:43] with the counter example. The interface [46:46] is really really simple, right? You you [46:50] can view it as a command line tool that [46:52] you pass this file on this very low [46:55] level language that's super easy to [46:57] parse and you come back with yes or no. [47:02] And l you have is a programming [47:03] language. You have libraries. You have [47:06] mechanisms. You have interactivity. You [47:08] have user interface. You have LSP. You [47:10] have build system. You have G. You have [47:12] that is so vast. I mean that's [47:18] another challenging part for me as I [47:22] mentioned Z3 was a back end. [47:24] The Z3 users [47:27] are very sophisticated software [47:30] developers people that speak the same [47:32] language I speak. It's way easy easier [47:37] to talk to people that speak your the [47:39] same language with L is completely [47:42] different, right? The B the first users [47:44] are all math math people. They have [47:48] completely different backgrounds, [47:49] different expectations, different [47:52] everything and a different community [47:55] and then you have people that want to [47:57] use L as a programming language. You [48:00] have I I I'm not a programming language [48:02] person. uh my background is automated [48:05] reasoning [48:06] and yeah it's different language [48:09] different expectations [48:11] >> was there like a a singular component [48:14] that was just really technically [48:17] challenging [48:18] >> I I told you that l implemented in ling [48:21] of course it was not always like that [48:24] right I mean it had to be implemented in [48:27] something else at the beginning the [48:30] switch from origin origally was C++. [48:35] The switch from CC C++ to lean was [48:38] extremely painful. Really really uh I [48:43] remember I literally want to cry when [48:46] when I managed to compile Ling. I was [48:49] just uh Sebastian and I at the time were [48:53] building L for together [48:56] and but this was before we had a [48:58] nonprofit for Ling. I remember calling [49:01] him and I said, "Wow, man. This is [49:05] insane." [49:06] Say, "Are you not excited?" He said, he [49:08] said, "Yes, I am. I am." I mean, super [49:11] excited. [laughter] [49:13] >> What What made that switch uh hard? [49:16] >> The first thing is is imagine you're [49:20] going to implement the language in [49:21] itself. The first thing you want is to [49:23] reduce to minimize number of features as [49:26] much as possible. So you want to [49:28] implement ling using barebones [49:31] features because you're going to have to [49:33] be able to compile it with itself. [49:36] uh uh then now you have like 100,000 [49:40] lines more or less uh I don't know the [49:44] exact number but was between 100 around [49:47] 100,000 lines and you start trying [49:50] compile you fail the first you cannot [49:53] even compile the first file in the [49:55] pipeline that that more than 1,000 and [49:58] the first one fails then you fix the bug [50:00] you can compile the first one then you [50:03] can compile the second and you keep [50:06] moving and you're always finding [50:08] discrepancies between the new and the [50:11] old one. I mean and you're trying to [50:14] reconcile make things easier for the new [50:17] one. [50:18] because you want to replace the old one [50:20] and this process [50:24] is pain and l is a complicated language [50:26] because of these dependence types and so [50:28] on the proofs [50:31] for example [50:33] when you're implementing ling you you [50:35] still need some proofs there I mean [50:38] there are some basic proofs you need but [50:41] you have to construct these proofs [50:43] without no interactivity nothing bare [50:46] bones you have to provide the proof [50:47] time. It's almost like programming in [50:50] assembly. The proof uh this was also [50:53] super painful. I mean, my god. [50:56] >> Yeah. [laughter] [50:57] But it took Yeah. Many people thought we [51:01] we were going to fail. Sebastian and I [51:03] would not be able to do it. [51:05] >> 100,000 lines is a lot. Like all human [51:07] written. [51:08] >> Yes. All human written. Yeah. [51:10] >> We talked a lot about lean and I know [51:12] there's competitors to lean. What are [51:15] the pros and cons of the different proof [51:17] assistants? You know, in what scenarios [51:20] is one preferred over the others? For [51:23] instance, the first disclaimer, I'm a [51:25] completely biased person here, right? [51:28] But I can tell you what users tell me. I [51:31] mean about for example one thing the [51:33] users love is the fact as l is super [51:36] extensible because l implemented in ling [51:40] you can add extensions to imagine you're [51:43] doing your math proof in the middle of [51:45] this math proof and say oh I want this [51:47] fancy automation here you can write in [51:49] the same file or the AI can write for [51:53] you the extension for automating a proof [51:57] and it will do it I mean even the AI is [52:00] they know about the the fact L is [52:03] extensible. [52:05] If I ask the AI to isolate an issue in [52:09] ling, I give the AI a link file, it will [52:13] start writing a ling meta program, a [52:16] program about the link tunnels to [52:18] validate the conjecture it has about why [52:22] it doesn't work. It's crazy. I mean the [52:26] I keeps writing link meta extension [52:28] there. The fact that L extension is [52:31] really popular with so many people for [52:33] example there is Patrick Masur he's a [52:37] French mathematician [52:40] uh he wrote something called Labos [52:44] Labose you can he uses for teaching we [52:48] have this language for writing the [52:50] proofs but he made the language look [52:52] like English and he has the info view [52:56] now is a point and click you can click [52:58] there it gives you suggestions about the [53:00] next move that's written in structured [53:04] English like you find in a textbook. You [53:07] see the the the student has a really [53:10] good idea on how to write in formal math [53:13] proof and he did that without asking me [53:16] any questions and he all this stuff the [53:18] point and click the the new language the [53:22] new interactivity he did all by himself. [53:25] He's not a computer scientist. He he's [53:28] has a math degree and he did all this [53:30] stuff and it's for English and French. I [53:33] mean you can choose I mean you can write [53:36] the proofs in French [53:38] uh and looks a textbook proof. I mean uh [53:42] uh the people that write visualizations [53:45] right for you want to visual you're [53:47] trying to prove something about a math [53:49] object you can write extension that [53:52] visualize these objects in your info [53:55] view right [snorts] that people that [53:57] write new domain specific languages [54:00] embedded in link for different purposes [54:02] for example for protocol verification [54:05] there's a language called veil is a link [54:08] you open veil you feel like it's a [54:10] different system for protocol [54:12] verification, but it's just a link file [54:15] with these extensions for protocol [54:17] verification. The language for this [54:20] writing protocol is a very convenient [54:22] way. [54:25] These folks wrote the whole thing [54:27] without ever talking to us. They only [54:30] talked to us after they had done it said [54:33] look I want this pass of link to be [54:35] faster. That's was the only interaction [54:37] we had. uh and so interactivity is a big [54:40] deal. [54:42] Uh another big deal now is the [54:44] mathematical library uh is vast. I mean [54:48] for stating problems open conjectures [54:51] you need a library to with the concept [54:54] to even state the problem right. So le [54:57] has a massive library and a massive [55:00] community. [55:02] Uh the community also plays a big role. [55:05] people uh before AI I think now most [55:08] people ask questions about link to AI [55:10] but in the past people would go to the [55:12] lens lip channel [55:15] ask a question about ling they would get [55:16] an answer in five minutes I mean people [55:19] would say human based AI I mean people [55:22] would be writing answers instantaneously [55:25] to your problems the community played a [55:28] big role another one was [55:32] we listen to to to our users I mean uh [55:37] uh the math I mean if you talk for [55:40] example Jeremat was the first user I [55:43] mean he has math backgrounds [55:47] he he you ask him look he said look I [55:52] could ask anything any new feature I [55:55] would get back the same day I mean this [55:58] the fix the new feature the same day and [56:01] this attracts people right I mean [56:03] because you are making improvements [56:04] making sure the system does what they [56:07] once uh uh they come back for more. I [56:11] mean uh this also has a huge impact in [56:15] growing the community. when I was doing [56:17] some research there was this idea I [56:19] think you mentioned in this conversation [56:20] too there's this uh dependent type yes [56:24] >> proof assistance and then there's higher [56:26] order logic what what is that difference [56:28] there [56:29] >> at the beginning uh when I start I won't [56:32] choose high order logic because it's [56:35] much [snorts] easier to implement I mean [56:37] uh the pen types is way harder there [56:41] uh [56:43] but the math community I mean Jeremy is [56:46] the one that convinced me that I would [56:48] never be able to attract serious [56:51] mathematicians like fields medal level [56:53] math people with high order logic. [56:56] Right? His his point is like how logic [56:59] is good for concrete math but if you [57:02] want to talk about abstract objects [57:05] uh dependent type theory is way more [57:07] powerful and is beautiful is easy to [57:11] explain why is called dependent. For [57:13] example, you can have a structure in [57:15] ling when you have several fields like x [57:18] and y are natural numbers or integers. [57:20] Let's say they're integers. [57:23] You can have another field. The type of [57:25] the field is a proof that x greater than [57:28] y. The type of this field is x let's [57:32] call greater [57:34] column. You say x greater than y. The [57:37] type depends on the value of the [57:39] previous fields. That's why it's called [57:41] dependence type theory. You can have [57:43] types that depends on the values of [57:46] other parameters, other fields and so [57:49] on. But the beautiful thing about that [57:53] that's in this you have this very small [57:56] language that is so expressive [57:59] for example this fields now that's a [58:02] proof [snorts] you you have to provide a [58:04] proof you can view it as invariance I [58:07] can only build elements of this type if [58:12] I give the x and y like in other [58:14] programming languages but I have to give [58:16] a proof that the x is greater than y is [58:19] impossible ble to construct elements [58:21] without providing this evidence, right? [58:25] Uh you can do this in variance that's [58:28] you don't have to invent invariants, [58:30] right? the language just the fact you [58:32] have these dependencies you can express [58:35] uh in the functions you can have a [58:38] function for example that says takes a x [58:41] a y and a proof that's y is different [58:43] from zero right I mean it's impossible [58:47] to call the function if you do not [58:49] provide evidence that y is different [58:51] from zero this was always cool but in [58:55] the past people would say wow providing [58:57] this proofs is really annoying but with [58:59] AI Now the I can synthesize the proofs [59:02] for you. Uh and it's really cool. [59:07] >> In higher order logic though could you [59:09] express the same? [59:10] >> No no that's you cannot you don't have [59:12] the you lose the dependencies. For [59:14] example one thing that you cannot do in [59:16] high order logic. Uh in l [59:20] in serious math people you have a bunch [59:24] of structures they manipulate. you have [59:27] like something a field I mean a ring a [59:30] group [59:32] you can write a function in ling that [59:35] takes a group and he turns a new group a [59:39] new structure [59:42] you're not man you don't really care [59:44] about the elements of the structure you [59:45] are viewing the structure as a first [59:47] class citizen that's something that the [59:50] penet can do easily and in order logic [59:53] is you have to play in coding tricks is [59:56] a mess. I mean, uh, some people say, [60:00] "Oh, it works for math." None of the [60:02] mathematicians agree with this [60:04] statement. None. I mean, you talk to to [60:08] terish, [60:11] Jerem, [60:12] Kevin Buzzard, Patrick Masu, they would [60:15] say, "No, no, you have to do the pens [60:17] type theory." I mean, [60:22] that's another example for me that [60:23] listening to your users is important. If [60:25] you want to appeal to this community, [60:27] it's totally okay to say I don't care [60:30] about this community. But if you care, [60:33] listening to what they really want is [60:35] importance. [60:37] >> So when we think about the the future of [60:40] lean, I'm curious to hear your thoughts [60:42] on where you think lean is going. Um [60:46] things you're excited about in the [60:47] future. You know, what might it look [60:50] like in in a few years? [60:51] >> Yeah. Yeah. One thing uh we have this [60:55] nonprofit behind LIN since 2023. [60:59] I mean L 13 years old uh the first 10 [61:03] years was [61:05] such project right I mean only when we [61:08] got the nonprofits behind ling that it [61:11] became you can view as a product we have [61:14] a team of engineers [61:16] and we managed to do it because the [61:19] impact on math right but Sebastian and I [61:23] I mean we co-ounded this nonprofit what [61:25] we are really excited about is le as [61:28] programming language, a programming [61:29] language where you can prove things [61:31] about your programs, right? And that's a [61:34] direction we are pushing really hard, [61:36] right? Link to uh uh we are super [61:40] grateful for AWS, [61:43] Amazon, they they're making the largest [61:46] donation so far to these nonprofits [61:49] where the goal is to accelerate this [61:52] path. I mean, LIN is doing super well in [61:54] the math path, but let's make Ling as a [61:56] programming language. lings a system for [61:59] social verification, harder [62:01] verification. Let's push to the extreme. [62:04] Let's give some love to these people uh [62:07] uh to this path that's right now we do [62:10] not really have funing to push seriously [62:12] this path. That's the nonprofits, right? [62:16] Uh for me to be in a world where you can [62:20] reason about your codes uh uh is part of [62:23] my life. They I'm not writing testes [62:25] anymore. I'm writing properties and [62:29] proving them. The AI is proving most of [62:32] them for me. Uh this is direction we are [62:36] pushing hard. And one people one thing [62:39] that people don't realize is that when [62:41] you have proofs it enables optimizations [62:45] for free. You can ask the for example [62:48] today if you ask the AI to optimize you [62:50] have to inspect the code to make sure no [62:53] bugs were introduced in the process. [62:56] But [62:58] if the AI is telling you, look, I [63:00] optimize it. It still computes the same [63:02] thing. Here's the proof. [63:05] Uh this is a game changer in my points [63:09] of view. [63:10] >> Yeah, I've heard multiple people say [63:13] this decade will be the you the decade [63:16] of formal verification of software and [63:19] yeah, maybe, you know, lean will be a [63:21] huge part of that. [63:23] >> Yeah. Yeah. We we for sure we're super [63:26] excited to make it happen. I mean uh we [63:30] uh [63:32] scalability is super important, right? [63:34] Because there's a big difference between [63:37] math and and social verification. In [63:40] math the the statements are usually [63:43] really tiny or small. I mean the is an [63:47] example. I mean super small but the [63:50] proofs insanely cheap. [63:54] for socialification [63:56] is the opposite right these statements [63:58] are big I mean but the proofs are [64:01] shallow the reason why this is true is [64:04] shallow but you have to manipulate this [64:07] big objects right [64:10] >> so for someone who wants to um learn [64:14] more about formal verification or learn [64:16] more about lean do you have a top [64:19] technical book recommendation [64:21] >> in the lean websites I mean we have uh [64:25] several books there that's introduce [64:27] lean functional programming lean theorem [64:29] proving lean mathematics in lean the [64:32] mechanics of proof is great for for [64:35] educational purposes we have we have a [64:38] collection of books if [64:40] people go to lind-lang.org or they they [64:44] you'll find all these books there. [64:49] But one one thing I I tell people these [64:51] days is that learning [64:54] l using AI is super efficient. I mean [64:58] you you keep talking to AI in natural [65:01] language asking what do you want asking [65:03] it to write examples many people split [65:07] the screen in three now right we had the [65:10] link codes the info view and on the [65:13] bottom now many people now using an AI [65:15] agent there that's writing the codes and [65:19] explaining natural language what's going [65:21] on there it's a super effective way I [65:24] mean Aren style he told me when he [65:27] learned ling he he uses old version of [65:30] it was before agents he [snorts] would [65:32] have the shajp on one window and the [65:37] visual studio code in the other window [65:39] and he would copy and paste between them [65:41] and that's how he learned but now he's [65:44] even more effective with the AI agents [65:49] it's easy to pick up I mean just talk to [65:52] the agent sometimes people say how do I [65:54] that start talking to the agent. He will [65:57] help you. here will customize [66:00] uh right you can explain what you know [66:03] already right I mean what's your [66:05] backgrounds and for example if you tell [66:08] oh I know hasll it's so much easier [66:11] right you can customize the process [66:15] >> and then last question for you is you [66:17] know if you could go back to the [66:18] beginning of you know building C3 [66:21] building lean and give yourself some [66:24] advice knowing what you know now what [66:25] would you [66:27] >> [laughter] [66:28] >> No, I'll keep it a secret. I mean, I [66:31] think ignorance is a bliss. I mean, you [66:34] don't know how hard things are and when [66:36] you start the adventure, maybe I'll keep [66:39] secrets. What I would tell I think one [66:42] thing, especially before starting I I'm [66:45] super introverted [66:48] and I would tell look you should work on [66:50] your people's skills. I mean, because it [66:53] helps a lot. I mean when you have to [66:55] interact with a community with people [66:58] for me it was hard to to learn that and [67:00] and I would tell myself look it's really [67:03] important to have people's skills too. [67:07] >> Well thank you for your time today [67:08] appreciate it. [67:09] >> Thank you. [67:10] >> Hey thank you for watching this podcast. [67:12] If you liked it and you want to see the [67:13] show grow, please support with a comment [67:15] or a like. Also, if you have any [67:18] recommendations for people you want me [67:20] to bring on, please drop a comment. [67:22] guests like Barbara Liskoff, Mike [67:24] Stonereaker, Mark Brooker. These were [67:27] all people that I brought on because [67:29] someone left a comment. On another note, [67:31] aside from the podcast, I'm working on [67:33] building the ergonomic keyboard that I [67:35] wish existed. Here's a glance at the [67:37] prototype. It's a split keyboard, so [67:39] there's two sides. Um, this is in the [67:41] case, but yeah, we launched on [67:43] Kickstarter and we hit our goal within [67:45] eight hours of launching. I really [67:47] appreciate it if you were one of the [67:48] people who grabbed one of the early [67:49] units. Um, we're now working on the long [67:52] journey of building the tooling now. And [67:54] so if you still want to pick one up, [67:56] I've left the late pledges open on [67:58] Kickstarter, so you can grab one there. [68:00] I'll put a link in the description. [68:02] Thank you again for watching the podcast [68:04] and I'll see you in the next