Who Checks a Proof No Human Can Read? — Leo de Moura

Leonardo de Moura created Lean and co-created Z3. ---This episode is sponsored by Parallel. Parallel, where agents find answers: web search, extraction and deep research APIs built for AI agents. Start free with the Parallel MCP server and $5 of credits every month: https://parallel.ai/mlst?utm_source=creator&utm_medium=podcast&utm_content=MLST---Tim Scarfe talks with Leo about how Lean escaped its original audience, why dependent types and Mathlib made it useful to working mathematicians, and what happens when formal verification leaves the lab. De Moura explains the small trusted kernel and independent checkers, and gives his account of the recent Collatz incident, in which a purported proof was accepted by both Lean's official kernel and Nanoda, apparently by exploiting a different bug in each.---TIMESTAMPS:00:00:00 Cold open: the green checkmark can lie00:00:59 Cathedral or bazaar: who controls Lean's core?00:04:55 Why Lean's core stays small and protected00:08:07 The Slack purge, Brandolini's law and the Lean FRO00:11:12 The Collatz exploit: two kernels, two bugs00:16:44 More kernels, reward hacking and safety by transparency00:21:04 Sponsor: Parallel00:21:59 Kim Morrison, Claude and the zlib proof00:25:25 Can we specify complex systems?00:28:04 Specs change: proofs are cheaper to redo with AI00:31:27 From Lean 1 to Lean 400:34:57 Dependent types in plain terms00:37:25 Lean 4's extensibility and Mathlib's growth00:41:44 Mathlib as infrastructure: Formal Frontiers00:44:15 Creativity, abstraction and nut-sniping00:48:46 Breadcrumbs, not learning: what AI agents lack00:53:03 Competence without comprehension, and verified guardrails00:56:21 Is the human still the author?01:01:44 AlphaProof, LLMs and why certificates still matter01:06:38 What's next for Lean, and its legacy01:11:42 How to start learning Lean---REFERENCES:tool:[00:00:48] Leanhttps://lean-lang.org/[00:01:24] Mathlibhttps://github.com/leanprover-community/mathlib4[00:12:09] nanoda_libhttps://github.com/ammkrn/nanoda_lib[00:12:19] CollatzLeanhttps://github.com/xrchz/CollatzLean/blob/a79357462a33d2a6babd4cf6c8d8bcd25425d653/README.md[00:13:06] Lean issue 14576https://github.com/leanprover/lean4/issues/14576[00:13:21] Lean pull request 14577https://github.com/leanprover/lean4/pull/14577[00:13:45] nanoda_lib pull request 22https://github.com/ammkrn/nanoda_lib/pull/22[00:15:33] Lean comparatorhttps://github.com/leanprover/comparator[00:18:02] Lean4Leanhttps://github.com/digama0/lean4lean[00:19:50] ARC-AGI-3https://arcprize.org/arc-agi/3[00:21:59] lean-ziphttps://github.com/kim-em/lean-zip[00:29:45] CompCerthttps://compcert.org/[00:29:45] seL4https://www.sel4.org/[00:30:23] Z3https://github.com/Z3Prover/z3[00:38:10] Veilhttps://github.com/verse-lab/veil[00:38:10] Velvethttps://github.com/verse-lab/velvetorganization:[00:00:52] Lean FROhttps://lean-lang.org/fro/[00:42:39] Mathlib Initiativehttps://mathlib-initiative.org/about/person:[00:05:11] Ilya Sergeyhttps://ilyasergey.net/[00:10:31] Joachim Breitnerhttps://www.joachim-breitner.de/[00:32:58] Adam Chlipalahttps://adam.chlipala.net/[00:38:42] Kevin Buzzardhttps://www.ma.imperial.ac.uk/~buzzard/[01:10:16] Terence Taohttps://terrytao.wordpress.com/book:[00:08:19] The Proof in the Codehttps://us.macmillan.com/books/9780374620059/theproofinthecode/other:[00:10:05] Brandolini's lawhttps://en.wikipedia.org/wiki/Brandolini%27s_law[00:45:33] A new result on unit distanceshttps://openai.com/index/model-disproves-discrete-geometry-conjecture/[01:01:08] Fermat's Last Theorem formalisationhttps://imperialcollegelondon.github.io/FLT/paper:[00:34:36] The Lean 4 theorem prover and programming languagehttps://doi.org/10.1007/978-3-030-79876-5_37---RESCRIPT:https://app.rescript.info/share/7d3d4a0059443236a01f6c9acbf4db58https://app.rescript.info/api/public/sessions/b007264c0ce89047/pdf

• 0:01Speaker 00

  This episode is brought to you by Michelob Ultra. Good times mean competitions between you and your friends. Like seeing who can throw some pigskin the farthest or rush the field the fastest. Winner gets an ultra. Because it's not just a superior like beer. It's also giving fans superior access to their favorite sporting events. Superior is worth playing for. Visit michelobultra.com/superioraccess to enter. Enjoy responsibly. Copyright 2026 Anheuser Busch InBev Michelob Ultra Beer, St. Louis, Missouri.

• 0:30Speaker 01

  Are your ad campaigns lighting up the dashboard? But not the pipeline? That's bullspend and marketers are calling it out in dashboard confessions.

• 0:39Speaker 02

  My boss asked for results, so I opened my dashboard for the only positive sounding metric I had. Impressions.

• 0:47Speaker 01

  Cut the bullspend. See revenue, not just reach. LinkedIn delivers the highest return on ad spend of major ad networks. Advertise on LinkedIn. Spend $250 on your first campaign and get a $250 credit. Go to LinkedIn.com/campaign. Terms and conditions apply.

• 1:00Speaker 03

  This proof, I think, was a disproof the Colossus conjecture was submitted with a link proof. And the claim is it's accepted by the official kernel that comes with link. Wow, I mean, this is horrible. We strongly believe was built by AI exploits one bug in the official kernel and this completely different bug in another. We don't have patience for doing this kind of low level implementation, but AI has the patience for doing that. I think this is going to be a game changer, going to better models. They keep doing more amazing things, but they keep doing stupid things at the same time. Boris Alexey submits a proof to is 1.2 million lines of link, the formal proof.

• 1:44Speaker 03

  Nobody wants to check the proof line by line. I'm Lyudmira. I'm the creator of Lean, chief architect and co-founder of the Lean Fro, a nonprofit behind Lean and also senior principal scientist at AWS.

• 1:59Speaker 04

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

• 2:41Speaker 03

  Okay, actually, this is a great question. This is a great question.

• 2:46Speaker 03

  Now, I don't control the core system anymore. I mean, we have the Fro, there's a nonprofit. We have 20 people there. Each one of them are owning. I like, I like this model, the developers in the core, they own parts of the system. It's their responsibility. They have ownership. If they're going to take external pull requests or not, they are the decision makers. But for the first 10 years, basically, I own a bunch of the system. Sebastian Ude, my colleague and friends that we built Lean for together, he own other parts of the system.

• 3:30Speaker 03

  But we believe, I strongly believe in the cathedral model for open source. Cathedral is like, there's a central entity that decides what goes into the code base or not. This is bazaar where it's more open people, everybody can contribute. And there was a lot of tension with the community, the Lean community. Many people want sometimes to contribute to the core. Contributing to a library is different from contributing to the core system. The library, many cases, suppose a library for binary trees is self-contained, right?

• 4:11Speaker 03

  The changes you make there, you can own that without impacting the rest of the system. But the core system, all the pieces are interconnected, they depend on each other. Another thing like a binary tree library, maybe missing some functions, maybe missing some terms about the dysfunction, but it's still useful. But a system full of holes is not very useful, right? I mean, if there are many pieces missing, many crashes, it's a more interconnected system. That's why I always insisted for the cathedral model for developing the core and creates

• 4:56Speaker 03

  tensions. But one, one cool thing about that, that's amazing extensible to enable people to add their own extensions without changing the core. And this became really popular with the community. I mean, many people implement should they extensions to Lean without coordinating. They implement, it's actually similar to the example you gave. They implement domain-specific languages that hide the complexity of focus on a domain-specific language for a specific domain, like distributed protocols. You can specify distributed protocols, you have a language that's optimized for that,

• 5:38Speaker 03

  hides all the complexity and this can be done without even talking to us. Sometimes they demo things to me, they never match me before they implemented this beautiful extension, right? Yeah, I think it's great. It was also a nice side effect.

• 5:55Speaker 04

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

• 6:10Speaker 03

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

• 6:52Speaker 04

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

• 7:33Speaker 03

  Yeah, there is that. I mean, there's also people adding something that's half bacon. They, it's like a lot of people like to have fun implementing software. Software is, I like to say, actually, is one of my academic brothers. He says, software is only fun if the software doesn't have to work. If it has to work, the fun disappears very quickly. And first issue, bugs, like you mentioned, people introducing bugs. Second issue, someone submits a feature that's not fully implemented, that many holes, it looks like it works, but it doesn't. Third thing, people may lock the design.

• 8:17Speaker 03

  They add a feature, it's complete, it's correct, but put constraints on how we can optimize the system or, and now we have this feature, it may become popular and prevents us from doing other things that are more important because it's there, people use it, we can easily remove it and we're stuck with that. Another issue, it's super important to prioritize the development, going chaotic, implementing random features and this happens if you start merging random PRs. It's really bad. It doesn't really scale.

• 8:56Speaker 03

  I think prioritization is super important and this model where you keep merging random PRs does not work. This is a strong belief I have.

• 9:07Speaker 04

  So you're a depth-first search kind of guy. And when you build something successful that involves lots of other people, you have to become more like breadth-first search. And because there are so many things that are coming in every single day. And I remember there was a bit in Kevin's book where he said, at some point, you just kicked a load of people off the Slack channel and you said, I just need to, I just need to focus now because it was getting ridiculous.

• 9:28Speaker 03

  Yes, oh, yes. Yeah, I forgot about this story of the kicking. Yeah, because at the point, at that point, wow, I really dislike people that keep throwing ideas. I mean, they don't even, they're having fun. I mean, it's different. I mean, for me, 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.

• 10:12Speaker 03

  You throw an idea, you didn't spend five minutes thinking about it. Then I find a hole, I send back to you. Then you polish a little bit, send back. Now it takes 10 minutes to find the hole, the next hole. It keeps taking exponentially longer to find the holes on the half-baked idea.

• 10:33Speaker 03

  For the person coming up with them, it's fun, I mean, but it's not fun. From the receiver, right? You have to do your work now, you spend time telling people why this is not a good idea, why it's not the time to do it. Yeah, there was a point, yes, I kicked out, I mean, stays only the core team that was really contributing to the projects. Only people that were writing useful codes to the projects stayed.

• 11:03Speaker 04

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

• 11:12Speaker 03

  Well, fortunately, now we have the throw, right, the link throw. I have many colleagues, many people that helped me. My life is actually better now. I mean, I have, for example, we had a serious bug this week. Johan Breitner, he took care. It's not just the bug, you have to take care of the community, explain to the community, communicate. He did all that. In the past, for me, would be a nightmare, you have to do so many people, the amount of the noise.

• 11:51Speaker 03

  Johan did that and we have many other people at the link throw that help coordinating the community,

• 12:02Speaker 03

  communicating the roadmap. For me, it's much easier now. Without the throw, we will not be able to run the projects now.

• 12:12Speaker 04

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

• 12:15Speaker 03

  Yes.

• 12:16Speaker 04

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

• 12:19Speaker 03

  Yeah, yeah, yeah. Basically, Ling is, we have the notion of a small trust's kernel. Ling is massive, has zillions of bugs, right? But to trust our results in Ling, only to trust the kernel that's much smaller, right? And, and we also have external kernels, right?

• 12:50Speaker 03

  The sequence of events, I mean, Johan did all the jigging, I mean, I'm glad he did. The sequence of events was like, one week ago, or 10 days ago, a bug was reported in one of the main external checkers. We have many kernels.

• 13:09Speaker 03

  One of the main ones, it's called Nanoda, is implemented in breast. This bug was fixed immediately by the Nanoda developer. And a few days later,

• 13:24Speaker 03

  this proof, the colat conjecture, this proof, I think it was a disproof, the colat conjecture was submitted with a link proof. And the claim is, it's accepted by the official kernel that comes with Ling and by the main external kernel, Nanoda, right? Would be, yeah, wow, I mean, this is horrible, right?

• 13:49Speaker 03

  Then the first reaction we had is that Nanoda was not accepting the proof. Then Johan said, okay, these guys are exaggerating, Nanoda does not accept. But then he said, oh, Nanoda from 10 days ago does not, was accepting the proof from. And then actually, the exploit, and we strongly believe it was built by AI, exploits one bug in the official kernel and this completely different bug in Nanoda. I fixed the bug in the official kernel and I found strange the example. Because there was a bunch of weird terms to create a hash collision that was completely irrelevant.

• 14:35Speaker 03

  I said, why did they put this stuff there? It's to pass Nanoda, I mean, to exploit the bug in Nanoda.

• 14:45Speaker 03

  Then Johan asked whether the LLM looked, they asked the LLM to look at the PR that was submitted to Nanoda. They said, the bug reporters said that was a coincidence, but they could not discuss the possibility the LLM by itself. Look at the Nanoda repository, saw the PR and crafted this exploit. Yeah, this, we have to, before coming here, I was talking to Johan and Sebastian on how to improve,

• 15:27Speaker 03

  what we can do to improve, to make it even more secure, because this is going to keep happening. People, AIs are really good exploiting and soundness, bugs in the kernels. We were from ideas like, oh, we should have bounce on people, for people building kernels that are bulletproof, they get some cash if their kernel cannot be attacked for more than X months. Or another idea is to simplify the kernel, to make it simpler to verify. Another thing is to support, Mario Carneiro is working on that. Try to prove the kernel is correct.

• 16:10Speaker 03

  Trying to assist him or to accelerate the development of his proof, I mean. But yeah, but coming here, I was talking to Johan about how to improve the situation for avoiding this kind of thing from happening again. But there are some concrete steps, like one concrete step that Rob did. We have a tool called comparator that's for, that's basically, comparator exports the proof, because some people can use meta programming in the extensibility features we discussed as to inject false proofs. You can even call C function corrupt the memory, for example.

• 16:55Speaker 03

  But you can, we have comparator that will export the proofs, we check them in a sandbox. And one lesson is to, for comparator, always to download the latest version of Nanoda. Right, and so we don't have to manually upgrade Nanoda. If someone submits a bug fix to Nanoda, it will be used immediately by comparator. And comparator have rejected, right, if it had done that. And we're doing that, yeah, but we have lots to do. We want to prove more things about the kernel, about the code generator. That's another place we have to improve.

• 17:36Speaker 03

  Yeah, but this was, I could not imagine the situation without the throw to help us.

• 17:43Speaker 04

  Yeah, and I wonder whether it's a similar thing, but there was an incident where the, you know, GPT-6, let's say, hacked hugging face recently. And the models are becoming reward hacky, reward seeking. And I don't know whether you think, I mean, maybe you implied this was a similar situation, but, you know, there was, there was a green check, basically, so it looked like this proof was valid. And sometimes these proofs are quite inscrutable, they're difficult for humans to read. So in principle, the LLM could have done reward hacking and rather than kind of doing the spirit of what we wanted to do, it didn't. And what OpenAI did was they changed their guardrails. So that, you know, when, when a model generates some code, they don't just look at the code in isolation.

• 18:25Speaker 04

  They look at the entire trajectory, the reasoning trace, why did this code come to be? So they're trying to sort of like disentangle the intention behind this thing versus the intention of the developer that did the prompt. So do you see a similar thing here that we might, we might need to have almost separate adversarial systems kind of evaluating what's happened?

• 18:44Speaker 03

  Well, having multiple kernels is a way to accomplish that, right? If you have independent kernels implemented by different people using different programming languages, it strengthens the situation, right? The fact that we have the official kernel in Nanoda, we want to have more. I mean, the one from Mario, this is called Ling for Ling, is, is going to be special because he's proving it should be correct. So it would be not just another kernel, but a kernel that has been proved correct. That will be a big deal when it arrives. I mean, we can use Ling for Ling today, but it's not fully proved. It proved many parts, not the parts that had the exploits.

• 19:28Speaker 03

  If he had proved it, he would have found the bug before it was exploited. So having multiple kernels, having some of them prove it's correct, makes the story really bulletproof. Then there is the next level, you may ask, okay, you proved the kernel correct, but you're compiling with some compiler. The compiler maybe has a bug, right? And you prove it's correct, but what's running is not what you prove it, right? Then the next step, let's prove the compiler correct. Then you may say, oh, the hardware may have a bug, right? Say, oh, well, okay, let's ask Intel to publish formal specs.

• 20:10Speaker 03

  That's how they are saying this is the official formal specification for the microprocessors, same for AMD and so on.

• 20:22Speaker 03

  The movement here is always reducing what you have to trust, right? And this is going to be important, right? If for one day we want to have massive results, that's we don't have to spend time checking manually for exploits. It's really important that we can fully trust these mechanical proofs, right?

• 20:45Speaker 04

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

• 20:50Speaker 03

  Yeah.

• 20:50Speaker 04

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

• 21:24Speaker 03

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

• 22:05Speaker 04

  Speaking of checking where your answers come from, today's episode is sponsored by Parallel, where agents find answers. Most engineers today, they closely follow new model releases, but they don't pay attention to their agent's most important tool, web search. Parallel develops enterprise-grade infrastructure for agents to retrieve high-quality context from the web. Their core products are a suite of APIs for retrieving high-quality information from the web with Pareto optimal quality, cost and speed. So whether you're working on voice agents that need 200 millisecond latency, chatbots that balance speed, depth and quality,

• 22:45Speaker 04

  or long horizon agents to do thorough overnight research for you, Parallel is the single platform for all of your agentic research. Get started for free at parallel.ai forward slash MLST.

• 23:00Speaker 04

  Apparently, Kim Morrison used a Claude agent to produce a lean implementation of the compression format Z Lib and and prove some specific properties of it. So what exactly did they manage to prove?

• 23:12Speaker 03

  Oh, yeah, yeah, this, when Kim started working on this project, I thought, wow, this, it felt hopeless. No way, I, I, I thought was at the beginning of the year, right? To me, I, I thought AI is not good enough for that. I mean, we'll not be able to succeed at that. But they, I managed to translate from C to lean the code. Then managed to keep fixing the lean implementation to its passage that has suites that comes with the C version. And then it proved that for any compression level, for any data, if you compress the data and then decompress, you get the original data back.

• 23:56Speaker 03

  This felt completely out of reach for AI at the beginning of the year, but AI managed to do it and didn't stop there. Kim asked them to optimize the code, especially for this kind of program. Lean right now is not the kind of language for array manipulation. Lean has been optimized for programs that are manipulating trees because, I mean, you're manipulating terms, right? You're manipulating trees internally, you have the syntax trees, the expression trees. Lean is really good for this kind of program, but not for arrays. In my mind, this will never be competitive, right?

• 24:41Speaker 03

  But turns out that Kim asked the AI to keep trying really, you can go wild, keep optimizing the code. You, you have to keep proving the the property, you cannot break the property. And it's bits, our implementation in Rust. And Rust is a really efficient language for array manipulation. Then for us, it's really unexpected, right? I mean, first the sign, imagine now if we improve our way manipulation for lean, how far we can go.

• 25:22Speaker 03

  There's so many possibilities, right? We can ask now, they, I suppose that we give the semantics of x86, the microprocessor, the the assembly. You can ask, I think, very soon, we're going to be able to ask the AI to prove writing assembly, exploiting all the dispensing instructions, but proving, you, you have to prove the property, right? We don't have patience for doing this kind of low-level implementation, but AI has the patience for doing that. I think this is going to be a game changer, right? Last year, I thought this would be impossible, but now is in reach. I mean, this experiment shows there is a path there.

• 26:07Speaker 03

  These AIs will keep, keep getting better and better at this kinds of tasks because there's a strong signal telling them you're on the right path, right? You have to still prove the theorem, right? You, you, you can't cheat. Yeah, I think this case the limits.

• 26:25Speaker 04

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

• 27:05Speaker 04

  So I suppose, do we have a chicken and egg problem that when we're working with very complex systems, we can't really yet specify, or if we can, we can only specify parts of it?

• 27:17Speaker 03

  Yeah, yeah, yeah, I, I agree that it's very common sometimes. You know, some properties the system should have, but not all of them. You're still engaging with the users about which properties the system should have. Believe it or not, this happens with lean all the time. The kernel is clear what the kernel should do, but the whole system, there are many components. I mean, there are many, for example, the statics I mentioned, the moves, what a move should do. We implement something, the users is really common for the users saying, oh, no, no, I want more, I want less. I know it's doing too much, I, I want more control, I want this flag, I want to have a way to to control where the proof is going more.

• 28:03Speaker 03

  It's a back and forth, the spec there is not really clear, right? Yeah, I think you're right, in many cases, the spec is not clear. But it's important to talk, to start documenting the properties, you know, they should hold, talk to your customers about them.

• 28:24Speaker 03

  And another thing to keep in mind that a, a, a high-level program in a very high-level programming language like lean, without any optimization, can be viewed as as a specification, right? You can say, look, this is what I want to compute. It's not super efficient, but this is what I want to compute. And you can ask the AI optimize this function for me. I implement the simplest possible, right? Idea, right? Without any fancy data structures, clever algorithms, it does what I want. Now it's, it's AI's job to optimize it.

• 29:04Speaker 04

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

• 29:37Speaker 03

  Oh, yeah, for sure. I mean, when you updated specifications, the code was generated, they've been validated, the proofs that the code meets specification need to be invalidated. In the past, form verification, this was a big deal, right? People would say, oh, my gosh, I mean, I spent all this time proving the implementation is correct. Now these folks want to add this fancy optimization. Now I have to redo many of these proofs. It, it, it, it's not rocket science, but it's a lot of work. But turns out the AI is really good at updating these artifacts for us, right? But before AI, this was a really big deal, right?

• 30:21Speaker 03

  Especially for the safety critical systems where form verification was used in the past. They were for application domains where the spec was very clear, like cryptography, the spec is very clear, right? They find a micro kernel, people put lots of thoughts in the micro kernel before they even started verifying the projects. All these famous verification projects like Comsol, Cell 4, people put a lot of thought on the spec, right? They, in some cases, they had to update along the way and what's painful is how to do it. But now, because we have AI to update the proofs, the artifacts, it's way less painful, right?

• 31:06Speaker 03

  I think there's still.

• 31:09Speaker 03

  I can see the near future, right? AI is too expensive, right? People would say, wow, I'm updating this spec. Now I have to waste zillions of tokens updating everything, right?

• 31:23Speaker 04

  It is really exciting though, because if I remember correctly, Kevin said in his book that I think Z3, that actually solved an incredible number of bugs in Windows 7 before it even got released. So it was life-saving. But we, you know, most of the time, this kind of technology is used for very high-stakes software. But do you agree though, in principle, that in the future, just everyone will be doing this, just every developer will be, you know, building this kind of software?

• 31:50Speaker 03

  They may not know they're using form verification, but will be there in their pipeline, right? They are going to be writing properties and the properties are going to be verified. Their code is going to be updated. I mean, there will be proofs showing the code still computes the same thing. People submit PRs, they're going to get proofs whether the PR is violating some of the properties in their test suite or not, statically. Yes, I think even if they don't know they're using formal verification, it will be there.

• 32:27Speaker 04

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

• 32:39Speaker 03

  Oh, wow. Okay. Lean, the first Lean is even called 0.1. I learned by doing it. I read many papers about the penance type theory. I used some of the other systems.

• 32:58Speaker 03

  But I always feel you get a different perspective when you implement something. There are so many nuances, details that you only now say, oh, wow, this is really important, I mean. And Lean 1, I also tried to make it very small, the code was too small. And it was unusable, maybe only Jeremy, I think Flores, one of his students also used Lean 1. But they were heroes. It was a horrible system. I mean, it was more like a learning and artifacts are used to learn the penance type theory. Then Lean 2 was for real, but

• 33:43Speaker 03

  and I think Lean 2 had like maybe between 50 and 100 users, very small.

• 33:53Speaker 03

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

• 34:34Speaker 03

  And then MATLAB started, things started growing very rapidly. And it was clear that Lean 3 had limitations, I mean, in terms of scalability. The system was the tactics you could extend yourself, but that was it. Some people managed to do linters, the MATLAB community figured out how to hack Lean, to write linters in Lean. But we want to make it fully extensible. And in 2018, Sebastian Oerig and I said, we're going to implement the whole thing.

• 35:09Speaker 03

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

• 35:53Speaker 03

  But it was really exciting to get there.

• 35:57Speaker 04

  And I don't think we sufficiently explained dependent type theory, so maybe you can do that. But there was this relationship between the expressibility space of the problem descriptions and how sophisticated the kernel needs to be. And I think early on, you were quite bullish about you want the kernel to be kind of like quite small and optimized and you had to admit more complexity there.

• 36:18Speaker 03

  Yes, yes, but this was in the design phase. I mean, it was before even Lean 0.1 started. When I started implementing Lean 0.1, it was the penance type theory, right? It was always, all inversions are based on the penance type theory. But it was more like when we were designing, deciding what to implement, was at the design level, this discussion about the penance type theory. To explain to the audience what the penance type theory is, I think one example is to say, you can have, in the penance type theory, you can have a structure like that has two fields, x and y. They are supposed integers.

• 36:58Speaker 03

  And you can have a third field that says the type of this field is x is greater than y. It's a proof. You have to fill this field with a proof that's evidence that x is greater than y. You can view it as an invariant. It's called dependence because of the type of something can depend on the value of something else. You're depending on the type of this third field depends on the value of x and y. Right? That's why it's called dependence. You can simulate invariance. In functions, you can have like a function that takes x and y and the third argument, y should not be zero.

• 37:41Speaker 03

  You have to call this function, you have to provide evidence that y is not zero. It's almost like a precondition. That's the beauty of the penance type theory, a simple idea. You can capture preconditions, you can simulate postconditions, you can have invariance. You don't need to invent all these concepts. Everything is really minimalistic. But it complicates your type theory because you have dependencies, you have to manage them.

• 38:14Speaker 03

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

• 38:17Speaker 04

  Yes, so the kernel had to be significantly more sophisticated to support that. What can you do in Lean 4 that you can't do in Lean 3?

• 38:26Speaker 03

  Ah, Lean 4 is fully extensible, right? I mean, everything's implemented in Lean. You have access to all the internal data. When you're writing your Lean declarations, you can in the same file, you can write code that accesses the internal representations of everything. Many, the first AI research labs, groups,

• 38:51Speaker 03

  for them was a big deal. They could extract training data, right, from the internals of Lean. They could write Lean code that extracts information about all the proofs that are in MATLAB. They could manipulate these objects. This was a big deal for them. All these extensions I told you about, like tools like Velvet, Veil, they are all using this extensibility we have in Lean.

• 39:21Speaker 04

  And I saw from your slides you presented this week. So I think that we've now reached the inflection point where there is as much Lean 4 code in MATLAB as there was Lean 3 code.

• 39:32Speaker 03

  Oh, yeah, way more, way more.

• 39:34Speaker 04

  Way more, yeah.

• 39:35Speaker 03

  Uh, MATLAB 3 stopped at 1.1 million. In MATLAB 4, we have 2.4 million.

• 39:43Speaker 04

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

• 40:12Speaker 03

  No, that's going to keep growing forever, yes. I mean, there will be always new math being invented, new structures defined, new mathematical objects, there will be always new things. There's a debate whether everything should be in MATLAB or not.

• 40:32Speaker 03

  At the beginning, for sure, at the beginning, it was amazing to have everything in a single library. Because the library, you have many concepts in mathematics. For example, you have rings. There's only one ring in the Lean mathematical library. The library's coherence, I mean, it's really common in other programming languages to have many implementations of the same thing. And things are incompatible. If you want to prove things about your code, it's important to have this uniform view. And MATLAB also, they also are another great thing they decided. We will always shoot for the more general, the most general description of something that was also a great.

• 41:16Speaker 03

  But there are limitations about the size, right?

• 41:21Speaker 03

  MATLAB is two point four million lines. Imagine if it's fifty million lines. Now it's starting to get to the size of the Linux kernel. Right, I mean, or big projects we have that's like Firefox. Size of this, these projects have teams of people just maintaining the build system. I mean, everything is more complicated. Sometimes they have their own specialized vision control system to handle the complexity. Now there's a lot of discussion on how to get the mathematical library. Maybe MATLAB is going to be a collection of libraries.

• 42:01Speaker 03

  You have the main ones like the standard library for math and many satellite ones. All of them maintainers, all of them coherence, but with different leaderships. I mean, you don't have the same group of maintainers for each one of them. All these discussions are happening. I think they're healthy. Yeah, but people predict if you want to do, if you have to have all mainstream math, the library has to be one hundred million lines. I mean, if you want to be able to formalize a laboratory research level mathematics papers, the library has to be one hundred million. Some people in the community have these estimates.

• 42:45Speaker 04

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

• 43:25Speaker 03

  Yes, yes, yes, both things have, it's exactly like software. You should, you're thinking the right way. There are things that people thought a lot and crystal clear how it should be. And there are things that are in flux, right? But one cool property we want to have, and there's a project now from the MATLAB initiative called Formal Frontiers. They want humans plus AI to formalize, to fill all the gaps in MATLAB and enable any research level math paper to be, people to be able to formalize the paper. To put in perspective for software developers, this is the equivalence like you want to develop some piece of software.

• 44:10Speaker 03

  And today people use hundreds of crates, right? If they're developing Rust. But imagine that you, half of these crates were missing. And you would say, oh my gosh, now I have to spend time building the infrastructure for building my application. It feels like, I say, like something that would take one month, takes years because you have to build all the infrastructure. Same thing for math. If you're trying to formalize a paper, people in the community will tell you it's doable or not. Because if there are so many components missing, it's going to be a gigantic task, right? But if all the components are there, you only need to formalize your paper,

• 44:54Speaker 03

  your contribution, not the background material. It's like if you have all crates there, grades, it's easy, I can focus only on my application. I don't need to build a JSON library. I don't need to build a bit trees. I don't need, you get it, right? It's what I mean, but it's exactly like software.

• 45:15Speaker 04

  I've got, I've got a theory that creativity is about deep understanding. So when, when, when you understand something deeply, you can kind of extend that lineage. And there's a really interesting thought that sometimes, you know, language models, they, they can acquire all of these abstractions. I love using the example of linguistics. So they can skin sentences like an onion, even ones that we can't skin. And they explain it to you using concepts from PhD linguistics textbooks. And it's a similar thing across the board. So, so they, they, they know about rings. And, but, but I have a theory that even though they have the abstraction,

• 45:56Speaker 04

  in a sense, they don't understand it because, you know, the path that led to rings, you know, it's like a big evolutionary tree. Understanding is about knowing the difference between what's possible and what's not possible, counterfactuals, how could it be different and so on. So if you start with something that is very, very distilled and you don't understand how it came about, then it's difficult to be creative. So what we see with language models is they, they start quite low down the abstraction mountain. So, so these, these are still a form of understanding, but they're, they're deep, concrete understandings. They're still quite fractured, they're not very factored, but they have more degrees of freedom. So when you look at this proof from the, the new GPT model disproving this, you know,

• 46:38Speaker 04

  unit distance problem, what you see is insane verbocity. It's just kind of going around, it's doing quite surprising things. So isn't it interesting that from a creativity point of view, what we think is most important, so these really deep factored abstractions, might not actually be how the AI models are creative?

• 46:58Speaker 03

  Really hard to tell. I mean, I, I keep thinking about this. They surprise me in both directions, sometimes doing amazing things. We had a bug, not, not in the trust, this is a simple bug in, in, in the top level that's not, doesn't need to be trusted. But nonetheless, it's a very complex piece of software there. I think very few developers, lean developers understand this part. They, I understood perfectly, perfect, the explanation was spot on. I was blown, I said, how come they understand so much about the internal implementation? Right, I was blown away.

• 47:38Speaker 03

  But on the other hand, sometimes it makes idiotic mistakes. I mean, and it's not, it, it, I, I, I don't see the behavior changing. I keep going to better models, they keep doing more amazing things, but they keep doing stupid things at the same time. But we do stupid things, sure, right? I mean, maybe they are. Today I feel like they are really good for not, tasks that we call not sniping. Like, if you have a hole in a, you have a statement, you want to prove, if you don't need to create a new theory, you are just combining the pieces that exist.

• 48:23Speaker 03

  They're a bit, feels like they're unbeatable by humans. They are way better. You ask to implement micro optimizations to a piece of code also, they're amazing doing that. But if you ask them to come up with a new technique for implementing something, they fail miserably. I, I feel like maybe, I'm not a machine learning expert, maybe you tell me. One conjecture I have is like, these things are like, you turn on, they are like waking, waking up, I mean, with no, only if the training, you show them a problem and they go for it.

• 49:05Speaker 03

  I mean, they read all the literature during the training, during the, the training, they saw all the literature. They have a bias towards exist solutions that people use. If you can solve this problem using a collection of tricks from the literature, they will do it, they will crush it. But if you need a new trick, it feels like they fall short. Of course, in the future, you may have AI agents that keep updating their weights and learning. You tell me, I mean, what, what, does this match your understanding? I'm not an expert.

• 49:46Speaker 04

  Really, I'm, I'm as excited as you are, but there is this weird thing that they have lots and lots of intelligence, but they still clearly need to be directed. So the, the best case scenario is you're solving a specific problem and you can hill climb towards it, but you still need to give it a kind of aspect ratio. I use the analogy of shining a flashlight into embedding space. So the, the flashlight has a beam. So as an expert, what you're doing is, is you're saying, okay, well, well, this perspective is quite interesting, you know, here are some sample seeded solutions. Here are some tricks that you can use and here, here is a clear optimization objective. And in that case, it's miraculous. But there's still some human taste and expertise required. But the, the thing that seems to be missing for me is it doesn't have powers of abstraction.

• 50:31Speaker 04

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

• 51:12Speaker 03

  Yes.

• 51:12Speaker 04

  And maybe they are to some extent.

• 51:14Speaker 03

  It's very limited. I feel like, you know, machine learning more than I do, but to me feels like they wake up and they leave breadcrumbs for the next one that will wake up and just reads all the breadcrumbs and do the next step. They're not really the memory, I like breadcrumbs for the next one. They're not changing their weights in any meaningful way. It's almost like.

• 51:42Speaker 03

  And there's so much you can do. You keep leaving bad breadcrumbs for the next instance that we wake up and reach all the breadcrumbs and take the next action. But eventually, they diverge and that's where the humans help a lot. Keeping them in the right direction, right? Does this match your?

• 52:03Speaker 04

  I have a feeling that the reason why we can do this abstraction is because we are we're in the world and we could have done differently. You know, we have agency, we can, you know, towards doing a goals, we can actually kind of subject to the constraints that we are, you know, that we have applied to us. We can try different things. An example of this is if I hire a video editor. So I've been evolving video editing skills for five years and I could say to the video editor, okay, I'm going to optimize your process because I've learned all of these important lessons. So always use a tripod, don't even bother holding it by hand because you're going to have lots of problems with there. So, you know, let's just, we're going to prevent that problem from even

• 52:45Speaker 04

  happening. And I can lay a load of constraints and they would have competence without comprehension, right? But they would always be pushing back at me and they would say, oh, you know, I want to try this and I want to try that because they don't know why those constraints are. I understand it because I understand the space of possibilities and I know why those constraints came to be.

• 53:03Speaker 03

  You know, I agree. It's like you learn by experience. Your experience taught you that. And yeah, learning from your experience, they do not experiment themselves. Yeah. For example, S M T, I mean, you mentioned Z three. If you ask questions about a S M T implementation to large language models, you're going to get exactly the textbook explanations. But the large language model never tries them. It is repeating the learnings from people that wrote the papers, right? That's exactly what you said. They are repeating, they are not, they are not trying experimenting themselves.

• 53:49Speaker 03

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

• 54:03Speaker 04

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

• 54:45Speaker 03

  Yes.

• 54:46Speaker 04

  Yeah.

• 54:47Speaker 03

  Learning by doing it gives you new perspective, right? Maybe the AI can get new perspectives by learning, by doing itself, right? Not relying on what we did, but learning by doing itself, maybe updating their own, their weights and.

• 55:06Speaker 04

  That's conceivable. And maybe it's just a matter of computation.

• 55:11Speaker 03

  Yes.

• 55:11Speaker 04

  And maybe if we did have a society of agents that were actually doing weight adaptation. But it would be quite difficult and possibly dangerous in some ways because the good thing about having big fat models that are trained every six months and, you know, on a platform is we can, we can put safety guardrails on there and, and at least there's only one model to check. I mean, just, just imagine, this is something that interests me as well, is the extent to which the, the platform owners should be responsible versus individual engineers' responsibility, right? Because if I, if I make a sophisticated agentic system, it's already got to the point now that I don't read, I don't think anyone should be deploying

• 55:53Speaker 04

  Fable class models in production, you know, so maybe during the, the development and the R and D phase, you need more intelligence and then the engineers place constraints in and then it should get to the point where it's halfway between a normal software application and, you know, so, so then maybe we, we would have a lower intelligence model in production. But how much responsibility do you think the engineers have for kind of degenerate behavior?

• 56:17Speaker 03

  Well, the main difference is you're talking about a scenario where the application has AI embedded insights, right?

• 56:28Speaker 03

  If you have this scenario, I think it's super important to have guardrails, right? To have, and even better if your guardrails are verified using a system like Lean, you're proving properties about the guardrails. Some people are talking about having verified sandboxes in the future.

• 56:50Speaker 03

  Yeah, I would love to see that. In my mind, I always use AI to develop software that does not contain AI. Lean does not contain AI, right? This is a much safer scenario, right? And many people are using like that. They build applications, but the applications themselves do not have AI embedded in them. It is a much safer scenario, right? You're fighting against bugs in the application, not putting guardrails around this AI.

• 57:22Speaker 04

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

• 57:35Speaker 03

  Really hard to tell, right? I mean, I couldn't predict. One year ago, I could not have predicted what happened so far, right? I mean, I cannot even imagine in five years. It feels like it's accelerating, it's moving way faster than we expected. Sometimes people ask me, do you fear being, becoming obsolete? I would feel like we leave. I mean, developing software, it would feel like mission accomplished. I don't have to do it myself anymore. Maybe I can spend my time only with implementing softwares that do not have to work. It would not be the end of the world. I hope. One thing I want

• 58:18Speaker 03

  to become, I think we are always going to be in the loop. Because we have to keep always, the specification saying what the software should do will be always our responsibility. We're the ones that are benefiting from the AI. We're the ones that's saying, this is what we want. We will be there somewhere, even if it's just at the specification level, stating what we want. Of course, people can create scenarios where the AI is super intelligent.

• 58:50Speaker 03

  We have robots and we talk to the robots what we want and they go in natural language and they are obedient, they do exactly what we ask it. But we're still the ones telling them what to do. I feel like we are always going to be some role for, for us in the future.

• 59:12Speaker 03

  But I can see the exciting parts. I mean, how many, as a developer, most developers I know have many ideas, but they only implement a small subset of them. Because time is finite. I mean, they, they don't have time to implement all their ideas. And they see, many of my colleagues, they, they see the ones that have the most, the ones that are most probable to work. It's like you're playing a game, saying the effort versus the chance it's going to work. And many of the ideas you discuss, say, this very low probability is going to work. I mean, but with AI, we can try

• 59:53Speaker 03

  more ideas, right? I give the example of your him. I mean, he's not vibe causing the sense people do, but for trying ideas, he sends the AI in different missions and sees the ones that are worthwhile, his time to implement them. This is already a big win, right? I mean.

• 1:00:16Speaker 04

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

• 1:00:44Speaker 03

  Yeah, I can see Mathlib.

• 1:00:48Speaker 03

  In the near future, people will use the AI to maintain the proofs, to construct new proofs, proofs that are boring, that nobody cares. But the key ones, they will still write by hands because they want them to be beautiful or have some specific structure that's good for teaching, for communicating ideas. Coming up with the roadmap also is going to be a human activity. What is in MathLib, what is not? How do we define the rings? Another mathematical structures is all going to be done by humans. There are lots of exploration happening. For example, one cool idea was, and I've seen people find this idea, let's say I is

• 1:01:31Speaker 03

  substituting the whole mathematical library. What's going to happen, right? It can be garbage, but how do we control these processes? Johann Komeling, one of the main people behind these formal frontiers, they just to have, one way to control the process is to have key theorems that are super simple to state, but need a lot of math to be proved. If the AI managed to construct a proof of this key theorem, it's doing something worthwhile there. One example is Fermat's theorem. I mean, you can write, you only need the natural numbers to state the theorem.

• 1:02:16Speaker 03

  It's very simple, but you need a lot of math to prove it. You can say like, this is a milestone for the AI. You can build your crazy library, but you have to get there. I mean, you have to show me you got there. And you can have many of these milestones that are easy to state, but really hard to prove. And if the AI managed to build a library that allows you to prove that, maybe it's worth our time looking what is there, right?

• 1:02:44Speaker 04

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

• 1:03:27Speaker 04

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

• 1:04:10Speaker 03

  Okay, I think there are two ways to answer your question. One is whether techniques like Alpha证, it follows the Monte Carlo tree search, is like a hybrid technique, you can maybe even say is a truly neuro-symbolic technique for proving, whether this pays off or not, right? And the other one is that, do we need formal verification at all? I think the answer to the second question is yes. Even if I have a model that generates right answers 99.99999% of the time, we still want

• 1:04:53Speaker 03

  certificates. Just to give an example of how proofs can get massive, this unit's distance conjecture that OpenAI proof false, Boris Alexey, it's a proof to, it's 1.2 million lines of Lean, the formal proof. Nobody wants to check the proof line by line, right? It's great to have a certificate. I think having certificates as a machine checkable, this excellence, having moves, that if you're playing with the AlphaZero architecture, the moves, or a large language model is saying,

• 1:05:34Speaker 03

  boom, boom, boom, these are the moves to do it, you still have the moves, right? It's just how you produce the moves are differently. I think having the moves in the game, viewing math as a game, this is valuable and will stay, right? Because the AI will synthesize a formal proof that's a sequence of moves independently of the fact if it's an LLM, an agent controlled by LLM, or it's a Monte Carlo tree search combined with some kind of neural network. The question why it pays off or not is still open.

• 1:06:17Speaker 03

  I mean, everybody's impressed. I mean, the community with GPT-5.6 and Claude Fable, they, I think, outperform all these systems that are using Monte Carlo tree search. But then we have to ask the question, the cost, right? Which one is cheaper? I was talking with some colleagues that are doing these experiments during the conference this week, and they told me it's not clear because each move of these systems using the hybrid approach of Monte Carlo tree search with, the moves are much cheaper, but they're making way more moves because the moves are dumber.

• 1:07:01Speaker 03

  The LLM is more expensive, but it gets there faster, right? It's still debatable. I can imagine in the future that for some domains, this hybrid approach works and the LLM works. There are also scenarios where it goes, we improve so much the hardware that is so cheap that nobody bothers with hybrid approaches anymore. Everybody's using just large language models or something like a large language model. This part is still huge debates, whether it pays off or not.

• 1:07:38Speaker 04

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

• 1:08:08Speaker 03

  Yeah, well, there is still lots of work to be done, right? I mean, one thing that we want to improve a lot, Lean is a programming language, right? We want Lean to generate code that's competitive with Rust, right? Especially for ray-manipulating programs. There will be a lot of investments there. A lot of investments in Lean as a platform for software verification. One thing is to verify some library or the other thing is to verify full systems, right? I mean, that's much bigger. We want to invest there, make sure this Lean scales. We want to make sure that, we have been keeping up with MathLib growth, but MathLib, the growth is by humans.

• 1:08:53Speaker 03

  Just to give you perspective, MathLib from 2025 and now, MathLib grew 44%, but the completion time reduced by 10%. This way, we are making Lean faster and faster, but with AI now writing math, we have to step up. I mean, AI, the library can grow way faster than we can keep adding improvements. We will need AI to help us to improve the performance and keep up with the size of the library. So scalability will be a big issue. How do we support a library that's 100 million lines of code? This is an open question. Scalability, Lean is a programming language as a software verification platform.

• 1:09:38Speaker 03

  And then improving trust, we want to have a verified compiler, the code you generate from Lean. People don't understand that the trusted code base for Lean, if you only want to prove theorems.

• 1:09:51Speaker 03

  Is much smaller. You only care about the kernel. If you only care about proving theorems, but if you care about, suppose you wrote a programming Lean, you prove a property about it and you generate executable. Today, the trust code base includes the compiler. That's much bigger than the kernel. And we want to prove this compiler. We want to remove, in the future, we want to have a compiler that has been verified and you do not have to trust us that this compiler was implemented correctly. Not because we are malicious, but because we make mistakes. I mean, like everybody, reduce the trust code base will be an activity, right? From now

• 1:10:32Speaker 03

  on, we want to keep reducing, AIs will keep getting better and better at finding vulnerabilities, exploits. You want to keep improving that, making sure that Lean is a platform, I mean, for developing software and math, a- a- about legacy. I- I- even if I die today, Lean will continue. I think the Lean flow is amazing. I think the folks there can take care of everything, even, yeah, they don't need me. I- I- I'm always trying to help, but the project would continue even if I die. I mean.

• 1:11:08Speaker 04

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

• 1:11:15Speaker 03

  No, no, no. Even in my wildest dreams, I never imagined that Terrence would be using, people like Terrence would be using Lean, right? And giving talks about that. Never imagined that. I thought, I felt like we are building a platform for refined safety critical systems and they would be, the proofs would be done by hands, right? I mean, it's, it's, some people claim I'm lucky, maybe I am, because making Lean interactive was great for AI. The tree is a black box. The AI has very, cannot influence, cannot guide

• 1:11:55Speaker 03

  the tree, but it can guide Lean, right? I was really lucky. So many amazing people like Jeremy, meeting Mario, I mean, I found him in obscure conferences, Sebastian Ulrich, your head, Brayton, and so many, Kim Morrison, so, so many, all these folks at the flow. Yeah, all the colleagues, I mean, yeah, it's, it's incredible. Kevin showing, Kevin Buzzard showing up, Kevin Hartnett taking the interest, writing articles. Yeah, it was, yeah, maybe I'm the luckiest person in the world.

• 1:12:42Speaker 04

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

• 1:13:12Speaker 03

  Well, for software developers, I would recommend start using Lean as a programming language. Just write codes, ignore the proofs. Don't try proofs at the beginning. Start writing codes and playing fit is a cute thing, right? Then when you're comfortable with the Lean syntax, you go to the next step. You start trying to prove simple properties about your codes. Another thing that I tell everybody, have your AI agents around. They know lots and lot. They know everything about Lean. They know Lean better than I do.

• 1:13:50Speaker 04

  I finally down that.

• 1:13:52Speaker 03

  No, they can explain. I mean, they can explain extensions that they do not develop. Lean is extensible. They know about all extensions and they read the documentation. They will read the documentation. Very few users read the documentation. The AI reads it and can explain through you. You can tell the AI your backgrounds. For example, a software developer is vague. If you have, for example, a software developer that has been using Haskell or Lisp, it's going to be much easier to learn Lean because they are all functional programming languages. But suppose you can tell the AI, I'm a C sharp developer or Java developer.

• 1:14:34Speaker 03

  The AI now will calibrate the explanations for customize to your backgrounds and they will effective at teaching you Lean step by step. You, you, if you open a video that I can see, it's very overwhelming with many tactics that are like moves in my game, in the game of proving theorems. You can ask the AI, explain to me, this is the background I have. Tell me what I should know before I even try to understand this example. It's really good that's that.

• 1:15:11Speaker 04

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

• 1:15:14Speaker 03

  Thank you.

• 1:15:19Speaker 05

  Now, more than ever, we need someone on our side. But Rob Whitman? Whitman's votes drove up costs, cut Medicaid and risked 350,000 Virginians' healthcare to pay for tax breaks for himself and his donors. He's not on our side. Shannon Taylor will fight corruption, cut taxes and bring down costs. This November, vote for Shannon Taylor. She's for us. Paid for by HMP, the HouseMajorityPac.com, not authorized by any candidate or candidate's committee.

• 1:15:49Speaker 06

  Your heart can tell you a lot about your health. Apple Watch Series 12 measures your heart rate every five seconds with the most accurate heart rate sensing in wearable. So your vitals app, now with heart rate variability, can tell you when something is off. And your readiness score can let you know when to rest and when to push. Hear the story in every heartbeat with Apple Watch Series 12. The features described are for wellness purposes only and not for medical use. iPhone 11 or later required. Based on Apple conducted study of heart rate accuracy, August 2026. Visit apple.com slash apple watch series 12.