AIがコードを書く時代、誰が正しさを証明するのか

All right, so today we have a treat. We have Leo DeMura, VP and Distinguished Scientist in the Automated Reasoning Group at AWS. And more importantly, he is a creator of Lean, which can be found at lean-lang.org. Lean is both a programming language and a tier improver. And he is also the chief architect of the Lean Focus Research Organization. So with that long-winded introduction, Leo, welcome to the podcast. Thank you. Thank you. Very excited to be here. All right. So I guess the overarching thesis of this conversation is that we're in an era where generation has become easy, not necessarily cheap, as people who use thought code will attest, but easy. but easy. And so then one of the key challenges is verification. And so Lean is normally associated

as the go-to tool. In fact, it's going to be a tool, I think, that will increasingly be in the lips of many people in AI in the next year around the topic of formal verification. So I guess let's start here, Leah, just the basics. For someone, for a listener who's accustomed to code reviews, QA, and testing, what does formal verification add? Yeah, at least both a programming language and a proof assistant, right? You can, at the same time, write codes, but also state properties the code should have. You can state open conjectures in math, and you can provide proofs to these claims, right? But the proof is not informal. The proof is written in the Lean language, and more importantly, it's machine-checked. Lean is a big piece of code, but to trust a result, prove it with Lean,

you need to trust only the kernel. It's where the proof is being checked. There's lots of, like any other programming language, you have all the tooling, LSP server, IntelliSense, code generators, auto-completion, completion, all these features are available in Lean, but this is also important for the proof checking step. And we have more than one checker. You can, in Lean, proofing can do proof as data that can be manipulated, that can be transformed. You can export your proofs and check with different checkers. Some of these checkers are verified now. We have two verified checkers. The third is coming soon. But this ability to be able to have machine-checkable proofs, it helps to address the trust bottleneck, not just the trust bottleneck between humans, but also between humans and AI. For example, suppose that you want to synthesize a piece of code, you want to implement a piece of code that has specific properties.

In the past, you would implement the software. Maybe you would add some testing infrastructure to make sure these properties hold. Some property-based testing is very popular these days, right? And you would write the testing framework. Testing framework is very useful for finding bugs, right? But it's not useful for proving that there are no bugs. You may even have a separate team conduct the testing. Yes, yes. Now, with formal verification, you can start with the properties. You can, for example, write the properties down, ask the AI, implement a piece of code that satisfies these properties. And prove to me, you're going to implement the code and write a proof, a lean proof that will be machine-checked. And the AI now is fully capable of doing that. For example, a colleague and friend of mine, Kim Morrison, she did an experiment where she ported ZLIP to Lean.

This is a compression library. Now she has a property, a property that says that if you compress data and you decompress, you get the data back. There is no loss. The data was not corrupted. It's an important property. No matter the level of compression. Exactly. Exactly. Exactly. Great. The theorem says exactly that. One of the parameters of the theorem is... And so, Leo, for our listeners, she did this. She wrote this compression tool using Lean, and then Lean served as kind of the formal verification tool. So if I'm a developer and I do the same thing and I say, I'm going to use Lean to formally verify my software, but I'm going to write it in Rust first, So can Lean still help me? Yes, yes, it can in two different ways. The first way is using Aeneas. Aeneas is a tool that allows you to verify REST code using Lean.

Aeneas is used, for example, by the Syncrypt team at Microsoft. Syncrypt is the verification of the crypto library at Microsoft. They use Aeneas plus Lean to verify the crypto library. You can start by using Aeneas. Another possibility is to ask your AI, build a model of my codes in Lean. The AI will read your codes. No matter what language. Yes, no matter what language. I mean, if someone had told me this last year, I would say this is science fiction. And this has a name, at least in mathematics, they call it auto-formalization. Yes. So in mathematics, for our listeners, you might have a math paper, and it's a paper. So it's composed of words, mathematical symbols, theorems, lemmas, and so on and so forth. And then auto-formalization, which was, as Leo points out, was not a thing as recently as maybe a year ago, is now a thing.

Exactly, exactly. So, Leo, this step, you folks at Lean had nothing to do with. This just happened because the frontier models became capable of doing this. Exactly, exactly. From the Lean side, what changes for us? Scalability, right? I mean, now AI, for example, the mathematical library built by humans for Lean is called Mathlib. It has 2.5 million lines. Incredible. This is like, for our listeners, imagine every, this is not the case, But imagine almost all mathematical books and papers were translated in the way we described using auto-formalization into Lean, which means then you have access to all of them. Yes. But look at the speed now. The Lean proofs now that have been published, that's about 50 million lines. The math lead took 10 years written by humans to go from 0 to 2.5. And now there are people writing proofs that's AI writing the proof that's 50 million.

The Fermat's last theorem proof that was written by Anthropik AI is 13 million lines. In the case, as you point out, Leo, in the case of software, there's something equivalent going on for every programming language. Yes. There is now, the frontier models are now capable of translating whatever program you wrote in whatever programming language. into Lean, and then now you have the Lean infrastructure for verification. Exactly. But one important thing to keep in mind, when you create a model of your program in Lean, if you use AI, there's always, is this model, the question, the main question is, is this model faithful to your code? Some people now are using differential testing, right? they run the Lean model in the program and see if they compute the same thing, right, to find discrepancies. And people have been finding bugs. I mean, even the...

So what you're saying is you're still responsible for this. Yes, exactly. And I see it happening in an incremental way. For example, a few weeks ago, the Cloud Code main developer, Boris, He posted that video where he just asked Claude, oh, check Claude's code for bugs using Link. And Claude starts creating the models, found bugs, tried to prove properties, noticed that he could not prove the properties, found bugs, filed the PRs, and Boris merged them. Yeah, these were real bugs. And Boris said, I don't even know Link. Right, right. But this is, for bug finding, this works reasonably well. But for the next step, for you to say, yes, there are no bugs. Now you have to start looking at the model and saying, yes, this is an accurate model of my code. And I want to maintain them in sync. Maybe I will use the AI. I will prove properties. You can start using A&E if your code is in Rust.

You can try to use A&E to prove that it's a faithful model of your code. But we expect in the next few months and years, people will focus way more on the specifications, on the models, on the properties you want the software to have. Yes. In fact, this same phenomenon is happening in math most recently in this proof of the Navier-Stokes equation, right? So maybe the auto-formalization step of translating the actual statement of the problem may not have been as faithful or whatever. But then it turns out that, in fact, they did prove the result. It's just that, you know, you still needed humans to kind of catch this and make the subtle adjustments, right? Yes. This is an important point for Navier-Restokes because it's so important results. Before OpenAI even started directing their models, we had a curated by human statement of the Navier-Restokes problem.

The statement of the problem was already in Lean, has been curated by experts. There was no doubt about whether the statement of the problem was correct, formalized. There's some controversy in the results because OpenAI presented informal proof written in natural language and a formal proof written in Lean. The informal proof and the formal one, they mismatches the proofs. I think it's at the level of, are you assuming fourth or fifth derivative? Yes, yes, yes, correct. Which matters for mathematicians, but you can see how subtle the differences were, right? Let me give you a point. There's a tool that I think is important to tell your audience. There's a tool called Vosal Blueprints. Virtual Blueprint is a tool for if you want to present a Lean result mixing natural language with Lean you can use virtual blueprints It almost like literate programming

You can mix natural language LaTeX with Lean and align the two presentations. We are very confident that if the AI was using virtual blueprints, this mismatch would not have happened. I mean, uh-uh. This is a matter of improving the tooling. Another misconception people have They think a lean proof Is a static object It's not Like we factor code You can factor proofs You can simplify them There are groups, for example For the Fermat's last theorem Proofed by Antropic There are groups that already reduces the proof by half By the way, this is true for proofs written by humans too Yes, true But here, you get machine checked Yeah. Right? I mean, you're making, you find the proof, but Lean keeps saying, yes, it's still a proof. Right? You can manipulate, you can ask, the AI can help you navigate the proof. You can align the proof with an informal presentation

using Lean Blueprints. It's all possible, right? I mean, this is one thing that I see on social media people are missing. These formal proofs are not static objects, are objects that you can manipulate, you can simplify, You can probe, you can ask questions, you can interact with them. So I guess I want to just nail down this one point, which I think should be clear by now, but I just want to make sure the audience who may not be familiar with what we're talking about gets this point, which is this difference between formal verification and plain QA and testing. why should I bother with formal verification when I already have AI writing all these tests for me? And, you know, I'm using AI to generate a plethora of tests, edge cases. You know, I have maximum coverage, Leo. I don't need verification, right?

Yeah, yeah. Testing is great for showing the presence of bugs, but not their absence. Even if you try to write, use the AI to generate many test cases, your AI may not be as smart as the AI that will be used to find a vulnerability in your software. We should not, I think technologies, the technologies are not in conflict with each other. They complement each other. For example, one mistake I see many people doing, trying to prove something that may be buggy. No matter how many, the amount of resources you put, how many tokens you burn, you'll not be able to prove something that's not true. This way, testing is always a great way to start. It increases your confidence, your understanding, and then you prove now you're proving for any input. You're not proving like only for the tests I tried it to work it, but you're proving that for any possible input, your program works.

It's for all instead of for some And honestly I think software Engineering may be Behind other engineering disciplines I don't know, like aerospace or whatever So maybe they've had More rigorous discipline Around verification because After all, there's much more serious Consequences in these other fields Yes, great points I think this is just a case Now that we have more and more people writing code and code is easier to write. And it just happens that verification has had its image net moment, so to speak. I guess, Leah, the main thing that's happened, because you folks have been working on Lean for a while and Lean has been rock solid for a while. So the main transition is really this auto formalization, the capability of the frontier models to write Lean. Yes. And also connects to your previous comments.

You made the point, yeah, in some industries, people have used formal verification in the past. But why it was not popular if it was so good? Because it's too time-consuming to prove things by hand. And AI dramatically reduces the cost of verifying codes. And it gives you other benefits. After you have a formal proof, right, you can start asking the AI, I want you to change, optimize my codes, but you have to keep proving that it's correct. It's almost like the proofs are guardrails. Now the AI can try wild optimizations that you may not even understand exactly how they work, but you have a proof that saying, yes, it still computes the same thing. It's way more efficient, but it still computes the same thing. So based on what we've been discussing, it seems like the software engineering profession will now focus on not writing code, maybe not even verification, because verification, maybe you can also semi-automate based on what we've discussed.

It's really requirements, right? So describing what you want. So there's two buckets, I guess, Leo. So there's the requirement gap. So is there a difference between what you want and what you are able to write down? And I guess what some people call the model gap, which is really are the conditions around what you're testing representative of production. So in other words, maybe your testing scenarios are too idealized in some ways. And obviously, you alluded to this earlier. To some extent, you have to trust Leo and Tim, the Lean kernel, right? So as Lean becomes more popular and you rely on it, and by relying, I mean you're relying not only that Lean verified your code, but all the libraries that your code depended on, right?

So I guess those are three things. So there's a requirement, there's the model, and then there's the lean kernel. Well, we have multiple. You don't need to trust us that kernel is implemented by other teams. This part, I think we're addressing well. I mean, we even have a kernel arena now where we collect kernels. Yeah, and they compete against each other to see which one is the fastest, if they get it wrong, if they have a bug, they are penalized. and everybody can see it. It's called arena.linglang.org. You can see all of them. And all of them are open source? I think, pretty sure. I mean, I cannot say I don't use all of them. I use the main ones. The ones I use, they are all open source. Do you have to be written in Lean to be? No. No. Some of them are implemented in Rust. There is one implemented in C Sharp. There is another one implemented in Haskell. Believe it or not, there is one implemented in Peck. Tech is this language for typesetting program.

Math papers and papers in computer science, math, and so on. But Tech is a full-blown programming language. And a colleague of mine, Kim Morrison, implemented a checker, a kernel in Tech, just to show that you can implement it in many different programming languages. Oh, there's one in COBOL, for example, implementing one in Fortran. So then the education and training of a software engineer will change, right? Well, I think there will be way more focus on writing formal specifications, writing properties, the requirements is essential. Many times we don't even know exactly what the software is supposed to do, right? And by the way, Leo, so some of these applications are complex, right? So they interact with databases, distributed systems. Yes. and so on. So then, I mean, how do you exactly? You're not going to be able to nail down the requirements. Or maybe that's what distinguishes you.

In the past, the, what do you call it? The superstar programmers were the super coders, right? Maybe in the future, it will be the people with the ability to, okay, so these are complex. I'm going to use Kafka. I'm going to use Spark, right? Yeah, but the models will have imprecisions sometimes because people don't know exactly what they want. But look at the difference. Before people would write a doc, before they design a database, they would have documents explaining the design, the architecture, in natural language. Some people would use a Word document to write the specification of the data. Usually there's some sort of architectural diagram, right? Yes, exactly. Exactly. But then what happens? Now we have these informal documents. You have no way to check if the actual implementation matches these documents. Some human has to go over the code base and keep maintaining both in sync.

It's a pain. I mean, you change the documents, you have to check if the implementation still matches. All of us know that we have comments that are out of sync in our code. But if everything is formal, you are going to have tools that will check whether the documents, your design matches the implementation or not. This is a step forward, right? For sure, you are going to have documents that are imprecise. Your customer wants X. Your specification is X prime. But you want to keep polishing, refining. This is the ground truth now. And then as the thing interacts with the real world, you go back and refine it. Exactly. And refine it. But now your code is going to be, you're going to have a tool that says the code matches the new model. You refine it. You improve it. Right. It matches. For example, some people say, oh, the code has been verified. There's so many caveats. What does it mean to verify something? The properties you wrote are the ones you really want.

I mean, you're going to be, now this process where you keep polishing your properties, making them more precise. Some software you have, you're going to model, track models, you're going to have track models for people that try to unpack your system. So these descriptions, these requirement docs, I guess these PRDs become what you track in your source control system. Because basically, in many ways, Leo, you know, as you learn more, right, so you're constantly verifying each version. But it's almost going to be the case that each version, I'm just going to have the AI write it from scratch. Why do I have to save any of the previous code? Yes, yes. the crown jewels becomes this which ultimately is still going to be owned and maintained by humans right Exactly exactly With the systems of AI Yeah yeah yeah Yeah yeah yeah And tools like Lean right

Yes. But doesn't that mean you have to almost revamp the entire CS curriculum? No. Not completely, but... Completely, but it's going through a depth. I mean, I've seen many colleges and universities where formal verification is not even a required course. course. And the only one is more like a curiosity that people do not use in industry because it was too expensive until now. I think there will be the focus on formal verification will increase, but I think it's still valuable to learn low-level. I mean, there will always be people that learn low-level assembly code, that learn low-level languages, that learn how to write codes and check that we will be assisting designing systems at a very low level. This will continue to exist. But you're right. It will change, for sure. But in this world, Leo, you could be a very productive

and very much in-demand engineer without actually being proficient in coding. Yes, this is going to happen. Well, but it's some kind of writing, let's see, it's still coding. Writing formal models It gives you a coding. You're just working a higher level. Yes. By the way, I think you wrote this phrase, which I love, and maybe you can elaborate by what you mean if you did, in fact, write this phrase, which is the verified stack. Yes. What do you mean by the verified stack? The verified stack is about the rich host software stack. I mean, that's some pieces of code that is not a big concern if they are buggy or not. I mean, for example, a video game is a piece of software. If it is buggy, it's annoying to the users, but there's no crisis in the world if there is a bug there. The critical software stack is our operating systems, our compilers, the communication layer, TCP, IP.

This is what I mean by the software stack, and it would be great if you have models, specifications for all these components. We have experts writing them, discussing them, and we start to verify properly, making sure these specifications, the actual code matches these specifications. Some direction that I think is really worthwhile investing in the future. So, which is interesting. So, Leo, imagine you're a CTO of a big Fortune 500 company, right? And then I come to you as a vendor and I go, hey, Leo, you should trust our software because we are formally verified. Yes. So, what are some of the key questions you need to ask me in order to make sure that I'm not BSing you? show me the specifications, show me your specifications, the properties, what you have verified. Someone can formally verify that my property is just true.

It's basically saying there is no property. You are not making any claims. I think you're absolutely right that we should be aware of claims like my code is formally verified without explaining exactly which properties have been verified. What's the specification you verify is against? What proof checker kernel did you use? Exactly. That's important. Right, right, right. Which tool? Another one that should be important, the trusted code base. There are tools that have a large trusted code base in Lean and other proof assistants like Rock, Isabel. They just focus on the trusted code base should be really small, right? Yeah, yeah, yeah. And obviously, to the extent that you can convince me that your software has run in a similar setting, in other words, a realistic setting, maybe that adds to the meat behind the verification claim, right?

So what about, you know, we talk about software as if, you know, they're just static things, but now we have software called agents, right? And then we now are entering the world of long-running agents. So what does verification mean in the world of agents? It's just a great question. I think the first thing we want to put guardrails on these agents would be great to have reliable sandboxes. I mean, we have been seeing the last few weeks, many people claiming the agents are escaping the sandboxes. Part of the verified software stack. The sandbox, we want reliable sandboxes, right? good specifications for them, proofs that the implementation meets these specifications. We also want to be able to write policies about the agent's behavior. And we want to make sure the code that enforces these policies has been formally verified. Imagine you spend all the time

writing policies about what the agent can do or cannot do, and then there's a bug in the code that enforces the policies. price. But what if another agent is doing the formal verification? So there's layers of trust, right? Yes, yes. One possibility people consider is, can an agent exploit a flaw in the link kernel or a flaw in the runtime where the link kernel is running? These are valid questions and this is why we have multiple kernels because even the agent would have to find a flaw. It would It would try to trick you in believing it proves something. It is not. And this certificate, this proof, would have to be accepted by multiple kernels that have been implemented and verified. Independently. Yes, exactly. This is serious. I mean, these agents are extremely good at finding vulnerabilities.

So have you interacted with people who are using the things we just discussed, verification specifically for agents? Yes. AWS, we have AgentCore, Dogwoods, they are all using Lean now. Out of sites, I gave the example of the author. The author of all the cloud codes uses Lean to find bugs in cloud codes. We've seen more and more projects like that because one main problem with other verification and tools like Lean was this steep learning curve, right? You would have to learn Lean, write these models, It's too much effort to start. But with AI, it helps you to reduce the startup costs. You can see value almost immediately, like Boris, his video he posted, where he just asked Claude, try to verify Claude's quote using Lean. And he got value immediately. And now it's worth, I almost feel like whenever you get immediate value,

you start investing more time learning the technology. they'll say, oh, maybe I should write my formal properties about my code that they want them to hold. Oh, maybe I should learn how to read the link code. I don't want to write it, but I want to be able to read, to be able to tell whether the model, the AI agents created a model that's accurate, right? And I want to discuss with the agents whether the model is accurate or not. So Boris, for long-running agents, right? So potentially agents that are exploring, doing research, exploring, coordinating among themselves, maybe for days, right? So we discussed that one of the challenges, obviously, is just nailing down the requirements, right? I mean, how can you nail down the requirements for something like that where it's like a human being exploring all sorts of directions? Imagine a human being who has infinite resources, can travel all over the world and can do anything. Yes, yes. It's a big challenge, but the AI can help you start.

It can write the first model, and it's good to say, oh, that's how we formalize. And these agentic systems are complex systems, right? There are multiple pieces interacting with each other. There are protocols there, communication protocols between these different pieces. And you want to make sure these protocols are correct and accurate. But the AI agents will help you to get started with the model, the formal model. It's almost like it's going to give you the first drafts and you can keep iterating from there. Right. So it seems like ground zero for everything we've discussed right now are coding and math. And math, just over the last few weeks, you have fields medalists crying. You know, I mean, the whole field has just basically been disrupted in a big way. Yes. Right. My PhD is in math, so I used to be in that field. I wasn't very good. Well, maybe now I could be with infinite computing resources.

But, yeah, so in that case, it seems like the combination of Lean and MATLib especially makes MAT even more of a sweet spot than coding. Am I wrong? No, no. What MathLib gives you, MathLib was constructed by humans, by people that have strong math backgrounds. In Israel, the definitions there, you know they're precise. But they must have started years ago. So they had the foresight that, hey, we're laboring here in the coal mines in obscurity. No one appreciates what we're doing. But once we scale. Yes, when they started, I mean, the first, I think nobody expected AI would get this good. But in their minds, one win for the math community was when they realized that Lean helps them to work in big numbers. For example, in 2024, Terence Stahl has a project where he broke a project in smaller pieces.

He was like an architect, right? And then there's no way for him to verify everything, personally verify everything. There, instead of having AI agents, you have many humans filling the holes for him. Many people that he never met. Giving him the proofs, he doesn't have to check the proofs correctly. It's almost like humans filling holes in his big design. And people said, wow, this is great. I remember him telling me, I never imagined that he would be working for amateurs. He only works a professional mathematician. This goes back to what you said very early on, which is trust, right? Because in many ways, math, like most of science, is built on trust, right? So I'm a mathematician. I'm proving a theorem. I'm citing many, many other theorems from the past, maybe some from 50 years ago, which I personally don't know how to prove these theorems. I just trust that they're correct, right? Exactly. And this is what they done right With Matlab Exactly But at the time I remember Terry giving talks and saying well one day AI agents will be in the loop

They will be filling these holes. But I think none of us imagined it would come so quickly. Instantly, right? Yeah, yeah, yeah. A few months ago, this was nobody would be. Six months ago, if I had told any of the Lean developers, the lean math lead maintainers. Oh, we won't have AI that will be discapable. They would not believe. But now, because of auto-formalization, the ability of AI to translate math into lean, I think it's just going to continue, which begs the question, Leo, why can't I do this in theoretical physics? Well, there's a library called PhysLib for Lean, where they're formalizing physics. Well, now I believe they probably switch it to AI. I think everybody's moving to AI. I mean, even the Lean developers, we are now implementing Lean using AI. I mean, it was funny because it started like, oh, the AI is really good at finding bugs

and isolating the bugs for us. Oh, AI is really good at patching the libraries. Oh, AI is writing code. Oh, wow, it's writing code better than we do. So what's the timescale for physics to get disrupted as much as math? Theoretical physics. They had their first win. I mean, a few months ago, they found a bug in an important physics paper by trying to formalize the results. The challenge here is that in physics, we are creating models of the real world. Our models are always imprecise. They are models, I mean, of the real world. Well, they start out as theoretical, right? For example, string theory has never been proven experimentally. Yes. So you could still be in a field in theoretical physics where the experiments haven't happened yet, but still make progress and publish papers. And those people can get disrupted soon, right?

Yes, yes. They can write now very accurate mathematical models, right? I mean, using Lean. Yes, it's totally possible. And so since Navier Stokes and since OpenAI published a bunch of more results, have you personally heard from your mathematics friends? Hey, Lydia, what did you do to our field? No, there's lots of mixed feelings, right? That some of them are super excited, right? We're going to be able to attack problems beyond our imagination. that people concern us about what's going to happen. I mean, students, what's going to happen with me? I mean, like software development, it will, software development, we will have developers. The job will be different, but we will have the format, the same thing. Yeah, I mean, major disruption. People, some people are angry, some people are excited, some people are scared, but I hope we will get, it's going to be a good change.

So the question in my mind, I've been thinking about this, is in the past, set aside software engineering in math, right? You kind of knew who the best mathematicians are, right? So you just start talking to them and then they know much more than you, right? So they're quicker. They know much more than you. They can prove harder theorems than you. It's almost like raw IQ was nothing you can do. I mean, that's why I left the field, right? because basically I can't compete with these people, you know. But now, does that change who wins Fields' medals in the future, right? So maybe it's the person that's smart, but not off-the-chart smart, but has access to more compute. I don't know. So have you thought about – in software, I would imagine it's the same, right? Oh, yes, same. Same. If I have access to more compute than you, maybe I can get more – I'll definitely get more done than you. Yes, exactly, exactly.

Right? Yes, I do. But it's so true what you said. I mean, for me, I do one of my superpowers was to tolerate pain. I mean, developing software is painful. Yeah, yeah, yeah, yeah. Proving theorems is painful. Yes. Hey, I removed this pain. But yeah, I lost my super... My superpower is not as useful as it was in the past. But we will be able to move faster, right? We will be able to achieve more. I think this is good. I mean, you're right that the person, a person with a different skill set may be more valuable in the future or may be able to leverage, not say be more useful, but leverage the technology better. We will have issues about access to tokens, right? But we see that in science all the time. I mean, for example, the James Webb telescope. You have to get, you can write a proposal, you get access to the telescope.

It goes in like queue. I believe in the future, the same thing will be for math. I mean, you have a massive project that requires an insane amount of money, but you're going to write a proposal. Maybe it will be funded. We'll get access to this model that's extremely powerful. unless there's a breakthrough and the models get more efficient and you know kind of like in chess right so in chess i guess i haven't kept up with this maybe you'd know is there a difference leo between a chess program i can run on my laptop in a chess program that runs on the cluster does that give me an edge i'm not a big chess player but my perception it was just running a computer i read extremely good i mean and i hope you're right i mean uh will you have models that we run on our computers. But I believe here these stakes are so high that there will always be the supercomputer. It's like the James Webb telescope. We can buy a telescope that's really good

and have at home. But the James Webb is way better, but it's way more expensive. Which means if looking ahead to the future, if you attend one of these academic conferences like in math, the person who used to be popular was the smartest guy, the Fields Medalist, now it's the guy with the cluster. Well, I mean, I think there's always... Everyone wants to talk to the guy with the cluster. Well, maybe this guy is not even the guy that has the ideas. I mean, there's a committee probably that manages the James Webb Telescope, but scientists submit proposals all the time. I mean, and they get access. I mean, I think the same thing will happen in the future. So we talked about, we started at coding and then obviously math, we speculated on physics. So what other areas are you seeing that maybe is below the radar where this equivalent of Matlib or something like that is happening? I'm seeing many people interested in finance.

Finance has many algorithms. I mean, there are people interested in this area, right? But the algorithms are the stats. So in math, you have proofs. Theoretical physics, you have proofs. But algorithms, how does that work? There's a lot of math in finance. Yeah, yeah, I know. It's financial. Yeah, yeah, yeah. I'm seeing people excited about applying formal verification to this area, using more precise models. But that, Leo, the challenge there is they don't work in the open, right? So they're secretive. Yes, yes, yes. So how do you come up with MATLAB? Yeah, I've seen people that are open to the tracing algorithms. Probably they want to keep all secrets, right? But there is a math background for finance. People want to formalize and make it public, right? But you're right. There will be people keeping their secret sauce. So finance, what else? I see people trying to build libraries for chemistry, biology.

methodology. I think any field where... And what's the relative progress in each of the fields you named? Like, how far along are they? They are all, I think the finance, the one that's maybe, basically outputs math labs by far, super far ahead because math is precise. Then we have the physics library and we have the computer science library that are trying to catch up to math lab. Then we have these new initiatives in finance, chemistry. But if you get the papers in each area, you see how precise, how rigorous these papers are. The math in these papers will give us a hint on how hard it will be to create a formal library. Yeah, because there's theoretical and computational chemistry, right? Yes. But then, don't you think, Leo, because of auto-formalization, any community that decides to go in this direction will get there faster, right?

Because the Matlib people toiled in obscurity for years, but once auto-formalization happened, boom. Exactly. Yes. So are there non-scientific fields where you think this might happen? So, for example, let me draw out a couple of examples for you, but I don't think they will work, right? Accounting. I have generally accepted accounting principles. I have the tax code. The tax code and the GAAG are my theorems in many ways. But then here's the problem. I talked to some accountants about this. The problem is, here's some funds. Do I put that here or here or here? Right? So it's subjective. Yes, yes, yes. I saw people trying to do formal law. Oh, so yeah, yeah. I talked to someone about this too. But then the problem is with law, the reason we're suing each other is we disagree. Yes, exactly. But that part of the law, I had once heard that he was a lawyer.

He's a lawyer now. I mean, for example, civil procedures are very, very formulated. Yeah, almost like a program. Oh, really? Yeah, yeah. There are parts of the law that can be formalized, right? I see. Yeah, yeah, yeah. And with that, thank you, Leo. Thank you. Thank you very much. You can follow the work of Leo DeMura online at lean-lang.org. Please join the thousands of people who subscribe to our newsletter, which you can find at gradientflow.substack.com. And we are listener and reader supported. So if you can, please become a paid subscriber. Thanks for joining us. If you like the show, please subscribe and rate us through Apple Podcasts or Overcast or TuneIn.com or Spotify and never miss an episode. The Daily Exchange Podcast is a property of Grade & Flow. And I'll be back next week and we will do this all over again.