Lean 4 語言體驗心得與軟體的未來

Thank you. Thank you, Mick. Thanks, everyone. Uh thanks for having me here. Um so, I'm CC.

Hi. Used to be working uh EF building uh full stack prototypes and uh later GK applications. Uh it's like no better than anything that to describe what my past work was. I was the cloud core for EF. Um so, today we're [clears throat] going to talk about like yeah, like so, you know, when I realized like, "Okay, I'm the cloud core of EF."

Then I am I Ascension now? Like um and how do we like even do software programming in in a world like full of AI and and AI coding? So, um that's the story today. And I would like to like open this talk with a nice story uh in like 1950s. And then um it's a science fiction by Asimov in his famous like short story series I, Robot.

Uh I think the you know, like the date set in the story is like 2057 or something. Um it says like uh basically there were two uh company major companies that are building a spaceship uh for the hyperspace travel. Uh but uh think that two companies like Open AI and and and Anthropic. And then uh one company failed, but the other company they uh kind of successfully built uh some like computer called Bram and like Uh this is this is, you know, when Asimov wrote this this is before the time we had computer like you know like like Turing Turing Turing machine was like 1940 something and you know like 1950 like Taiwan was still don't [clears throat] ask. And um So the brand like the computer that it designs a uh spaceship spaceship like but there's some problems and the company sent two engineers to investigate it and they enter a space spacecraft and then they see no controls no beds no no toilet no nothing just nothing.

And then then the ship just set off. And then when I I read this story like we're we're kind of I feel like we're kind of living in that kind of world today like computer designs something like it could be a software today but like in the future it could be anything right? And then it's like computer handles all the designs and implementation and like no human was in the loop and it was involved and it's kind of scary but it's kind of like where we are and but like as we'll see in today's presentation like we have um some way to handle it. So while um So in this talk I'll mention like three things like first is my personal experience in like picking up Lean Lean programming language. And then we'll do some case studies, um, like formal verification today, how, uh, like I'll show you some cool projects people are currently building.

And then, uh, like what it means to be a theorem software in general. And I hope you like after this talk you can, uh, get a feeling like what doing math proving with code feels like and what is what is it relevant to software programming. So, here we go. Why the hype? Why everybody is talking about Lean right now?

Like what's happening? So, formal verification has been like has been there since forever. Like it's it's 60 years, uh, like kind of paradigm, but like I feel like very sorry for like like like Isabelle like Rock and like uh, communities like they've they've been here forever, but they didn't get the attention they deserved. But like like Lean they kind of took all the credits, like. But if you try both, like I think Lean has very like has better user experience if you actually try to prove things with them.

So, first like So, I think the whole narratives of using Lean like I I'll I'll boil it down like into like these three three stupid reasons. One is the threat, like you know, AI like needles, they can find bugs quickly, they can find like bugs hiding in a open source operating system in 26 years, and then and and just just burn the token and you find it. And then, uh, you can find it very quick today, you can find it They're quicker tomorrow. So, this is a threat we have to address. And second is the opportunity.

The formal verification is very very painful to to do and very difficult to write if you actually try it. But now you have very cheap labors of AI and then like you can dump formal verification in relatively cheaper cost. So, this is the opportunity. And third is the need. Like uh who here who here already like doing the software programming with 20 agents?

Okay. Really enter okay.

[laughter]

One here okay. I I I I don't really like I I I only have a like 20 USDs monthly subscription. Okay. But I like think about like okay if we want to do like 20 agents and then uh how much of the code and then how how much of them you can actually review it like you probably don't want to review them. So, that that is the need.

So, this is the three reason we are doing formal verification uh today. Let me pay attention to the time. Okay. Okay. So, what is Lean 4?

So, uh unfortunately like we we have lots of name collision in the space like Justin Drake is also building a Lean is a protocol but Lean we're talking about today is a programming language not a protocol. It's a proof assistant and programming language. That means like you can write math with Lean 4 language. You can also use it as a usual programming language too. And I think that uh that is why Lean 4 is so powerful because uh the other formal verification languages, they usually are built on top of other languages.

So, if you want to do some like fine-grained operations, you might need to do some C++ code, or you might need to do OCaml code. But, in Lean, like you just do everything in Lean. Like, you don't need to introduce other programming languages. So, that actually lower the barrier of entry a lot. And so, if if you write a proof with Lean, and then it when it compiles, then you can almost be sure like that the theorem is true.

Like, like you you just you just like like you just verified it. Um, so in Lean, like um it's it's it's kind of like a Coq video game. You you have a goal, and you have a toolbox of theorems and tactics. And then you choose your you choose your tactics and theorems to finish the goal. Uh, that's all you do.

And the Lean community builds a very great introductory game called natural number game. I highly recommend it. It's really fun to play, and it really gets you like up to speed. Like, you're if you're afraid of math, if you're afraid of coding, just just just play the game really slowly, and then with some help from AI, like you can get up to speed very quick. So, let's um let's show some examples.

Let's say like so, this is this is what math in your like this is what this is what math look like in your daily life. Uh, you see like we're we're typing this math with LaTeX. LaTeX. And and sometimes like you you write a math on a paper, you sometimes write a math on a whiteboard. But let's say we we we assume y equals to x + 37.

We assume this to be true. And your goal is to show that 2 * y equals 2 multiply x + 37. Like how what will you do? Like how do you solve this? Yeah, I get it.

Divide by two.

Divide by two. Yeah, you can divide by two and then you get a y equals to x + 37, which is exactly our assumption and then you you solve the goal, right? So, what I'm saying here is like we are treating the math like doing a proof as some kind of a set of operations, set of rewrite operations, or set of canceling, set of like applying theorems, and they are actually computation steps. And then um you can actually like write it into a program. So, we we here in Lean the hypothesis is something we assume to be true and then we will list it list them in the hypothesis and the goal is something we want to solve.

So, yep. It's the same thing but you're seeing different fonts. And then you'd use the rewrite tactic. So, RW means rewrite and then you rewrite the hypothesis. It will replace the symbol on the left-hand side with the symbol on the right-hand side.

So, this is a little bit different from the solution Alex proposed. So, we are actually replacing the Y with a X + 37. And then, you get the both side two times X + 37. And then, when when the equality of is reached, you you close the goal. Okay.

So, we can actually do a theorem proving with an example. So, we copy this. We'll prove this you know, like junior high school formula. Who who hasn't seen this before? Like A + B squared.

All right. Everyone has been to junior high school. Okay. And let's see. Let me make it really big.

And then, okay. So, Wait. First, we have to import math lib. So, math lib is very Yeah, we start file. Very cool because Oh, where is it?

Capital math lib. Yes, capital math lib. So, math lib is like it's a community effort to try to pack every known mathematical theorems in in inside just one packages. But, it's like super fat. Like every time you have to rebuild a math lib and it's very painful.

It takes a long time to build, but it has every formula you ever need. Okay. And then, now we have this custom like my add square theorem we want to prove. The left hand side is A plus b squared and the right hand side is the expansion a squared plus two times a b plus b squared. And here we have a sorry.

The sorry means like okay, we we haven't figured out how to prove this yet. We'll we'll add this thing to silence the the compiler error and then but the compiler will tell you okay, like like I won't tell you the detail about this but like you you have something you haven't proven. Don't forget to prove it later. And in the context of like formal verification, I call this sorry a formal apology.

[clears throat]

So here like um Okay, so how do you do this? Like okay, so here we actually see we have a goal here. So this is your goal we we don't have a hypothesis. Like I I don't have a hypothesis in this one. And we we want to reduce this goal into like something true.

So first we'll do like a b um So this is I kind of like uh the next step to introduce Okay, we're introducing variables into our like game board. So now we have a b they are natural numbers. Natural numbers are integers greater or equal to zero. And now we have to break down this this square part. So So um I really remember some formula uh from the math league.

So, a square. Okay. So, we write square we break down the square into like the same thing times itself. And now like we have to multiply this out. So, then we'll rewrite something called um uh I think this is add the mule.

So, there uh the math league has a system of naming things. Formula add, sorry. No, um Oh, I think it's uh it's building, sorry. Let me check my cheat sheet. Oh, mule add.

Yeah. Okay, maybe I'll just copy everything to just speed up this. Yes. So, the whole thing is this like um Okay, it takes some time to build, but uh the point here is like when we are trying to use a set of steps and to um to break down this formula, to break down the left-hand side and to the point it equals to the right-hand side. Uh Yes.

Does it apply to all the operators like only

Uh it applies to the right hand side, too. So, sometimes sometimes we have to do this and rewrite uh, to be specific like like where which part you want to rewrite. So, I think the lean forward is a type checking to check if any shape of the formula matches the match the theorem you want to apply. So, it it

Can we import though? Like is it possible to import individual operations? Not like the whole library, but

Oh, that's a good question.

import something, and will it speed up the viewer in that?

Um, so you So, you can you can import a particular name like mathlib tactics or something like usual algebra or something, but I I don't know if that improve improve the speed because in in a package side you still need to import the whole mathlib. There is no way to, you know, like I just want part of the mathlib like it just need everything like it's I I think that might sound like technical choice that that might not make sense in the usual software sense. And also it seems there there's no way you can lock the version of mathlib like it always loads the latest version of mathlib and then and live or yes, you you got the suffer for a lot of breaks. Yeah. So, okay.

That's that's that's how like proving things feels like. Like I I hope you get a sense like So, um, can I show you Okay, maybe maybe let me reload again. Uh, okay. Okay, let's let's give up this. Uh, anyway, like at the end you will see a goal cleared and then and that's very like dopamine feeding.

So, uh, my experience So, first I did a natural number game. So, like when you go to the website, it looks like this. It's like like Mario stages. Like there are different different worlds, different stages and about additions, some about multiplication. Uh, you have to prove things about natural number.

Like you you have to construct it from the the piano theorem or something. And then, uh, the inside [clears throat] world it looks like this. You have a uh, you have a goal here. You have objects and hypothesis here. You have a bunch of tactics in your toolbox.

Um And then and then you just apply them, execute them. Um And then you get uh, you clear stage, clear stages. So, this is my stages. Like why there is a blue one like like it's unfinished there? Why?

Because there is a stage and it plays uh, Fermat's Last Theorem there. Then I you you you probably need a PhD to to to actually finish that. I heard So, the sort of So, the stage description says like currently it needs like a billion a billion nights of code to to actually prove it. Like So, very scary. So, after natural number games and I also tried uh, lots of other other games that people are building new games there.

So, I want to actually prove a real paper. I actually want to try a real project because the reality can can hit you in a in a in a unexpected way. So, I chose the Arrows Impossibility Theorem. This is a very classic theorem in a economic textbook. It says you cannot design a perfect voting system satisfying like three very like minimum basic like sand idea and then um and there are people has been like over a year improving shortening the proofs.

So, I try to find um like the shortest paper I can find and eventually I took like three two three painful weeks to to actually finish it. The paper looks like this. This See, the proof part is like two pages left and right and then you know like 50% of it is a diagram like how hard could it be? And um I I I kind of like the first day I kind of have like two or three like statement like like three base criteria down and the final formula down but then the rest of the index the it took me like two weeks to fix it. So, here is my my diagram I asked Carl to analyze the comments and then the line of code is increased and then this is lines of stories.

So, so lines of stories means like yes.

How do you count the story count?

Just just count the lines. Oh, the lines of stories in in the code.

But you see them and you just

Yeah, just just add them. yeah, yeah. And then um because like like um when you're working on the formula, you you might like branch branching it like maybe you have four branches and then you have four stories there. You just put a technical debt there and then pay back later.

So, what's the stump you place or it's uh it's the compiler returning sorry to you?

Uh it it's it's it's uh you you write it in the code.

Oh, sorry.

Yeah, yeah, yeah. So, here like sorry goes to zero, this is uh second week and so this means that everything is proven. But there's a statement like um there's a like strong uh preference and a strict preference and weak preference and I didn't state it as the paper say. So, uh I took another week to actually address that problem and also like try to reduce the lines of proofs um to to the point that I I think it's like almost 1,000 lines of code and at the end like 300 lines of code. And there's a lot of struggles there.

[laughter]

And why did it so hard? Because uh you need to uh reasoning about types. Like like Lean is kind of the you know type checking on steer steroids story. Like is that American thing? And and like if you ever ever done Rust like I if Rust feels painful to write, like Lean is like kind of 10 times more painful to write.

And you have to you know do a lot of like plus one negative one like corrosion like like uh something very mathematically trivial, you have to uh do a lot of corrosion in in um in in Lean. And the craziest part is like the paper has this line like, which can be easily extended to other things. And then that line like, it takes 16 branches and then

[clears throat]

like and and also like I think the final version like, if you pick the right variable to branch about, like you can reduce it to like seven branches, but like it's it's maybe it's easily extended to other cases, but like it's very very tedious. So, okay. So, we we we talk about like proving math. And then like how can we use this to prove like program? Like I think this is more relevant to you as a software developer.

So, imagine like we have a Python function here. We want to add number A and number B and return the the sum of them. So, so first you want to do maybe you want you might want to add some test. Testing is the current like paradigm of doing things. You try some numbers, you try two numbers and you make sure they work.

But then boom, like someone just passing a string and then like 1 + 2 become 12 and not three. So it kind of comes up with Thank you. Like 20 roughly like 10 years ago, like type checking become some kind of mainstream. So, you you have to label like A is an integer, B is an integer. If you add two strings together, compiler would complain about it.

So so that's how like uh how how we're doing software today like just type checking and testing. But what can So Lean has like type checking already built in. Uh you have to specify A and B are natural numbers. And then this add function So it it looks exactly almost the same as the Python Python function. And then you can you can also do some kind of test cases like like with this evaluations.

And then you get the a result of addition. But what's more Uh and also you get a type checking. If you try to pass the string here, uh they will complain about it. But here is the powerful part. You can add a theorem and prove that for every natural numbers, it always add up.

You always add up. Like like how many test cases do you need for for giving this claim? Like this is like every night there are infinite natural numbers, right? And then So So here what we're here is like we just unfold the definition of add method, and then you get the A plus B on the left hand side, A plus B on the right hand side, and you said, "Okay, the left hand side equals to right hand side." And this theorem is proven.

Correct. Like by construction. So So this is how we kind of we can prove a program is correct. Uh there are more horrible things like I I didn't introduce here like like um like core logic or something like that. There are more advanced things in uh but uh like there there save it for future.

Okay. So here uh we finally can talk about some cool case studies. So, the first uh first case is LeanZip. This is how if you want to build like uh 20 agents and like uh using like, you know, like holding in Lean and then uh proving the software is correct. Like this is the case study you should uh dive into.

So, uh LeanZip is a Lean implementation of a compression library. Uh originally it was written in C, but uh this uh the author came. Uh he they kind of uh used AI to re-implement it into uh Lean 4 version and added a theorem to prove its correctness. Uh so, in in uh compression library, I think the biggest threat is the zip bomb. So, if you There's a zip bomb is something like let's say you receive a RAR or zip file um on an email and you just unzip it on your computer and then your computer just crashed, hanging there, freeze.

Because like it kind of unzipped unlimited amount of data and then kind of uh like crash your your your your storage. So, so here like uh what the guarantee we want is actually if you have something you have you have a data that is less than this max output. So, this is 1 GB. If you get a raw data and you deflate it, compress it, and then decompress it, it always go back to the same data. Like like this one uh like like there's no chance for zip bomb.

And you know, in the zip library, there there are many different kind of compression algorithms. And this proof So, this theorem will have proof delegated to other other proof for for each individual algorithms. And so, this is um Okay, one very powerful part about like software coding. Like I did I forgot to mention is that proofs are composable. Like if you if you prove A component is safe and B component is safe, you can combine these two proofs in a third proof.

You can reuse the proof, but you cannot reuse the test cases. Like uh proof can you can composite. And then so so the whole software is kind of like rely on this main theorem to to make sure like everything under 1 GB will be compressed safely. And but like Okay, we have to be skeptical like like claims like this. Like okay, then does that means the the software is bug free?

Someone actually like very skeptical and and actually took the challenge and and tried to find more bugs. They did find no memory vulnerabilities, but they actually find bugs in uh links run time and also like some some other parts in the software didn't protected by the proofs. So, actually like like you know, like bugs just relocates to to other places. Like like to uh they they they didn't disappear. Like they just um moved.

Okay, [snorts] so now like uh second case study like this if you are doing like GK circuits like this is very exciting like um So this is by GK security team like so you know like if you did circom and you have a is zero circuit that if you have an input if it's zero then it gives one and if it's not zero it gives zero. And circom follows like this is very every variable here is like finite field elements and it's very error prone like like like one mistake here can like cause you lost million of dollars. Um but in um in lean like you can you can express the circom circuit like this but this is not a powerful part. The powerful part is um So the man is the the man function here is your man algorithm. And then you put them into this circuit object but here you have to first you have a spec here.

This spec tells you what this uh what this uh function this algorithm actually do like this you know like um this algorithm is about like testing if an input is zero but if you see the content of the algorithm you cannot see that kind of statement. But this is the guarantee you you the result you want the algorithm to perform. And then you have to attach two proofs soundness proof and completeness proof so that you you make sure like every possible um every possible inputs and outputs like they will not break soundness and completeness. So, I I just expand the the dot dot dot with with the actual proof like that that looks like this that content is not important but like it it's kind of you feel like like okay, this circuit security problem is solved. It's solved like you you can actually prove your your right uh secure like correct circuit like bug-free.

All right. And also okay, this is the other exciting part like um some kind sometimes your circuit security depends on which field like which field element you're using. So, the how So, some something sometimes your security depends on a big field. And and this this usually when you audit the circuit like this is always forgotten. But in um in in in a clean project you need to uh you need to satisfy the property like like um given a given a size of the field element you need to uh prove the soundness and completeness for it.

So, uh questions so far? Okay. Yes.

Um Uh I I just want to ask a question that that might sound a bit naive. Um there are many real world cases where uh the process of a uh a a a a proved mathematical theory that is that is safe, but when we translate into the programming language um there will be some um necessary trade-off to implement that system. So, the question will be uh suppose that uh we we have built a system and uh want to write a formal verification of it by Lean. How can we ensure that that formal verification is uh is equal to this system?

Oh, that's a that's a very good question and I So, so I got a partial answer to this. So, uh So, first like Lean is not a performance language. So, you you don't actually use Lean in production. So, So, actually in production you need to write some optimized code. Um And so, one option is you can use uh you can compile Lean into C code and then you run the C code and assume it it it is secure.

And and then then then then um the second is you you kind of write a Rust code like for for performance and then you kind of prove that your Lean code actually matches your uh like status uh like they they are equivalent to your Rust code, but I haven't seen like like uh I I think that project exists, but I haven't checked about it.

Okay, so um um another question is that uh uh so the the compiled version of Lean code will be will be sent out C or Rust.

Uh you you can Yeah, you can kind of compile it to C. Uh I don't think you can compile it to Rust yet.

Okay, okay, I see. So, um in just for some kind of theoretically

Yes.

Lean will uh you you can you can make a um maybe um go Ethereum by Lean.

Um I think so. Like yeah. But uh so so I I I try to search like like is Lean like is Lean slow because like it's a you know, early language or like there are fundamental reason like it it is slow. And I heard there are fundamental reasons like there are like everything in Lean is boxed. Like so the box is kind of like kind of make it memory safe.

Uh like you use a lot of uh memory like it's not not efficient. So So yeah, maybe you can write a your Lean version of Ethereum go Ethereum. But like uh it it its performance will not be good. And but maybe you you can verify like you you can use it to verify the go version of of go client. That's my speculation.

Cool, cool. Thank you.

All right. So, case study three. Uh um

[snorts]

So, this uh this one is even cooler. Like this this is also a um See uh GK security project. But uh let's have a quick recap of what is EVM. So, in EVM code you can see um there are a lot of opcodes and which uh each of them have some like gas price. And my the story is when you write Solidity, everything compiles to EVM code.

When Alice sends Bob USDC like behind the scenes it's EVM code execution. And every execution client like implements EVM. So if EVM has a bug like like it will kind of hit everything. So that's why we need multi clients. Like if one client failed, the other will cover it.

And it this is Go Ethereum code. Like this is how you usually implement EVM. You implement in a high-level language. When we say high-level language it it looks like this. It looks it looks a little messy but like this is still for human.

Like it looks like English. And this is how people do programming today. Like you write you try to speak English so logically and then computer can understand. Like or you can build a compiler with translate this language to computer and then and you can you know come convince the silicon to work. But the computer like natively they they listen to like low-level languages like opcodes, assemblies or something like that.

Um So you know like like so so writing EVM in Go is kind of today but tomorrow we like maybe we talked about this like many years ago but like we wanted to do ZK proofs. And ZK proofs we want to compile EVM execution as RISC-V VM executions. And then you use a ZK VM to run this EVM execution. And and prove everything in ZK proofs. Um but uh there's a problem like when you compile EVM code to uh RISC-V traces, like can you trust the compiler?

Can you trust the compiled trace? Uh they are not they are actually not verified. And there are also some performance issues. Uh the compiled code usually like kind of uh bloated. They are not the most efficient uh version.

So, this EVM assembly project is uh kind of implement uh just 52 EVM opcodes uh in uh RISC-V opcodes. So, it looks like this. Like this is messy. Like this is this is not for humans. This is like uh RISC-V opcodes.

Like um This is the theoretically most efficient version you can get out of a machine, but it's um it's also not so readable for humans. Uh we don't do this um now because uh human need to reason the code. Like if you do this today and you want human to read it, it's very error-prone. It it's very easy to make mistake. But, if you prove it with math, if you you can provide theorem to prove that for every possible number like 256 bits A to this is B and then this always gets the uh the sum of them, then like it's okay to be messy here, but like you you can just prove all of the result is correct.

So, you get the correctness and also efficiency and both. And then So, uh that's kind of uh the you know, like uh Yoichi wrote it he he wrote it a post called as the final form of software. Like like like there's a very crazy title and very crazy claim. And like it but it it it looks like it it's a very cool concept. Um Um so, yeah.

Uh Sorry. Yeah, so so yeah. So, okay, we we review like three projects and and then like uh like uh we we see like how like uh mathematical proving can gives you like what what can you like, you know, um get the cost, the efficiency, and security from from the math proofs. And then you can delegate uh things to AI. And then like what's the role for human?

Like what what what do you actually do? And So, this is a paper from our uh Japanese friend Bonnie, and he he he he uh he kind of devised an algorithm and then to um so, you know, like in in Lean Coq, you have theorem depends on other theorems. You have a graph of theorems. But with the graph of theorems, how many of them needs actual human review? Because most of them are actually like uh type They can They can be checked with type checking.

But if they are definitions or theorem statements, they need to be um reviewed by humans. And for like, you know, proof-heavy libraries, like 95% to 99% of proofs needs no human review. Which uh means you'll only review 1% to 5%. And that means uh your review time can, you know, like scale 20 times, right? Or 100 times.

Depends how how much less code you need to review. And so, this is kind of uh au- automatic, like uh you you just ask AI to write everything and write the proofs to guarantee the correctness, and you just review the one person of the mass code. And then And then that's a productivity boost. Um And then the back where we locate they will relocate to specs. They will be relocated to a supply chance.

Just a company base. They they will go to a link library. They will go to any composition boundaries. Um but it is easier said than done. Like I it's actually very painful.

Like but think about like like one year from now, half years from now. Like the and and yeah, like Vitalik wrote it in article like like like yesterday, two days ago. Um and and he said like like the software is actually like it's not not not like crazy. It's not as pessimistic as what people say. It comes like um the the security is actually improving year by year and uh formal formal verification is just one of your tool you can add to your toolbox.

And the most important is thing is like how do you match your intent with the you know the implementation and the code you're writing. You're actually making a wish to a monkey paw, right? And so so you just use type checking and so testing and formal verification. It's just multiple tools to make sure your intent match your implementation. And yeah, and also like I think I I like one sentence.

Like like he said like when we talk about formal verification we use a lot of code like correct, secure, and like you know like correct by construction proofs. Like that. Those like three demos kind of marketing terms that they all they they they have a lot of like asterisks on on on top of them like they are not They are correct in the very scoped uh situation. So, yeah. Uh Yeah, let me close I like so eventually the the the spaceship in the Asimov story returns Earth safely and well, Asimov's um brilliance in uh robotic story is that like before Asimov, people write robotic story at by treating robot robots like Frankenstein's monster and like robot just hurts people.

But Asimov like turned it into like uh robot actually follow some rules and uh and actually actually like um they kind of protected uh protect people. Like the argument is that when you devise a tool and you want to use it, you must devise some protection and to use that kind of tool. And so, I think the link here like formal verification tool is kind of when we need to scale our uh coding production to like 20 agents, we need this kind of protection to to make the scaling safe. So, yeah, thank you so much.

Yeah, could you please show us slides 53 and 54 again because

It's like there is something important and you skipped them very fast.

[laughter]

Yes.

Now, I skip it really fast because they are nice lumps.

And actually, I have a question maybe related to this slide, but just in general. Um how can I, as a like a stupid human,

Yes.

make uh such a mistake

Yeah.

while writing Lean that will make me think that I'm actually proving something but that is just incorrect, you know? Like I I I wrote something, it it says, "Yeah, like you have like solved it." But in fact, it is incorrect. Do you have any examples, maybe?

Yeah. Uh so um I don't have a coding example, but usually it's a uh misstatement in your uh in your theorem statements. So So, for example, in my uh Arrows' impossibility theorem, although it's kind of a useless theorem, like you cannot use it in real life or something, but uh there's a preference, like like it it models like people's preference, and then uh if you have like strict preference, uh you only uh limit people to have strict preference. It It kind of uh makes the theorem less useful, but if you have weak preference, like it makes the theorem more uh more more kind of useful. And And I think if uh but in in maybe in the context of software um security, maybe or maybe let's say the uh this uh the the the the the zip one, okay.

So, here, like this theorem needs to cover every uh compression algorithms you have. If you one, that one is unprotected. And then I think that is something like you you might miss in practice. Like if you have 20 algorithms, but you only protected 19 of them.

Okay. I have another question.

One more question. Uh from your experience, are like mainstream LLMs good enough to write lean just by your prompt?

Oh, uh how? That's a very good question. So, I I So, so during my most of the work, I I sent a pull request to, you know, the VCBIO or another uh lean library. And uh I used Cloud Code uh with Sonnet. Like it is a like mid uh you know, like mid-level model.

It's not the smartest one out there. And uh it does decent work. Like it it sometimes it gets stuck, and sometimes it uh Yeah, sometimes it think very it take a long time to think or maybe I but I I can't actually tell if it's stuck or maybe it's just reasoning, but I I I didn't like I didn't know, but like um but I haven't used a like local LLM. Like I heard but Alex said like uh there's a lean lean straw, like it's a local LLM. It good do decent work, but uh I think it's it's not yet like for complex work, it's not, you know, like one shot you can one shot it with a prompt, you know.

Thank you. Um so in previous pages

Yes.

like the lean LLMs report.

Uh yes.

Um 90 something percentage.

I guess.

mean no human review. Does that mean um the current LLM LLM models are strong enough so they produce like upgrade.

So this is uh this is not about LLM. This is uh because um when you when you let's say you have a A theorem and it consumes B theorem.

Yeah.

And then um like if it B theorem is only used in the proof uh is only used in A theorem's proof. So you don't actually have to check B theorem. Because uh the link type check will handles the proving process.

Oh, okay.

So uh this is not like the This is not about the capability of uh LLM. This is about like type check how how much can you trust the type checking and the math library.

Oh, got it. So is it just because of the composition? Like you don't need to check something that is already have been proven valid and if something is made out of that, this is the reason why you don't need to check the the result. Or

Uh if it's it can be covered in type checking. All right, maybe let's say you have a A theorem depends on B theorem then depend on C theorem. Maybe you need to check the statement of A and statement of C. But the B in the middle it's like purely depends on C and purely depends on A. You don't You don't really need to You don't care about what B actually written because it's type checked by Lean's compiler.

It's It's like It's like like something something in the middle. You don't Like if it's wrong, the compiler will report like there's an error. Yeah.

Oh, thank you for your talk and uh think

I

Can you don't want to say anything?

This is just like the timing soundness and completeness You will really just think the things are uh Just you just don't want to learn them.

Yeah, you got it. You got it. You got it. You got it. You got it.

You got it. So So I get the question is about like uh proving soundness and completeness might not as easy as it seems. Like This is just two lines of second code. And it becomes like this is like 10 15 lines of Lean proof. So and of course you can compose different proofs together, but I imagine like usually um this would like blow up really fast.

But um But the cool thing is about like that learn the term called like proof engineering. Like how do you, you know, write very efficient proofs? Like like you can actually like if you write a you if you find the right abstractions, right abstractions of code right abstraction in math, and then you can turn a very messy proofs into a very clean and short proofs. So, I think like Like it's it's very interesting. Like if you turn the whole mathematics into a library, you will find like maybe lots of abstractions in math textbook it might not be the most efficient abstractions.

For example, like in after algebra we learn about like groups, rings, and fields. But in math maybe most of time you will see like add calm group like that. This like group with addition and like commune commutative rules like Like so so okay, so answering your question like it could get messy if you want to prove it and it could take a lot of time. But if you find a good abstraction of proof, you can also reduce the size of a proof.

And as you mentioned in the paper

Yes.

You need your fasting searching something. Hey, then I see someone has find out hey, wait there is a C++ problem, not this problem.

Oh, yeah. Yeah. Yeah. Yeah. Yeah.

You mean the this one?

Yes. Fasting searching.

Yeah. See uh

C++ Yeah.

So, if we need change his kernel to uh Lean self, so it will not be happen anymore.

Um it Okay, so let's talk about Lean trust kernel and you you will get you will not get a this trouble from other languages like C++ and something else.

Uh sorry, I I didn't understand.

I did Is it the implement the the the kernel maybe you Okay. You will Okay, let me show you Mhm. I ran now Lean kernel right now. This one. Yeah, so uh So, the the one you mentioned like 5,000 line is the I think it's a rust kernel like Nanoda this one.

So, uh the type checking like uh So, in Lean like there's a very uh core piece of uh software called

And all of the type checking correctness depends on the kernel. If kernel fails, then your type checking might fail and some bugs might leak through.

Thank you. And so uh so solve this problem like this is like exactly like if you have multi-client structure like there are multiple implementation of lean kernel in different languages. So if one one kernel has problem like it will be detected by the the other kernels. And there are actually one instance detected by this uh nano nano down. Yeah, so the question I just want to supply something else.

So so you just mentioned that if we all newbies can use LLNS to assist in our lean for coding and you can check Terence Tao Tao Zhexuan's blog post and there is a project called what's that? The E equation of theories project is all open on GitHub and a lot of the contributions there being done by top level LLNS. So it's doable and the people there they they all credited their contributions as assisted by LLNS written by hand or etc. etc. And it's a very good learning learning ground for you to try to give yourself give yourself hands on good taste of lean for projects and by by that I recommend using top level although is a bit expensive $100 US dollar like GPT 5.

5 Pro thing. It's been proven on Twitter you just search for hashtag I can write very good or be a very good assist in for our verification projects. Yeah.

And read the the keywords again.

Uh the the the project? E-

equation of theories project. Yeah, you might want to check the yeah, the GitHub.

Maybe I missed it, but is there any kind of tool or like a language where you write something let's let's say you're you're writing a program and at the same time you prove that it is like I mean it's it's formally verified and it compiles to your target. Like I don't know whatever like maybe EVM or normal computer assembly or something like that.

So you mean like writing proving and then compile your result to Yeah, yeah, yeah. So so that's So the only thing I heard is the C code thing. You can you can compile it to C language and then C language do that stuff, but I haven't verified this like I haven't tried it like it's It's like everybody tell you this, but like

So just follow up the question. So if the link for is compiled to C, do we have to trust the compiler in C? Thanks.

Yes.

Uh you say the Lean 4 is a type checker, kind of verifier, so for programming. Yes, we try to verify a computational process is correct. And if we are doing a real math proof, we are trying to reduce the compile error until it becomes zero, and so the theorem can become a really formal one when we trying to write the math proof inside the Lean. This is kind of this process. Or Uh I mean I mean if we we want to write a new math proof, and so when we have some some goal, and we write down its formal representation and in a symbolic way, but actually we don't know the claim from A to B is correct or not, so the Lean can tell us uh now we have something is not verified, and so we will try to uh do one by one, or if the gap is very big, how can we do the uh this kind of process one by one?

How can the assistant tell us about this?

Okay, so Uh so so for for right now, like Lean will not tell you like how far you need to go from uh to make your proof from math proof to being proved. But uh I think that is where I'm coming to help you finish that proof, then just tell you, okay, this claim is not proved yet. It it's like usually like you you might have some stories in in the theorem. Does that answer your question?

I mean uh some of the formal math theory will have some scope. Uh we have premise first, precondition first, and so we can know the type we want to compute this correct or not, or we rephrase this process to become the final final final symbolic representation we want. But uh if we if lots of uh type uh I mean if some of the type cannot be represent properly in some field, and we want to write a new one, or we want to approach it, can uh so we need to do from from goal and backward, or from uh some known theorem and try to proceed to our goal. I mean uh if we write in a new thing, which direction is more uh uh which direction is more easier way you think to do such thing?

Uh I think it depends on it it's case-by-case. Like sometimes it's easier to, you know, like go back from your end goals and prove backwards, and sometimes it's easier to, you know, back from your you know, like maybe in types and then and reach to the goal. And you can also do both. Uh usually like you probably want to start your project with uh your goal and lots of intermediate goals and then just just don't prove them yet. Just just say sorry and then I think it's it's similar to what what you do software programming now.

Like you you you probably need to design lot of uh functions or like uh uh let's let's [clears throat] not say UML but like like lots of different classes and then you do kind of interfaces and then you implement that interfaces. And I think proof engineering is kind of similar. Like you you want to have uh lots of different interfaces that would make the later proof easier and then you tackle those you distribute the work of the proof application of intermediate steps to other people, other agents. I think I think it's the last