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

Leonardo de Moura (0:00)

This proof, I think, was a disproof. The Collatz conjecture was submitted with a lean proof.

And the claim is it's accepted by the official kernel that comes with a lean. Wow, I mean, this is horrible. We strongly believe it was built by AI, exploits one bug in the official kernel, and this completely different bug in Nanoda. 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 Alexeyev submits a proof to his 1.2 million lines of Ling, the formal proof. Nobody wants to check the proof line by line. I'm Leo de Moura. I'm the creator of Ling, chief architect and co-founder of the Ling Throw, a non-profit behind Ling and also senior principal scientist at AWS.

Tim Scarfe (0:59)

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 a lot of creativity sometimes happens in the community. So there's different levels of adaptation. So there's the core thing. 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 Mathlib, 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?

Leonardo de Moura (1:40)

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

Now, I don't control the core system anymore. I mean, we have the fraud, there's a non-profit. We have 20 people there. Each one of them are owning. I like this model. The developers in the core, they own parts of the system, it's their responsibility, they have ownership. If they're going to take external pull requests or not, they are the decision makers. But for the first 10 years, basically, I own a bunch of the system, Sebastian Udig, my colleague and friends, that we built Lean for together. He owns other parts of the system. But we believe, I strongly believe in the cathedral model for open source. Cathedral is like, there's a central entity that decides what goes into the code base or not. This is a 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, in many cases, the potential building library for binary trees is self-contained.

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, it depends on each other. Another thing like a library, a binary tree library may be missing some functions, may be missing some theorems about the dysfunctions, 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. It creates tensions. But one cool thing about that is that I made Lean Extensible to enable people to add their own extensions without changing the core. This became really popular with the community. I mean, many people implement should they extensions, should lean without coordinating.

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, hides all the complexity. This can be done without even talking to us. Sometimes they demo things to me. They never met me before. They implemented this beautiful extension.

I think it's great. It was also my side effects.

Tim Scarfe (4:55)

Can you give me an example of that?

When solving abstract problems, sometimes there are ingenious and creative approaches. Do some of those really surprise you when you just see what people do?

Leonardo de Moura (5:10)

Yes.

I remember last year, Ilya Sergei is a professor in Singapore. He was with his student, Vova, and they demoed something to me. I said, why these folks are demoing this stuff? This is not lean. It was really cool, the demo. At the end, they said, no, this is lean. This is an extension we implemented on top of lean. I was really surprised. It was for software verification. We 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.