AI能写出证明，谁来检查？——Leonardo de Moura

A refutation—I think it was a refutation—of the Collatz conjecture was presented as a proof in Lean. The claim is that it was accepted by the official kernel that ships with Lean. Wow. I mean, that's terrible.

We firmly believe that AI created this. One bug is exploited in the official kernel and a completely different bug in another one. We don't have the patience to deal with such low-level implementation, but AI does. I think this will change the rules of the game.

Moving on to better models, they continue to do amazing things, but at the same time, they do stupid things. Boris Alekseev presents a proof with 1.2 million lines of Lean code—a formal proof. Nobody wants to check this proof line by line.

I am Leonardo de Moura. I am the creator of Lean, the chief architect, and co-founder of Lean FRO, the nonprofit organization behind Lean. I am also a senior principal scientist at AWS.

1. Cathedral or bazaar: who controls Lean's core?

At some point, you actually isolated the main part of the system and said, “Okay, this is locked. I control this.” There’s an interesting tension here, isn’t there? A lot of creativity sometimes arises in the community.

There are different levels of adaptation. There is the main part. For example, the shooter Quake 3 had bounce bugs, and a whole community formed around speedruns, those bugs, and stuff. Similarly, Lean now has a core system, there’s mathlib, and there’s a whole community that’s getting creative in different directions.

The main part adapts much more slowly and is controlled by you personally. What do you think about it? Do you feel like you have control over the Lean ecosystem, or does it take on a life of its own?

I mean, okay, that’s actually a great question. No, I no longer control the core system. We have Lean FRO, a nonprofit organization. We have 20 people there. Each of them owns part of the system.

I like this model.

Developers on the core team own parts of the system. This is their responsibility. They have property rights. Whether to accept external pull requests or not is up to them.

But for the first 10 years, I essentially owned most of the system. Sebastian Ullrich, my colleague and friend with whom we co-created the Lean framework, owned other parts of the system.

I strongly believe in the cathedral model for open source. A cathedral is when there is a central body that decides what will go into the codebase and what won’t. There is also a bazaar, where everything is more open and everyone can contribute.

There was a lot of tension with the Lean community. Many people sometimes want to contribute to the kernel. A contribution to a library is different from a contribution to the core system.

A library, in many cases—let’s say you’re creating a library for binary trees—is autonomous, isn’t it? You can control the changes you make there without affecting the rest of the system. But in the core system, all parts are interconnected. They depend on each other.

For example, a binary tree library may lack some features. It may lack some theorems about its functions, but it is still useful. A system full of holes isn’t very useful, is it? If there are a lot of missing parts and failures, it’s a more interconnected system. That’s why I always insisted on a collegial model for core development, and that created tension.

One good thing about this is that I made Lean extensible, allowing people to add their own extensions without changing the core. It became very popular in the community. A lot of people have implemented extensions for Lean without consulting us.

They implemented it in a way that is similar to the example you gave. They implement object-oriented languages that hide complexity by focusing on a specific subject area, such as distributed protocols. You can specify distributed protocols with a language optimized for this. It hides all the complexity, and it can be done without even talking to us.

Sometimes they show me things. They had never met me before, and they implemented this beautiful extension.

2. Why Lean's core stays small and protected

Yes, I think that’s great. This was also a nice side effect. Can you give me an example of this?

Well, when solving abstract problems, sometimes very inventive and creative approaches come up.

Do some of them really surprise you when you see what people do?

I remember last year, Ilya Sergey, a professor in Singapore, was with his student Vova. They showed me something, and I said, “Why are these people demonstrating this? This is not Lean.”

It was a very cool demonstration. At the end, they said, “No, no. It’s Lean.” This is an extension that they implemented based on Lean.

I was very surprised. This was for software verification. They have a language that makes it much easier for people to verify software, especially imperative software. Yes, I was impressed. They stunned me with their demonstration.

Is that part of the reason why you’re so protective of the core? If you think about it, Lean’s reputation is the most important because it’s a tool for software verification, mathematics, and so on.

It reminds me a little bit of MATLAB or maybe Mathematica. There are incredibly optimized core libraries for linear algebra out there, but someone might come along and, with great power comes great responsibility, they might just screw things up by doing operations that aren’t already vectorized. That will cause slowdowns, and maybe in Lean they’ll do something that affects the integrity of what they’re building.

Is this part of it? Do you want to establish a little more control?

Yes, that’s also true. There are people who add something unfinished. Many people like to have fun developing software. I like the saying of one of my fellow scientists: programming is only fun when the program doesn’t have to work. If it has to work, the pleasure quickly disappears.

The first problem is bugs, as you mentioned. People add bugs. The second problem is someone submitting a feature that is not fully implemented. It has many gaps. It seems like it’s working, but it’s not.

Third, people can capture the design. They add a feature; it’s complete and correct, but it imposes limitations on system optimization. Now that this feature has become popular, it prevents us from doing more important things because it’s already there. People are using it, and we can’t easily remove it. We’re stuck with that.

3. The Slack purge, Brandolini's law and the Lean FRO

Another problem is that it’s extremely important to prioritize development. A chaotic approach, with the introduction of random functions, is what happens if you start merging random PRs. This is very bad. It doesn’t scale. I believe that prioritization is extremely important, and this model, where you keep merging random PRs, doesn’t work. This is my firm belief.

So, you are a proponent of the depth-first search approach. When you build something successful that involves a lot of other people, you have to operate more on the principle of breadth-first search, all because there are so many requests every day.

I remember a passage in Kevin’s book where he said that, at some point, you kicked a lot of people out of a channel in Zulip. You said, “Listen, I just need to focus right now because this is getting ridiculous.”

Yes. I forgot about this story about the exile. At that moment, I really didn’t like people who kept throwing ideas around. They were just having fun.

I mean, I tried to create something that works. Some people were in the Zulip channel, having fun and brainstorming ideas. It’s cheap. You can just throw ideas at the wall, and the other side has to keep telling you, “No, that doesn’t work.”

This is one of the most frustrating scenarios for me. You throw out an idea without having spent even 5 minutes thinking about it. Then I find a hole in it and send it back to you. You polish it a little and send it again. Now it takes 10 minutes to find the next hole.

Finding holes in an unfinished idea takes more and more time in exponential progression. For the person who invents them, it’s fun. But that’s not fun at all for the person receiving them, right? You have to do your job, and now you spend time explaining to people why it’s not the best idea and why now is not the time to do it.

There was a moment when I kicked out a few people. Only the core team that really contributed to the project remained—only people who wrote useful code for the project.

Apparently, now with generative AI, it’s even worse. What you’re talking about is called Brandolini’s law: it takes exponentially more effort to refute stupidity than to create it.

Well, luckily we have Lean FRO now, right? I have many colleagues and many people who help me, and my life has actually become better.

For example, we had a serious mistake this week. Joachim Breitner took it upon himself. It’s not just the mistake itself; we need to take care of the community, explain things to it, and communicate. He did all this for me.

Before, this would have been a nightmare. You have to deal with so many people and so much noise. Joachim did that, and we have many other people in Lean FRO who help coordinate the community and communicate the roadmap.

It’s much easier for me now. If it weren’t for Lean FRO, we wouldn’t be able to manage the Lean projects right now.

4. The Collatz exploit: two kernels, two bugs

What was the mistake this week? Something to do with the Collatz conjecture?

Yes.

Yes, I was going to ask you about that. Maybe you can tell me about it?

Yes. At the heart of Lean is the concept of a small trusted core. Lean is huge; it has millions of lines of code. But to trust our results in Lean, we only trust the core.

It’s much smaller, right? We also have other kernels. The sequence of events—I mean, Joachim did the whole investigation. I’m glad he did it. The sequence of events was as follows: a week or 10 days ago, an error was found in one of the main external kernels.

We have many kernels. One of the main external kernels is called Nanoda, and it is implemented in Rust. The error was immediately fixed by the Nanoda developer. A few days later, this proof—I think it was a refutation of the Collatz conjecture—was submitted along with the proof in Lean. It was claimed to be accepted by the official kernel that ships with Lean and by the main external kernel, Nanoda.

That would be—yeah, wow. I mean, it’s terrible, right?

Our first reaction was that Nanoda didn’t accept the proof. Then Joachim said, “Okay, these guys are exaggerating. Nanoda does not accept it.” But then he said, “Oh, Nanoda didn’t accept the proof 10 days ago.” And then they actually wrote the exploit.

We are convinced that it was created using AI. It exploits one bug in the official kernel and a completely different bug in Nanoda. I fixed a bug in the official kernel, and I found a strange example because there were a bunch of strange things in it to create a hash collision that were completely irrelevant. I asked, “Why did they put that in there? That’s ridiculous.”

This is nothing else—I mean, it was there to exploit a bug in Nanoda. Then Joachim asked whether we had asked an LLM to look at the pull request submitted to another repository. They said it was a coincidence, but they couldn’t rule out the possibility that the LLM itself had looked at the other repository, seen the pull request, and created these exploits.

Before coming here, I spoke with Joachim about how to improve the defense, because this will continue to happen. AIs are very good at finding errors in logic and vulnerabilities in kernels. We’re afraid, so we say, “We should introduce rewards for those who create bulletproof kernels.” They could be paid if their kernel is unhackable within X months.

Another idea is to simplify the kernel to make it easier to test. Another thing is to support Mario Carneiro, who is trying to prove the correctness of the kernel. We should try to help him or speed up the development of his proof. I mean, yes, on the way here, I talked to Joachim about how to improve the situation and avoid something like this in the future.

There are concrete steps, one of which Rob has already taken. We have a “comparator” tool that exports proofs, because some people might use metaprogramming and extensibility features to implement false proofs. You can even call a function and corrupt memory, for example. So, we have a comparator that exports proofs, and we test them in a sandbox.

One of the lessons is that the comparator should always download the latest version of Nanoda, right? This way, we don’t have to update Nanoda manually. If someone submits a bug fix to Nanoda, it will be immediately used in the comparator.

And the comparator would reject that, right?

It would, yes. And we do that. But we still have a lot to do. We want to prove more things about the kernel and the code generator. This is another area we need to improve.

5. More kernels, reward hacking and safety by transparency

Yes, but I can’t imagine this situation without Lean FRO’s help. I wonder whether this situation is similar to the incident where GPT-6, let’s say, broke Hugging Face recently. After all, models are becoming increasingly prone to reward hacking and profit-seeking.

I don’t know whether you think—I mean, maybe you implied that it was a similar situation—but there was essentially a green check mark, so it looked as though the proof was valid. Sometimes these proofs are quite confusing, and they’re hard for people to read. So, in principle, an LLM could have engaged in reward hacking: instead of acting in the spirit of what was wanted, it did something else.

What OpenAI did was change its evaluations. When a model generates code, they don’t just look at the code in isolation. They look at the entire trajectory, at the course of reasoning. They try to distinguish the intent behind it from the intent of the developer who made the request. So, do you see something like this here, where we might need almost separate adversarial systems to evaluate what happened?

Having multiple kernels is one way to achieve this, right? If you have independent kernels implemented by different people using different programming languages, that makes things better, doesn’t it? The fact that we have the official kernel and another one—we want to have more.

What Mario is doing, called Lean4Lean, will be special because he proves that it should be correct. So, it won’t be just another kernel, but a kernel that has been proven correct. This will be a big event when it appears.

We can use Lean4Lean today, but it’s not fully proven. It has proven many parts, but not the parts related to the exploits. If he had proven those parts, he would have found the bug before it was exploited. So, having multiple kernels, some of which are proven correct, makes the story truly bulletproof.

Then there is the next level. You might ask, “Okay, you’ve proven that the kernel is correct, but you compile with some compiler.” There might be a bug in the compiler, right? You proved the compiler correct, but what actually runs is not what you proved, right? The next step is to prove the correctness of the compiler.

Then you can say, “Well, there might be a hardware error.” So you say, “Okay, let’s ask Intel to publish formal specifications.” This is what they call the formal specification for a microprocessor. The same applies to AMD and so on.

Yeah, the whole point of this movement is always to reduce the number of things you have to trust. Isn’t that right? That will be important, right? If we ever want to get great results, we won’t have to waste time manually checking for vulnerabilities. It’s very important that we can fully trust this mechanical evidence.

I wondered if this was an example for you, since you are also an open-source advocate.

Yes.

But let’s say we look at an AI benchmark called ARC-AGI-3. They use a semi-private dataset and a private dataset. Of course, they’re trying to prevent model hacking and data leakage from these sets. When they test on a private dataset, they know that the models haven’t seen it before.

Do you think this is an exception you could make in your philosophy? Or maybe we need a separate, independent, private kernel that can’t be hacked, so that we always have a trump card up our sleeve for verification?

I don’t like security through obfuscation or hiding. I believe that we should always be transparent. Otherwise, you end up saying, “Look, I have a nice kernel for checking the results, but I won’t show anyone.”

For the sake of transparency and trust, you should be completely open about these kernels. Right? We can improve the situation by proving the correctness of these kernels and adding more kernels implemented by different people, but everything should be transparent.

That would be security through secrecy, and it goes against everything our community believes in.

6. Kim Morrison, Claude and the zlib proof

So, it seems that Kim Morrison used the Claude Code agent to create an implementation of the zlib compression format in Lean and prove some of its specific properties. What exactly did they manage to prove?

When Kim started working on this project, I thought, “Wow, this looks hopeless. No way.” I thought that was the case at the beginning of the year. I thought AI wasn’t good enough for this and wouldn’t be able to succeed.

But they managed to translate the code from C to Lean. Then they fixed the implementation in Lean until it passed the C version’s test suite. This proves that, for any compression level and for any data, if you compress it and then decompress it, you get the original.

At the beginning of the year, this seemed unattainable for AI, but it was able to do it—and it didn’t stop there. Kim asked it to optimize the code, especially for this type of program.

Currently, Lean is not a language for manipulating arrays. Lean was optimized for processing and manipulating trees, because you work with terms, right? Internally, you are manipulating trees. You have syntax trees and expression trees. Lean is really good for those kinds of programs, but not for arrays.

In my opinion, Lean will never be competitive, right? But it turned out that Kim asked the AI to continue trying. He told it, “You can act boldly. Keep optimizing your code. You must continue to prove the property. You cannot violate this property.”

It ended up being a bit like the implementation in Rust, and Rust is a very efficient language for manipulating arrays. That was really unexpected, right? Imagine if we improve the way we work with arrays in Lean—how far we could go.

There are so many possibilities, right? We can ask AI—let’s say we give it the semantics of an x86 microprocessor and an assembler. I think very soon you will be able to ask AI to write assembly code using all these complex instructions, but with proofs of the properties.

That’s true. We don’t have the patience for such low-level implementation, but AI does. I think this would be a game changer, right? Last year I thought it was impossible, but now it’s quite possible. This experiment shows that there is a way to do this.

These AIs will continue to get better at these tasks because they have a clear signal that they’re on the right track, right? You still have to prove the theorem, right? You can’t cheat.

7. Can we specify complex systems?

Yes, I think the possibilities are endless. Yes, it’s so attractive. I am passionate about the idea of specification-driven software development. We have already had similar periods in the development of AI. For example, there were expert systems, and we had the concept of a knowledge engineer or ontologist.

There are certain things that we just understand. We can be computer scientists and boil them down to the essentials. But I think a big part of software development—and the reason we have Agile—is that the world is so complex. The steps to get to the specification are difficult, and after thousands of iterations, we have moments of epiphany where we compress and collapse some of it.

So, I guess we have a chicken-and-egg problem. When dealing with very complex systems, we can’t yet specify them, or, if we can, we can specify them only partially.

Yes, I agree that this happens very often. You know some of the properties that a system should have, but not all of them. It’s worth interacting with users about what features the system should have.

Believe it or not, this happens all the time with Linux. With the kernel, it’s clear what it should do, but the system as a whole consists of many components. I mean, there are a lot of them. For example, those system calls I mentioned—what should the system call do?

We implement something, and it’s quite common for a user to say, “Oh, no, no, I want more. I want less. I know this is doing too much. I want more control. I want this checkbox. I want to have a way to control where the proof goes—more control.” It’s a constant dialogue.

They expect the specification not to be very clear, right?

Yeah, I think you’re right. In many cases, the specification is not clear. But it’s important to start documenting the properties that you know should be there and to discuss them with the customers.

8. What's next for Lean, and its legacy

I think it’s worth remembering that a high-level program in a very high-level programming language like Lean, without any optimization, can be considered a specification, right? You can say, “Look, this is what I want to compute.” It’s not very efficient, but this is what I want to compute.

And you can ask the AI, “Optimize this function for me.” I’m implementing the simplest right idea, right? Without any fancy data structures or complex algorithms, it does what I want it to do. Now it’s the AI’s job to optimize it.

9. Specs change: proofs are cheaper to redo with AI

I suppose that the engineering of getting the specifications can be done—we can optimize that process. We can make it interactive, with a lot of feedback and so on.

But if we were to go to a model where the specification comes first, and we have globally distributed software, would there be a problem with updating the specifications? We have software that’s deployed based on a previous specification, and here we’re doing development while someone else is updating the specification. How do you think that would work?

Oh, yes, absolutely. When you update the specifications, the generated code can become invalid. The proof that the code conforms to the specification needs to be canceled.

Formal verification used to be a big deal, right? People would say, “Oh my God, I spent so much time proving the implementation was correct. Now these people want to add this cool optimization. Now I have to redo a lot of these proofs.” It’s not rocket science, but it’s a lot of work.

But it turns out that AI is very good at updating these artifacts for us, right? Before AI came along, it was a really big problem, wasn’t it? Especially for safety-critical systems, formal verification was used in subject areas where the specification was very clear, like cryptography. The specification is very clear, right?

They verified the microkernel. People thought a lot about the microkernel before they even started verifying the designs. All these famous verification projects, like CompCert and seL4, involved people thinking a lot about the specification, right? In some cases, they had to update it as they went along, and it was painful—to the point of horror.

But now that we have AI to update the evidence and the artifacts, it’s a lot less painful, right?

I can see that in the near future, right? AI is too expensive, right? People will say, “Well, I’m updating the spec. Now I have to spend billions of tokens to update everything.”

This is really exciting, because, if I remember correctly, Kevin wrote in his book that Z3 seems to have helped fix an incredible number of bugs in Windows 7 before it was even released. So it was a real lifesaver.

But we know that these technologies are mostly used for high-risk software. Do you agree in principle that everyone will do this in the future? Should every developer be writing this kind of software?

They might not even know they’re using formal verification, but it’s going to be in their workflow, right? They’re going to write properties, and those properties are going to be checked. The code will be updated, and there will be proofs that the code should evaluate to the same thing. People will write PRs, and they’ll get proofs of whether or not a PR violates any properties in their test suite.

Yeah, I think even if they don’t know they’re using formal verification, it’s going to be there.

10. From Lean 1 to Lean 4

Tell me about the evolution of Lean. The first prototype came out in 2013, then Lean 2 in 2015, Lean 3 in 2017, and Lean 4 took a really long time to develop. Tell me the whole story.

Oh, wow. Okay. The first version of Lean was even called 0.1. I learned as I went. I read a lot of papers on type theory, and I used some other systems. But I always feel like you get a completely different perspective when you implement something in practice. There are so many nuances and details that you only discover when you go, “Wow, that’s really important to me.”

In Lean 1, I also tried to make everything very compact—maybe even too compact. It was unusable. I think only Jeremy and, I think, Floris, one of his students, used Lean 1. But they were heroes. It was a terrible system. It was more like a training tool that I used to learn dependent type theory.

Then Lean 2 came along, which was more serious, and I think it had 50 to 100 users. Very few. One of the lessons came when I went to MIT. Adam Chlipala is a professor there, and he said to me, “Look, you need a real tactics system.” A tactics system is a set of steps.

One thing he wanted to say was that these steps had to be extensible, right? You had to be able to add new steps as a user. That was the main lesson of going from Lean 2 to Lean 3. We added a new framework for writing these steps. Users could write them, and they could write them in Lean itself. You didn’t have to use another programming language.

That became very popular, and then Mathlib came along. It all started to grow very quickly. It became clear that Lean 3 had limitations. In terms of scalability, the system was such that you could extend tactics, but that was it. Some people managed to make linters. The Mathlib community figured out how to hack Lean to write linters in Lean.

11. Lean 4's extensibility and Mathlib's growth

But we wanted to make it fully extensible. In 2018, Sebastian Ullrich and I said, “Let’s do this.” At that point, I wasn’t a programming-language expert, to be more specific. I was a machine-learning expert and a formal-verification expert. Lean was actually the first programming language I ever implemented, right?

The syntax was terrible. There were a lot of weird things in the implementation, and we said, “Okay, now we know how to do this. Let’s do it properly in Lean 4.” Then we started, and implementing Lean in Lean turned out to be much harder than we expected. It took us from the beginning of 2018 to the end of 2020 to get Lean to compile itself. But it was really exciting to get there.

12. Dependent types in plain terms

I don’t think we explained dependent type theory enough, so maybe you can do that. There’s this relationship between the expressiveness space of the problem descriptions and how complex the kernel needs to be. I think before, you were pretty sure that you wanted the kernel to be pretty small and optimized, and you had to accept more complexity than that.

Yeah, yeah. But that was in the design phase. I mean, that was before Lean 0.1 started. When I started implementing Lean 0.1, it was dependent type theory, right? It always was. All versions of Lean are based on dependent type theory.

When we were deciding what to implement, at the design level, there was this discussion about dependent type theory. To explain to the audience what dependent type theory is, I think one example is to say that in dependent type theory, you can have a structure with 2 fields, X and Y. Let’s say they’re integers. You can add a third field where the type of this field is “X is greater than Y.”

This is a proof. You have to fill in this box with a proof that is evidence that X is greater than Y. You can think of this as an invariant. It’s called dependent because the type of something can depend on the value of something else. The type of this third box depends on the values of X and Y. That’s why it’s called a dependency.

You can model invariants. In functions, you can have, for example, a function that takes X and Y, with a third argument: Y must not be zero. In order to call this function, you have to provide evidence that Y is not zero. It’s almost like a precondition.

That’s the beauty of dependent type theory. The simple idea is that you can fix the preconditions, model the postconditions, and have invariants.

You don't have to invent all these concepts. It's all very minimalistic, actually. But it complicates your type theory because you have these dependencies that you have to manage. But it's worth it. I mean, it was worth it.

Yeah. So the core had to be much more complex to maintain. What can you do in Lean 4 that you couldn't do in Lean 3?

Lean 4 is completely extensible, right? Everything is implemented in Lean. You have access to all the internal data structures. When you write your Lean declarations, you can write code in the same file that accesses the internal representations of everything.

For a lot of the early AI researchers, that was really important to them. They could pull training data from the internal components of Lean. They could write code in Lean that pulled information about all the evidence that was in Mathlib. They could manipulate those objects. That was really important to them.

All of these extensions that I've been talking about, like tools such as Verit and Veil, leverage this extensibility that we have in Lean.

I saw in your slides that you presented this week. I think we've already reached a tipping point where there's as much Lean 4 code in Mathlib as there was in Lean 3.

Oh, yes, much more. Much more. Mathlib 3 stopped at 1.1 million lines. In Mathlib 4, we have 2.4 million.

But what's interesting to me is that Kevin Buzzard seems to have said something like, “It's going to keep growing forever.” This is always going to be—I think he said—at 0%. I think that's quite instructive about the nature of mathematics, because it's something that's constantly evolving in many different directions.

There's a temptation to think of mathematics as this kind of distilled thing that we just discover, and there it is. But is it or isn't it?

No, it's going to keep growing forever. There's always going to be new mathematics invented, new structures defined, and new mathematical objects. There's always going to be new things.

There's a debate about whether it's worth keeping everything in Mathlib or not. In the beginning, of course, it was great to have everything in one library. In a library, you have a lot of concepts from mathematics. For example, you have rings. In the Lean math library, there is only one ring.

The consistency of the library is important. In other programming languages, very often there are many implementations of the same thing, and these things are incompatible. If you want to prove a statement about your code, it is important to have this unified view.

There is also another great thing about Mathlib: they decided that they would always strive for a more general, the most general, description of something. That was also great.

But is there a size limit, right? Mathlib has 2.4 million lines. Imagine if it had 50 million lines. Now it's starting to get to the size of the Linux kernel, right? All the big projects that we have, like Firefox, are comparable in size.

These projects have teams of people who are just maintaining the build system. Things get more complicated. Sometimes they have their own version—a specialized version-control system—to deal with the complexity.

There's a lot of discussion going on right now about how to develop a math library. Maybe Mathlib will be a collection of libraries. You have the main one, like the standard library for math, and a lot of side libraries. All of them are maintained, all of them are consistent, but with different management. You don't have the same group of maintainers for each one. All of these discussions are happening, and I think they're useful.

Yeah, but people predict that if you want to have all of the core mathematics, the library has to be 100 million lines. If you want to be able to formalize arbitrary scientific math papers, the library has to be 100 million lines. Some people in the community have these estimates.

13. Mathlib as infrastructure: Formal Frontiers

There's one thing: some knowledge is more crystallized than others.

Well, for example, rings—you study them at university. So this crystallization process has been going on for hundreds of years. I would say they're high on the mountain of abstractions, so we can compress them as much as possible.

But there's also all these lines of discovery, just like in writing software. We refactor code because, at the beginning, we didn't really understand the domain abstractly enough, and now we do. So we refactor, distill, and compress.

Is it like Mathlib, where some parts have evolved a lot and some parts are quite adaptive, and we're still learning about them? How do you think about that?

Yeah, yeah, yeah, yeah. Both things happen. It's just like software. You're thinking in the right direction. There are things that people have thought about a lot and that are crystal clear, and there are things that are in a state of flux.

One cool feature that we want to have is a Mathlib initiative called Formal Frontiers. They want people to formalize everything with AI, filling in the gaps in Mathlib and allowing any high-level mathematical article to be formalized.

To give you a better idea, for software developers, this is the equivalent of developing an application. Today, people use hundreds of libraries, right, if they develop in Rust. But imagine that half of those libraries are missing, and you say, “Oh my God, now I have to spend time building the infrastructure to build my application.”

It feels like something that should take a month is stretched into years because you have to build all the infrastructure. It's the same with mathematics. If I try to formalize an article, people in the community will tell you whether it's possible, because if you're missing a lot of components, it becomes a huge task.

But if you have all the components, you only need to formalize your article, your contribution, not the base material. It's like when you have all the libraries—it's easy. You can just focus on your application. I don't need to build a JSON library. I don't need to build B-trees. I don't need to build all that infrastructure. You get the idea, right? That's what I mean.

14. Creativity, abstraction and nut-sniping

It's just like software. I have a theory that creativity is deep understanding. When you understand something deeply, you can develop that line.

There's a really interesting idea that language models can sometimes learn all these abstractions. I like to use an example from linguistics. They can parse sentences like an onion, even ones that we can't, and they explain them using concepts from graduate-school linguistics textbooks. It's similar in all areas. They know about rings.

But my theory is that even though they have the abstraction, in a sense they don't understand it, because the path that led to rings is like a big evolutionary tree. Understanding is knowing the difference between the possible and the impossible, counterfactuals, how things could be different, and so on.

If you start with something very distilled and don't understand how it came about, then it's hard to be creative. We see that language models start quite low on the mountain of abstraction. It's still a form of understanding, but it's a deep, concrete understanding. It's still quite fragmented. It's not very structured, but it has more degrees of freedom.

When you look at this proof from the new GPT model that disproves the unit-distance problem, you see a lot of verbosity. It just goes around and around. It does some pretty weird things.

Isn't it interesting that, from a creativity perspective, what we think is most important—these deep abstractions—may not be the way AI does creativity at all?

It's very hard to say. I think about it all the time. They surprise me in both directions. Sometimes they do amazing things.

There's a mistake there—not in the trusted part. It's a simple mistake at the top level that doesn't require trust. But even so, it's a very complex piece of software. I think very few developers, even experienced ones, understand this part. And they understood it perfectly. It was a perfect explanation, right on target. I was amazed. I said, “How can they understand so much about the internals?”

Yes?

I was amazed. But on the other hand, sometimes they make idiotic mistakes. I don't see the behavior changing. I keep moving to better models. They keep doing more and more amazing things, but they also do stupid things.

But we do stupid things too.

That's true, isn't it? So maybe they're really good at what we call “sniper proving” these days. For example, if you have a gap or a proposition that you want to prove, and you don't have to create a new theory but just combine existing elements, it seems like people can't keep up with them. They're much better.

You ask them to implement micro-optimizations for a piece of code, and they do it perfectly. But if you ask them to come up with a new way of doing something, they fail miserably.

I feel like maybe I'm not an expert in machine learning. Maybe you can tell me. One of my guesses is that these things are turned on, and they kind of wake up. After all the training, you show them a problem, and they go for it.

They've “read” all the literature in their training. They've seen all this stuff. They have a bias toward the existing solutions that people use. If you can solve a problem using a set of tricks from the literature, they'll do it. They'll do it brilliantly. But if you need a new trick, they seem to fall short.

Of course, in the future, AI agents may appear that are constantly updating their weights and learning. You tell me. Does that match your understanding?

15. Breadcrumbs, not learning: what AI agents lack

I'm not an expert. I'm as excited as you are, but here's the strange thing: they have a lot of intelligence, but they still need to be guided.

The best-case scenario is when you solve a specific problem and you can climb up to the solution, but ultimately you just need to specify a vector. I'll use the analogy of a flashlight shining into the embedding space.

So this flashlight has a beam. As an expert, you say, “Okay, this view is quite interesting. Here are some sample initial solutions, some tricks you can use, and a clear optimization goal.” In that case, the result is just amazing. But it still requires human taste and expertise.

I think they lack the ability to abstract. For example, it can even be good from a creative perspective, because the system finds its way through these low-level, concrete, fragmented representations and comes up with a solution. But after it adapts and finds its way, we need it to make sense of it in a meta-sense. It has to ask, “How can I compress this?”

Maybe I’m being unfair right now. Maybe, to some extent, systems do this, but when they have a memory system, it’s still a mess. It’s still the same human supervisor saying, “Okay, you’re doing this, but you need to optimize it. You need to—maybe if you think about it differently—boom.” If they could do that on their own, it would be incredible. Maybe they do it to some extent, but it’s very limited.

16. Competence without comprehension, and verified guardrails

I think you know a lot more than I do, but it seems to me that they wake up and leave crumbs for the next one. The next one wakes up, reads all the crumbs, and takes the next step. It’s not really memory; it’s just crumbs for the next one. They don’t change the way they perceive things in any significant way. It’s almost like there’s a limit to what you can do: you keep leaving crumbs for the next iteration to read and take the next action. But ultimately, that’s where humans really help, by guiding them in the right direction, right? So, I mean, does this fit in?

I feel like we can do this abstraction because we’re in this world and we could do things differently. We have subjectivity. To achieve goals, subject to the constraints that apply to us, we can try different things.

An example of this is if I hired a video editor. I’ve been developing my video-editing skills for 5 years, and I could say to the video editor, “Okay, I’m going to optimize your process because I’ve learned all these important lessons. Always use a tripod. Don’t even try to hold the camera in your hands, because you’ll have a lot of problems with that. Let’s just prevent this problem from happening before it even happens.”

I can impose a bunch of restrictions, and they will have competence without understanding. But they would always resist and say, “I want to try this, and I want to try that,” because they don’t know what these restrictions are for. I understand this because I understand the scope of possibilities, and I know why these limitations arose.

You learn from experience. Your experience has taught you this, and they are learning from your experience. They don’t conduct experiments themselves.

For example, SMT. You mentioned this tree. If you ask a question about implementing SMT on large language models, you will get exactly what is written in the textbooks. But the large language model never tries it. It repeats the knowledge of the people who wrote those works, doesn’t it?

That’s right. That’s exactly what you said. They repeat. They don’t try; they don’t experiment themselves.

Yeah, that part is definitely missing. But it looks like an area that can be enriched, so I don’t see any obstacles here. People will try it, right? They’ll try to improve large language models in this direction.

I’m convinced of this because competence without understanding isn’t necessarily a bad thing. We’re writing intelligent software now. We used to write software that just did exactly what it was supposed to do, and now there’s some flexibility. We impose certain constraints, and within those constraints, adaptation occurs. We can control it as an engineering task.

These restrictions are actually useful. There are certain things that we’ve figured out, and that’s why they’ve survived in our cultural lexicon: certain algorithms and certain ways of thinking. Frankly, it would be a waste of time to force AI to invent these things from scratch.

Yes, yes, yes.

Learning by doing gives you a new perspective, doesn’t it? Maybe AI can gain new perspectives by learning from its own experiences, rather than relying on what we did. Learning by doing on its own and perhaps updating its own weights is entirely possible.

Yes. Then maybe it’s just a matter of computation. Maybe we could have a society of agents that actually performed the weight adaptation.

But that would be quite difficult and, in some places, even dangerous. The advantage of large, powerful models that are trained every 6 months by the platform is that we can set up protective barriers, and at least there’s only 1 model to check.

That’s also something I’m interested in: to what extent should platform owners be held accountable versus individual engineers? If I create a complex agent system, it’s already gotten to the point where I don’t think anyone should put frontier-class models into production. Maybe during the development and research phase you need more intelligence, and then the engineers set the limits. It has to get to a point somewhere between a regular software application and an AI system, so maybe we’ll have a less intelligent model in production.

How responsible do you think engineers are for a kind of degenerative behavior?

The difference here is that you’re talking about a scenario where the application has AI built in, right? If you have that scenario, I think it’s extremely important to have protective barriers. Even better, if your barriers are tested using a system like Lean, you can prove the properties of those barriers. Some people are talking about creating formally verified sandboxes in the future.

In my mind, I always use AI to develop software that doesn’t contain AI. Lean doesn’t contain AI, right? This is a much safer scenario. Many people use it that way. They build applications, but the applications themselves don’t have AI built in. That’s a much safer scenario: you’re fighting bugs in the application, rather than putting barriers around the AI.

17. Is the human still the author?

If I make AI generate some Lean and then Lean proves it, is the human still the author? Will people play a significant role in this in 5 years?

It’s really hard to say, isn’t it? I couldn’t have predicted this a year ago. I couldn’t have predicted what’s happened so far, so I can’t even imagine what will happen in 5 years. Everything seems to be speeding up. This is moving much faster than we expected.

Sometimes people ask me, “Are you afraid of becoming useless?” I would feel relieved. For software development, it would feel like mission accomplished. I wouldn’t have to do it myself anymore. Maybe I could spend my time building programs that don’t necessarily have to work. It wouldn’t be the end of the world.

I hope so. One thing I think is that we’ll always be up to date, because we must always maintain specifications that say what the program should do. That will always be our responsibility. We’re the ones who benefit from AI. We’re the ones who say, “This is what we want.” We’ll be there somewhere nearby, even if it’s just at the level of specifications, formulating our desires.

Of course, people can create scenarios where AI is superintelligent. We have robots, we tell them what we want, they understand natural language, and they obey. They do exactly what we ask them to do. But we’re still the ones who tell them what to do, so I feel like there will always be a role for us in the future.

But I also see exciting possibilities. As a developer, most developers I know have a lot of ideas, but they implement only a small portion of them because time is limited. They simply don’t have time to implement all their ideas. Many of my colleagues choose the ones with the highest probability of success.

It’s like a game where you weigh effort against the chances of success. You reject many ideas because their chances of success are very small. But with AI, we can try more ideas, right?

I’ll give an example with him. He doesn’t program in the same sense as humans, but he gives AI different tasks to test ideas and sees which ones are worth spending time on. That’s a big win, right?

It makes me think, because it’s hard to predict the future when we’re just starting to understand the boundaries. But I think people have a deeper understanding. That means we have better intuition about interesting problems, and we’re better able to filter out the unnecessary.

Even with Mathlib, if in the future it becomes very easy to create theorems, the role of humans will be more about structuring and selection.

Yes, yes. I see Mathlib. In the near future, people will use AI to support proofs and to build new, boring proofs that no one is interested in. But they will still write the key ones by hand because they want them to be beautiful or to have a certain structure that’s convenient for learning and conveying ideas.

Creating a roadmap will also remain a human activity. What goes into Mathlib, what doesn’t, and how we define rings and other mathematical structures—all of this will be done by humans.

There’s a lot of research going on right now. For example, there was one interesting idea. I’ve seen people suggest this: let’s say I start building a whole mathematics library. What will happen? It may turn out to be garbage. But how do we control this process?

Yuri Manin is one of the main people behind these formal barriers. The idea is to have a way of controlling this: key theorems that are very simple to state but require a lot of mathematics to prove.

So, if an AI can construct a proof of such a key theorem, it is doing something worthwhile. One example is Fermat's Last Theorem. It can be written using only natural numbers. It's very simple, but it takes a lot of mathematics to prove.

You could say this is a milestone for AI. You can build your crazy library, but you have to reach a goal. You have to show me that you've made it this far. You can have many such milestones that are easy to formulate but very difficult to prove. If AI has managed to build a library that allows it to prove this, maybe it's worth taking the time to see what's there, right?

18. AlphaProof, LLMs and why certificates still matter

One of the long-standing debates in AI, I think, is pure connectionism versus neurosymbolism. I think we're now on the cusp of the era of neurosymbolism, and these agent systems are incredible. I think that's why AI works so well. But there are still people who believe that only connectionism is truly good.

To add a little context, we've long had a hunch that adding structure and constraints to neural networks makes them better. That was the premonition that Google had in 2024, when they won silver at the IMO using AlphaProof, which automatically formalized Lean code and generated those proofs in Lean.

There was a pretty interesting development last year, when they struck gold using—well, I don't even remember exactly whether it was an agent LLM or just a pure model, but it's interesting, right? These models are simply neural networks. They don't have any strict restrictions.

An example of this is the game of chess, where they're obviously getting better. They generate correct moves about 91% of the time, which, to be honest, considering it's just a kind of “spaghetti neural network,” is pretty impressive. But how do you see this situation developing further?

Do you think companies like Google will ever turn to Lean? Do you think we're moving toward a point where these models seem to learn certain limitations as they scale?

I think your question can be answered in 2 ways. The first is whether methods like AlphaProof, which use Monte Carlo tree search as a hybrid technology—perhaps even truly neurosymbolic—to prove theorems, are justified or not. The other is whether we even need verification.

I think the answer to the second question is yes. Even if we have a model that generates correct answers 99.99999% of the time, we still need a certificate. Here's an example of how huge proofs can be: the unit distance conjecture, which OpenAI disproved. Boris Alekseev provided a proof consisting of 1.2 million lines of Lean code—a formal proof. Nobody wants to check such a proof line by line, right?

It's great to have a certificate. I think having certificates that are machine-verified is great. It's like having moves. Whether you're playing with an AlphaZero architecture or using a large language model that says, “Boom, boom, boom,” those are moves, right? The only difference is how exactly you create these moves.

I think viewing mathematics as a game with moves is very valuable, and that's what's going to stay, right? AI will synthesize a formal proof as a sequence of moves, regardless of whether it is an LLM agent driven by a language model or a Monte Carlo tree search combined with some kind of neural network.

The question of whether this is justified is still open. The combination of GPT-5.6 and Claude Fable, I think, outperforms all these systems that use Monte Carlo tree search. But then we have to ask the question of value: what is cheaper?

I spoke to colleagues who are doing these experiments at a conference this week, and they said that it's unclear. Each step in these hybrid Monte Carlo tree search systems is much cheaper, but they take significantly more steps because those steps are simpler. A large language model is more expensive, but it gets results faster, right?

This is still a matter of debate. I can imagine that in the future, for some domains, this hybrid approach will work, and the language model will work. There are also scenarios where we improve hardware so much that it becomes so cheap that no one will bother with hybrid approaches anymore. Everyone will just use large language models or something like that. This issue remains the subject of heated debate as to whether it is worth it.

What is the future of Lean? I guess the first part of the question is: you've improved Lean 4 so much, right? Do you imagine what the next version will look like? Also, what do you think the legacy of Lean will be after you leave? After all, you created something that has become a real phenomenon. This will exist long after you are gone, and to some extent, it's just going to continue to evolve. How do you see this process?

There's still a lot of work ahead, right? One thing we want to improve significantly is Lean as a programming language. We want Lean to generate code that can compete with Rust, especially for programs that manipulate arrays. A lot of investment will be made in this, as well as in Lean as a platform for software verification.

It's one thing to verify a library; it's another to verify entire systems, right? This is much larger. We want to invest in this to ensure that Lean scales. We want to make sure we keep up with the growth of mathlib, but mathlib is developed by people.

To give you some context, mathlib has grown by 44% from 2025 to today, but compilation time has decreased by 10%. We're making Lean faster and faster, but now that AI is writing the mathematics, we have to take a step forward. The library can grow much faster than we can add improvements.

We will need AI to improve performance and keep up with library sizes. Scalability will become a big issue. How do we maintain a library with 100 million lines of code? These are open questions: scalability, Lean as a programming language and a platform for software verification, and increasing trust.

We want to have a verified compiler for the code you generate with Lean. People don't realize that the trusted Lean codebase, if you only want to prove theorems, is much smaller. You only care about the core. But if you're interested in programming, suppose you wrote a programming language, proved its properties, and generated an executable file. Should the trusted codebase include a compiler? It's much more than a core.

We want to verify this compiler. In the future, we want to have a compiler that has been verified, so you don't have to trust us that it is implemented correctly—not because we are evildoers, but because we make mistakes, like everyone else.

Reducing the trusted codebase will be our task from now on. We want to continue to reduce it. AI will become increasingly better at finding vulnerabilities and exploits, so we want to keep improving it. We want to make sure Lean is a platform for developing software and mathematics.

As for legacy, even if I die today, Lean will continue to exist. I think the Lean community is something incredible. The people there will be able to take care of everything. Even so, they don't need me. I always tried to help, but the project will continue even if I die.

In 2013, could you, even in your wildest dreams, have imagined that things would be like they are today?

No. Even in my wildest dreams, I couldn't have imagined that people like Terence Tao would use Lean and talk about it in presentations. I never imagined this. I thought we were building a platform for verifying critical systems and that the proofs would be done manually.

People say I'm lucky. Maybe that's true, because Lean becoming interactive turned out to be great for AI. A tree is a black box. AI really can't influence or direct a tree, but it can guide me, right?

I was really lucky. There are so many incredible people, like Jeremy, Mitchell, and Mario. I found him at some little-known conference. Sebastian Ullrich, Joachim Breitner—so many people came. Morrison, so many. All these people at Lean FRO, I mean, yeah. Old colleagues—it's just incredible.

Kevin Buzzard showed up. He got interested and started writing articles. I was probably the happiest person in the world.

19. How to start learning Lean

Yesterday I watched a video on Computerphile. There was a great guy there who used tactics for tautology. Was this the discovery or reduction of a tautology? Anyway, the point is that it was pretty scary.

There are a lot of training videos where people are doing everything at breakneck speed. They're doing one thing, then another. What would you advise people who feel overwhelmed by this initial shock when learning Lean?

First of all, I would advise developers to start using Lean as a programming language. Just write code and ignore proofs. Don't try to prove anything at the beginning. Start writing code, playing with it, executing it, and when you get used to the Lean syntax, move on to the next step. Start trying to prove simple properties of your code.

Another thing I advise everyone is to keep your AI agents close by. They know a lot about Lean. They know Lean better than I do.

I highly doubt that.

No, they can explain. They can explain extensions that they didn't even design themselves. Lean is an extensible system. They know about all the extensions and read the documentation. They will read the documentation. Very few users read the documentation. AI reads it and can explain it to you.

You can tell AI about your experiences, for example. “Software developer” is too general. If you're a developer who has used Haskell or Lisp, you'll find it much easier to learn Lean, because they're all functional programming languages.

Let's say you can tell an AI, “I'm a C# or Java developer.” Now AI adapts explanations specifically to your experience, and it teaches you Lean step by step very effectively.

If you open a video that seems awesome, with all these tactics that are like moves in a theorem-proving game, you can ask AI, “Explain this to me. Here is my original context. Tell me what I should know before I try to understand this example.” It's really good at it.

Leo, it was a pleasure and an honor to see you on our program. Thank you very much for joining us.

Thank you.