Episode 382 - Kevin Lacker on AI-Assisted Theorem Proving and Acorn

Transcript

[Music] Welcome to Zero Knowledge. I'm your host, Anna Rose. In this podcast, we will be exploring the latest in zero knowledge research and the decentralized web, as well as new paradigms that promise to change the way we interact and transact online. [Music] This week, Gar and I speak with Kevin Lacker, the creator of the Acorn theorem prover. The idea for this episode came about because of a discussion in our community. People were asking, since mathematical proofs are verifiable, could they be a natural fit for AI collaboration? Could LLM help generate

proofs that something mathematical is correct? In this conversation, we explore that question. We begin by discussing what theorem provers are, their history, and how they're used today. Kevin walks us through how ACORN integrates AI into the proving process and the benefits and challenges that come along with it. We touch on the history of mathematics, the foundations of formal reasoning built on solid axioms, and how AI might accelerate the creation of mathematical knowledge. If you're a researcher interested in tools that might change your workflow, this episode is for you. Now, before we kick off, I just want to share that we've launched season 3 of the ZK Whiteboard sessions. The ZK whiteboard sessions are produced by ZK Hack in collaboration with Bane Capital Crypto. This series goes deep on some of the key concepts in

ZK. I've added a link in the show notes. Be sure to check out these videos. They are a great way to learn about the fundamentals and techniques powering the ZK systems we often discuss on this show. Also, if you're looking to jump into ZK professionally or just looking for a new role, I wanted to point you towards the ZK jobs board. There you can find job postings from top teams working in ZK. And if you're a team looking to hire, you can also post your job there today. We've heard great things from teams who found their perfect hire through this platform and we hope it can help you as well. Find out more over at jobsboard.zeronowledge.fm.

You can find this on our website and I've added it to the show notes. Now, here is our episode with Kevin Lacer from Acorn. Today, GMO and I are here with Kevin, the creator of Acorn, which is a theorem prover. Welcome to the show, Kevin. >> Hi, Anna. Thanks for having me on. >> Hello, GMO. >> What's up? >> All right, I think to get started, it would be great for us to understand what exactly a theorem prover is and what Acorn is. >> So, ACORN is a theorem prover, which means you write mathematics in it and the theorem prover checks that your mathematics is correct. And what makes it special among theorem provers is that it has an integrated AI with the goal of making it easier to use.

>> Very cool. and we're going to be spending most of the episode talking about Acorn. So, we're going to get into the weeds, but I do want to mention that this interview was prompted by two things. One was a conversation happening in the big ZK podcast Telegram group, I think a few weeks or months ago. It was about whether LLMs could be used to help generate proofs and prove proofs and whether people could trust them and what it would take. And I think at the same time around the same time GMO you had just published a blog post called Acorn and the future of AI theorem proving and Kobe flagged that for me being like hey or for all of us actually being like this is coming up in the ZK community

why don't we have a chat about it and so this is how this episode came to be just before this interview GMO you and I were chatting about your paper as well and you gave me like a little bit of a framework for what you were thinking about with that paper. So maybe you could share a bit about that and then we should dive into Acorn. Actually, then we should dive into Kevin's background and then we should dive into Acorn. >> Yes, totally agree. So really quickly, I guess I'll just set up the what like the blog post is about is essentially like how do we do math? We like say something, give a theorem or a statement of a theorem and then we like prove it.

And what does it mean to prove it? Is like you write out some English that like tries to convince the person who's reading it that this thing must be true. And you know the cool part about math is unlike many other fields is you can there's like axioms right like in some sense every theorem is true because you can reduce all the way down to like the axioms of how numbers get added blah blah blah. And you know people realize this this is pretty early in like the 20th century and realized that you could like mechanize math. You could have a computer essentially check that your mathematics is correct. Right? And this is actually how you prove a bunch of interesting theorems about metathematics. Funnily enough, this is like why Turing came up with his original idea for a touring machine.

It's actually not >> for breaking the enigma or whatever. It was very much for proving theorems or showing that theorems are otherwise like not necessarily provable. So, okay. So, cool. You know, now we have modern computers. Like we can actually not just make a touring machine like a virtual thing in our head, but we can make it a quasi reality and you know you can like now give theorems to computers and then have it check that like a theorem is correct, right? By going all the way back down to the axioms and checking that every single step that you've done in this like theorem is good. And that's cool. You know, you get things like when you do that, you get a you can get in many languages, but one of them being lean and you can write out theorems as if they were programs. And if the

program compiles then you know the theorem is correct. >> The problem is that it sucks. It really sucks. Like it sucks in every possible way one could say it sucks >> because you know there's a gajillion like theorems you can prove about like tiny things like you add stuff and when you add stuff like you know when you add A and B that's the same thing as adding B and A. >> Do you mean like you'd have to write both of these rules into the language like all the edge cases and all the like variations? >> Yeah like exactly that's like one way to think about it. Yeah. So you you have to write it into the language like somebody has to go and like prove that that is true and it's a very trivial thing to prove that it is true often or at least

trivial enough but somebody has to go do that work right because you have to show the computer that every single possible step in every single proof is justified and so you end up you know if you think about like you know programs as or like aorems as programs right like every single one of these things has like a name associated with it like adcom is like a thing and it's like yes like it's true like it's an important thing to know, but it's like not how mathematicians think about math. We just like of course like A and B and B and A. Like people say an A plus B are the same thing. Like just like we don't talk about it. >> And so that's why it sucks is because like you know computers are the ultimate pedantic checkers, right? They like check every single possible thing even

though like you know it's true or obvious or things like that. >> And you know but these are trivial theorems to show and prove. And so I think this is where Kevin's, you know, we'll talk about it, but this is where ACORN is like a very beautiful thing which like like math is when you prove a theorem in math, you state things that are true and they don't necessarily like follow perfectly one after the other, but they are like very simple logical jumps, >> right? So it's not everything is perfectly justified at every step. Uh but it can be perfectly justified upon request >> and that's the important part. It's like when it is requested, it can be perfectly justified and the justification is often very simple. And so why not instead of forcing humans to do that, why not make the computer or the LLM, which is pretty good at doing

these kind of routine mechanical steps or not LM like an ML model in general, like justify those for the human and so the human can write things that look much more like normal math and in turn, you know, end up with like an actual like legible set of steps as opposed to a lean proof where you have to essentially justify every single step. They have shortcuts and stuff. I'm glossing over a lot of this, but anyways, that's what the blog post is about, and that's what we'll get into like very deeply in this episode, which I'm very excited to do. Um, yeah, >> very cool. All right, so that's a little bit of like the intro to the themes of this episode, but maybe before we kind of dive in, Kevin, I think it would be great to hear a bit about you and what

got you interested in this, what you were working on before. Have you been a mathematician your whole life? Like, what's exciting about this? I wouldn't say I've been a mathematician my whole life, but I've always been pretty interested in mathematics. When I was, let's see, long long ago, like in high school and college, I did a bunch of mathematical competitions. >> Um, like the International Math Olympiad and the the Putinham exam. And so recently, maybe you know 3 or 5 years ago or so, there was some interest in hey can we can we get these computer systems to solve these math contests.

>> Um and recently there has been a lot of great success in in LLM world in making that work. And I think there was a suspicion at the time that this was you know something to get into. And when people started talking about that, I thought, "Oh, hey, you know, I have I have this background, maybe this mathematics that that personally of I've of more like let be an aspect of my past, maybe that's relevant. Maybe I should take a look at these things." >> Were you a software developer? Like what kind of work were you doing before that that made this seem like something you should take on? >> Yeah, I've I've been a software engineer for a while. I worked I worked at uh Google and Facebook and started a couple Y Cominator companies. one one parse which was aimed at you know being a

developer tool making databases easier to use for mobile developers. So the the concept of making a tool with a good developer experience was a very familiar one to me. And so when I took a a look at lean at some point when people were starting to say okay can we can we make this system useful for solving math contest problems at some point they were saying oh can we could some people formalize the results of some IMO problems and so I thought okay that's something I can help out with you know I have a bit of familiarity with lean a bit of familiarity with IMO problems and then I started doing it and just quickly felt like oh this is this is much harder than I expected. M

>> uh I'm familiar with a lot of programming languages, but this adds many more layers of difficulty because you have to prove every step along the way and it involves remembering many many tactics is what it's called. different ways of solving different proofs and I worked on some some systems in in lean uh a rewrite search tactic to try to solve some stuff but after a little while it seemed it it like it wasn't a great fit >> and it made me think about well what what would a language look like if you thought that well what would the ideal interface for a person be to write this and if you could imagine that the AI could solve all the awkward bits for you how how would that inform the design of

the language itself? Is Acorn then a language or is it a tool set or is it a product? Because I mean you refer to it as a theorem prover but I don't know what that is like is it a concept. >> So the way you use it is you open up VS code and you type in characters that are that are written in a language the acorn language. >> Okay. >> But it's not a programming language because it's not designed to write code. You're not reversing a linked list. >> Um it's a language for mathematics. you're expressing a mathematical statement like if uh x is an even number then you know x 5 is also an even number >> some sort of thing like that so you can you can express that in acorn and then

what the theorem prover does is you you run it as a vs code plugin most commonly and the theorem prover you you type some mathematics and it just checks your mathematics for you if it if your mathematics is correct it puts a little check mark there >> and if your mathematics is wrong it will put a little yellow squiggle there. And if you type something that was complete nonsense, like it can't even tell what you're doing, it'll it'll put a little red squiggle. >> Is it similar to lean then? Is it taking like is lean similar to that or is it kind of moving it in a different direction?

>> It's similar to lean in the sense that it's a theorem prover. They both have the same goal of letting you express mathematics and letting you express a proof of it and verify that the proof is correct. But in practice when you look at lean code the majority of it is not mathematics but tactics which is a separate language besides mathematics that expresses how a proof is created. >> Ah >> the idea of acorn is that you don't learn two separate languages. You just learn the way to express mathematics and the AI will fill in the details for you and tell you if it can prove it or not.

And so the hope is that this is more like the human way of thinking about mathematics where you think of a bunch of mathematical statements and you might tell your friend, hey, is this does this seem reasonable? And when you tell your friend, well, if x²= 9, does that mean that x must equal plus or minus 3? Your friend doesn't ask you about your tactics for proving it or anything like that. They just say, yes, that's correct. >> Okay. >> Yeah. That the way I would compare it to Lena is like Lena's like hasll or maybe like rust. >> Oh, >> right. Like Rust is cool and it lets you express you know very very flexible types and you know how these things connect to each other traits and things like that. It is also incredibly verbose and the reason why is because like you

can essentially construct like while that's very good for like ensuring things are you know very nice and concrete in production all this stuff like in math we kind of implicitly endow like objects that we care about with types right or with like information about them and that information can be gleaned from the context it doesn't need to be kind of you know explicitly stated by the user so you can construct languages and a language I will like put in a separate bin is like more like Julia like Julia is also strongly typed in the same sense that Rust is in the sense of like every single object has a type it can have these like abstract classes and stuff but at the same time like you know you don't have to explicitly write all all of that information and in math we just want to

check whether something is true or not like we're not like trying to like make a production level system that like somehow can avoid edge cases or whatever right and so certainly you could do a lot of work like the machine can do a lot of work to like infer or what things are important about the thing you're writing. So lean if you like look at it it looks like very much like a very a fairly complicated language with a bunch of different functions and calls and syntax around like how you do different tactics and all this stuff >> whereas ACORN looks kind of like a much dumber and this is a very complimentary thing looks much dumber and it's like you know you have a theorem which is a statement and you have a bunch of lines that are just like how you would write

math normally you would just say like this thing is equal to this thing and this other thing is equal to this thing. And like Kevin said, the point is, you know, when you explain your proof to a friend, you're not explaining like the tactics you used to rewrite one side to the other. You simply just say like this thing is true, then obviously this next thing is true because it's like state that and your friend can like in their head come up with like why it must be true. And the point is instead of a friend here, you have your AI assistant friend who does the filling in those steps for you. whereas lean requires you not your AI assistant friend to fill in those steps for you and do so very very explicitly.

>> So anyways I I would recommend just like it will be helpful to like compare the syntax. I think in the blog post I have like a comparison of like what Acorn's version of this is and the proof in in lean and it's like it's actually quite enlightening because it's very illeible to a mathematician unless you're already very familiar with theorem provings like languages. >> Cool. We're definitely adding that link. I didn't mention that earlier, but we'll be adding that link in the show notes if anyone wants to see that article. You mentioned Kevin though at the start that like it's using AI. What's your connection to machine learning AI? Like are you coming also from a space that worked with that?

>> I've worked a little bit on AI in the past. Long long ago I wrote little tiny AI models at Google to solve problems that now seem ridiculously trivial. like if a domain name you know had uh you know zk prover for example or you know zero knowledge.fm FM. How how do you know that zero knowledge is actually two words, zero plus knowledge? >> Um, and you know, 20 years ago, this was a very difficult problem requiring AI. >> Nowadays with with generative AI, the AI is many many times stronger. So I would say I just h have a little bit of background in it enough to start figuring some stuff out.

>> In the case of Acorn, like how is the AI brought into it? like are you using out of the box solutions and sort of I don't know how you would do this but like adding it into the language and into this sort of theorem improver or is it like a bespoke take are you kind of training it yourself what's what is it >> it is trained itself on the acorn library so acorn is in in two parts there's the theorem prover itself and then there's the mathematical library so the mathematical library is written in acorn >> and contains a bunch of these very detailed proofs for basic stuff like you know how do you multiply two rational numbers together you know what are some

facts about even numbers or factorials and so from someone using it from their point of view when you get the VS code extension you download it and it comes with a small local AI model okay >> that is included and so every time you type a line or every time you save something it can run. >> Um, and so I think this is really important for the the mathematician experience as you type things because you want it to be saying, "Yeah, that's good every time you write a line."

>> Huh. >> And so it isn't as powerful as, for example, these models that are winning the imo by spending a large cluster and teams of enormous amounts of people to to crack these problems with many hours of computer time. But it is a tool that you can just go use right now. And when you have a tool that takes, you know, moments to give you feedback, it lets the the human and and the AI work together in conjunction. >> Interesting. I know you guys just defined it as very different from Rust, but as you say that, I start to think like is this sort of like a real time version of how like Rust does the compiling and tells you if there's bugs?

Would you put it at all in a similar category in terms of concept or is it so different left field? Yeah, >> I think it's similar. I think if you think of the borrow checker, you know, if you're writing some Rust, you just type your code and then occasionally it says, oh, you know, this mutable reference conflicts with this immutable reference. >> And in Rust, you don't explicitly say here are all these lifetimes. Here are these memory rules. There's all this stuff that in Rust is implicit. And if you're writing C++, you need to say in every single spot where exactly is every variable deallocated. And so if you compare some C++ code to the code doing the same thing in Rust, you'll find this the C++ is writing all these explicit deallocators. You're managing it

everywhere. You can screw it up all the time. >> And Rust makes this part of it easier. And you do have a little more you're a little bit more handcuffed if you really want to shoot off your foot than >> Okay. then C++ will make that easier for you. >> And would would in this analogy is lean more similar to C++ and Acorn's more similar to Rust? >> I think the the vision for Acorn is for writing it to feel more like writing Python. >> Okay. um where if it's it's clean and simple and if you take someone who is not primarily a software engineer, it's a lot easier to start learning Python when all this additional stuff to help

you is things that you can kind of ignore or not think about. And then if you compare to writing a more a more strict language like either C++ or Rust, there's a lot more stuff you have to learn. And so writing acorn should be much easier for a mathematician to sit down and learn some basic syntax and then start using it. >> I think like one really helpful thing which is like I it's kind of hard to describe in words. It's like way easier to be like you should just pull up you know acornprover.org or whatever. I don't remember what the link is. >> That is it. >> Okay. Nailed it. So good. Uh but like do you want to describe the workflow? Like the workflow is like a very it's a very satisfying thing. And I remember like I downloaded it and I kind of ran it and I

was like this is the way these things should be not like whatever nonsense we were doing before and I think that's the thing that like immediately to me was like very cool about it like highle description of the workflow like what does it look like yeah you download you know you have yes code you download this extension I want to prove that you know if I have an odd number I add one to it it becomes even what happens the the way I think of it is what workflow do I want if I'm writing a proof And I have someone who's just much smarter than me standing over my shoulder and helping me out as I go through it. And so to take your example, if I want to prove that if I have an odd number and I add one, it's an even number, then I would start out by taking

this that we can express in English and then writing it in the formal language. So in a be something like theorem you write the name you have your variable you know x is a natural number and then you you state the theorem you know like x is odd implies x + one is even all right and so in the acorn workflow you save this and what I think will happen immediately if you type it in correctly is it will put a a little yellow squiggle which means two things it means yes you wrote it down correctly if you're missing a parenthesis or something it'll red squiggle it >> and it means this is not trivial This is not something that you can just say without assuming. You got to prove it.

And so you think, okay, well, how do I start proving it? All right. So if if n is your odd number, the way you start proving it is, well, you let d a natural number be such that 2 * d + 1 equals n. And so this this thing I've said out loud is just about exactly one line in acorn code. Let dnat satisfy squiggly braces here, 2 * d + 1= n. And then you save your file. And then Acorn will check it for you if you mistyped it. Red squiggle. And I think this should be enough that it doesn't require a yellow squiggle. It says, "Okay, this should be like this is something you could take for granted because there's already some theorem or this is just the definition of odd probably >> like the definition of odd is there exists some number D, right? So that 2 *

D + 1 is the number. >> Yeah. All right. And then let's let's think about it. So 2 * D + 1 equals N plus one. So, I know this to be true because in my head I'm I'm doing the little algebbras and stuff and I actually don't know right now. This this is maybe on the boundary. I'd have to look to see if Acorn is going to be like, "Yep, that's obvious." Or if you have to put in another check. >> I actually think it it might automatically get it from here. But anyways, yeah, let's assume it doesn't. I I think I think it should, but I mean this is one of the underlying things which is however good the AI is now the whole world of people building AI things there there's so many brilliant people and so much effort into it into both how

good the public models are and how good are the the tools for you to train your own >> that you want to just build something and then think okay hopefully the AI people can just make this stuff work 10 times better over time. >> In this example though it doesn't fix it for you. It's literally just highlighting whether it's true or not, right? Or does it prompt you to tell you like, oh, maybe this is what you need. >> It doesn't really prompt you to say what you need if it says, you know, it's it's either if if it recognizes immediately, I know how to prove this. Then it just says check mark. >> Mhm. >> Um, and then if you if you select a thing, because if you type something and it's like, yep, that's true. And you're like, wait a moment, why? Like I I was

just kind of guessing. Uh, because sometimes that'll happen. The AI is like a step ahead of you. Then you select it and there's there's another panel in the editor you're using that will show you, okay, here is like why this thing is actually true. >> Okay. >> So, if it knows it, it'll just it'll explain the whole thing to you. And if it doesn't know it, it'll say, you know, I don't know. Why don't you why don't you keep going? >> Interesting. >> And I I think we can we could sort of build other stuff over time where it says, I don't actually know, but I have some ideas and let's have some feedback and let's go back and forth and chat. And I do think that that would be a compelling thing to do. But I think at that point we have to hook in cloud LLMs

and figure out some way to do all that stuff because this sort of local model is not yet powerful to just chat, you know, about whatever you want and to have a whole language thing going on. >> I actually have a bit of a disagreement on this now. >> Oh, yeah. >> So, so recently, I think about two months ago or something, Quen released a set of updated models. Oh, these are tiny models, by the way. >> What was the name you said? Quen. Quen QN. >> Okay. >> And I would highly recommend you do this. Just download the I think it's Quen 4B or something like that. Quen 4B thinking or something like that. It's a 4 billion parameter model. Runs on a phone. It can run on your laptop. No problem. Whatever laptop you have, it'll run quite well. And ask it something.

Ask it something like, you know, my my standard question for these tiny models is like, please solve this like small convex problem that's like non-obvious unless you're already familiar with it. And it will nail it. like nail like just like literally give you a complete English level proof that would absolutely convince any human that knows anything about math that this thing is true and it's not a problem that as far as I know is like super obvious in training data because it requires some like interesting steps about like AMGM inequalities and stuff but the point is I suspect actually that if somebody could be you Anna were to fine-tune said model on the acorn library I think it would probably be quite quite good at proving a lot of these these theorems

about like lists and and basic number theory and stuff like that. Like quite quite good. I was very impressed by what a 4B model could do. >> Yeah, I need to check out these Quinn models. It's definitely a danger of saying that anything is not quite possible in AI world uh nowadays is that you'll discover that there there's some other thing that came out in the last 6 months that like well it just it goes beyond your level >> is yeah there there's like a million people on like a hundred billion dollars trying to prove you wrong as much as possible you know or whatever. >> Yeah. Exactly. you know, and I'm I I think it's it's a pretty good bet that eventually, you know, even if even if Quen 4B thinking doesn't quite hit the sweet spot, it doesn't seem like we're anywhere close to how well you can do

with a model that's running locally. >> Yep. >> And there's also, you know, the model doesn't have to be running locally. It could be integrating a remote model. So there's there's many many different possibilities here for ways to improve the AI component of ACORN to make it even easier. >> You sort of said there's these two components that there there's a theorem prover and then there's this mathematical library. Can you explain a little more what that looks like? >> So the idea of theorem provers is that you can prove all of math from a a very basic set of axioms.

>> Okay. And these axioms, you know, pe people have figured this out over the past hundred years or so. >> The uh I think in the 1910s people before computers existed, people tried to boil down all of mathematics with the Prancipia, Mathematica, Russell and Whitehead, and it ended up being this this enormous book where it's like, okay, at page 200, you get to 2 plus 2 equals 4. And so people have been making these systems better and better over time in terms of a simpler set of axioms that is able to prove these things in a more straightforward way. And so I think the general way of of how to do this is is pretty accepted among the theorem proving community right now where you

start with some ways to handle inductive structures like a list where you can start off with either you have an empty list or you have you know you construct a slightly larger list from a smaller list >> and then you can you can build numbers that way too because natural numbers work the same way as a list right you have zero and then whenever you have a number you can have one one after it M >> and then you have you have some some basic axioms that involve things like substituting into a formula. You know if you have a formula where x is is some you know any natural number then and you have y is a natural number then you can substitute that in and then you have equality. If you have two expressions that are equal then you can substitute them out in any other expression. And

there's there's basically a pretty small list of of this sort of a and then you can start building up mathematics things like lists, natural numbers, integers. So integers as opposed to natural numbers and integers where you also allow negative ones and then rational numbers, real numbers, sets, all these other structures you can prove in terms of the more basic ones. And there's just many facts about these these structures that you can prove from from the basics. Interesting. You know, like if you have a list, if you reverse a list twice, then you get the same list. >> Yeah. You you would say that to to someone else and they'd say, "Yes, obviously." And then to actually write out the proof from the very basic definition of list is, you know, a fairly a fairly long ordeal.

>> This reminds me a little bit of an episode we recently did on IO. So this here I want to take it a bit into the cryptography proof direction, but >> IO being like a theoretical cryptography and our guest on the show was Rachel Lynn talking about a paper they had written in 2021 which was like using wellfounded assumptions like the some of these proofs that had been somewhat tested to now build a proof that this IO was possible under certain circumstances. and she she had a really lovely like analogy for assumptions and how they're very creative but then you have to prove them. So as as you talk about this and you talk about like build

these building blocks like there's the basics the axioms that are wellfounded people have very much accepted them and then you try to build on top of it and that's also how you've built as I understand this mathematical library or is the library just those basics and then the AI actually has to like learn like teach itself those levels up >> the very basics like the rules for equality and substitution and induction are built into the language and then the library is written on top of that in the acorn language.

>> Okay. >> And then the AI gets trained on the library to help you add more to the library. >> I see >> there's a flywheel of the more you add to the library, the smarter the AI can get. >> And then the smarter the AI gets, the easier it is to add more stuff to the library and so on. >> So yeah, I really want to hammer at this particular point too. One of the things I do want to like mention for like the library is like we think of libraries as like oh these are tools that we then use to build other things and that's kind of true but the way I would think about like libraries in theorem proving is that they are in in other words like a collection of statements that we know to be true and ideally like the best

possible library is a library that contains all statements that are known to be true. Oh, >> right. >> But that would be very big. >> That would be enormous. But nevertheless, it would be like the coolest library. And that's what kind of lean lean has a version of this called math lib. >> Oh yeah. >> Which they are trying to do, right? So they're trying to like every known statement that is obviously not every known statement like statements that are important enough >> to like have papers about them or something you would like to prove and then incorporate into the standard library. So it says other people can then use those theorems to prove newer theorems. Acorn's Acorn LIB I think is the actual name attempts to do something very similar but with an additional and important change which is because this AI model is integrated into Acorn itself

as people prove more theorems you can train the AI model to learn the techniques that people use to prove those theorems to prove newer theorems which in turn should enable like future theorems to be proven more easily because the AI now knows about the techniques that were used to prove theorems of the centered library. So it's this like very nice flywheel as Kevin noted. >> Are people who use ACORN adding to this library every time they do something? Then >> you can submit and add to the library if you want and you can also just use it on your own mathematical problems. It's it's up to you.

>> Would you be adding to your own library as you go? >> You can. Okay. But it's most I I think the eventual goal for the Acorn library is to have all mathematics in it. Okay. >> I mean you said that's all known mathematics is large. It's true in a sense but when you compare to the scope of these general AI projects I mean an LLM will be trained on all the documents on the internet and there's only about 100 math papers published today. It's sort of larger or smaller depending on how you think about it. So if you try to imagine a system that ingests 100 PDFs per day, >> that doesn't seem like an inordinate

volume. If you could even process it with, you know, you can you can afford to spend a decent amount of work for each one. M >> if it actually worked. I you know I should say once it actually works because it really seems like it will once the AI is able to do a human level job of taking a PDF and turning it into mathematics and incorporating it into a library. We should be able to take the existing human produced 100 PDFs per day and add to the library. >> The job's probably going to get even harder because once we have these better AI tools, people are going to use them to create even more mathematics, >> right? So, you know, we'll have to figure out how to handle that when we come to it. But the goal of the library is to have all mathematical knowledge in

a form where you can simply ask, is this thing true or not? And it has indexed all known mathematics. >> Do you then host this like master live? Because you you guys are talking sometimes about like doing it locally, but then also this like I I don't know if you can expect every person to locally be ingesting all of these papers every day. So is there sort of like a I don't know a central master list master library or something there >> there is there's there's a central one it's I mean it's a GitHub repository I think to actually scale up to be taking a 100 papers worth a day >> um I mean if you think of that as a 100 pull requests per day that's a lot but a lot of systems do handle that I think the only plausible way to get there will

be to have AI code reviewing and accepting pull requests and I don't think we're close to that. But I think we're going to get there. >> The difference between this and other sorts of code is that you can just validate that it's true. And if you have an ugly proof for something, but it works, >> that's pretty good. It's true. And if you imagine a world where well, if you have a hundred really ugly proofs being incorporated into your library every day, can you handle that? I think the answer has to be yes. We're we're going to handle that. That's how it's going to work. And if people or AI systems would like to come back and clean that up later, hey, that's great. Go for it.

>> Yeah, it is it is a funny philosophy, right? Like what's interesting about math 2 here and this is a debate I think like currently going on on Twitter. I just kind of woke up this morning and saw it, but >> is the cool part about theorem provers is like if it compiles it's good. Like that's the whole point. The whole point is like it doesn't matter like how you did it or where you did it. If you agree that this is a statement that is being made and it's a useful statement, if Acorn gives you a little check mark, then you're good. Like that statement is true by the reason stated below plus like whatever analysis of magic in it. At some point you would be able to like check every single line and in turn you would be able to see that you have

reduced it to like the axioms of mathematics or whatever and which is very different right from like kind of AI assisted slop as it comes into libraries, right? Like people right now are getting very defensive of programming projects because kind of if you if you have no idea what's going on, right, and use an LLM to like create a you know cryptographic library or something of the like, you're kind of screwed, right? Like if you have if you truly have no clue what's going on, you have no idea if like the AI has like constructed a thing that looks plausibly like it does something correct, but actually it's completely like useless or up or broken. Whereas by construction and by the fact that mathematics is like the one of the few truly checkable things here you can be sure that the thing is correct in the

sense of like you have proven the thing you have said you wanted to prove >> uh by definition like the acorn itself goes and does this checking for you and it has checked that you have indeed proven this theorem although the proof might be completely unreadable to a human and the hope I think Kevin is which is kind of an interesting thing is we should just accept the AI slop right output or whatever it is. Maybe not. Maybe I'm going to strain it in a little bit. But but the point is like if somebody really cares about this particular proof, you could either have a human or another AI tool go rewrite this in a way that is like more legible or more clean for somebody to go read through it. But the point is once you have a proof of that statement that Acorn itself kind of accepts it, says

like this is correct or this is good, then you know the statement is true. And the question is is it like worth including this in a library? And the answer is probably yes. H but when you talk about those like ugly proofs like if you have a lot of ugly proofs do they sometimes like mess with each other or just create like noise or even if they come through as true and correct can it compound over time if you start let like adding those together and then building on top of them can there be like more messed up problems within that >> you could definitely have messed up problems I think you do have to slightly distinguish between theorem statements and the proofs of the theorems themselves because a lot of concepts it's not quite clear what the cleanest

way to define them is. So there there are some funny edge cases like how do you express the fact that one divided by 0 is like quote an invalid thing to do. >> Yeah. Or another example is how do you represent subgroups is this is a little bit more mathematical but is a subgroup fundamentally tied to the group that it is part of. You know it's like you have a data structure and there's a couple different ways to define a data structure. You know it's like when you're defining a list for example should you say well this is a list of just one particular type or should you say this is a list of any type. So you have these sorts of definition questions and these are almost more aesthetic principles. If you define all your

variables really stupidly, then it's going to frustrate humans that read this. Whereas, if you prove things in a very roundabout way, you can generally ignore the proofs. >> So, we can't just let the LLM's sloth all over everything. I mean, in an acorn, it's separated out. You have the actual proof certificates where philosophically, that's where the LLM slop goes. If something is garbage and really long and the AI is like, "Here's the proof." Well, it's it's shunted off to the side. It's like in a different file where typically you don't look at it. If you want to debug, it's kind of like popping the hood of your car to see the guts of what's going on there. And then you have the acorn language itself, which is, you know, the idea is that this should be beautiful and simple.

When I think, hm, why is this true? I should be able to read the acorn and that looks pretty nice. M >> so to actually achieve the dream of having the computers or the AIS accept 100 PDFs a day we'll have to figure out a little bit more but we're not quite at that point yet. >> Do you see Acorn being used in cryptography for cryptography type proofs or more for other kinds of mathematical proofs? >> You know I think you two probably know so much more than I do about cryptography. I I would be excited for it to be useful. It's not entirely straightforward to me how it would be or what is what is the big need in cryptography.

>> I think in general with my understanding with zero knowledge stuff is that you usually want to prove that a specific computation actually did happen. >> So it's kind of like proving one specific sort of thing and the tools you have to do that are designed for that and they seem pretty good at it. Yeah, I think I mean ZKPS can be used to prove that something happened, but the people who create the zero knowledge proof systems have to prove things about those systems. That's it's more in the it's it's more for the practitioners and less maybe for the user of the proving system that I'm thinking a tool like this might be useful.

>> So yeah, exactly. Exactly. I think there's there's two things to separate out here and and I think both are quite interesting. So, funnily enough, the reason I actually got originally into ACORN, and it's funny that you discussed the subgroup thing because I think the current definition of subgroup might No, it's actually your definition of finite subgroup is my definition that's in Acorn Lab if I recall correctly. >> I'd have to look. >> Yeah. Yeah. Anyways, it's very entertaining because it's like we we now have two weird slightly different definitions of subgroup. One for the finite case and one for the not finite case. And so, the definitions are turned out to be quite important. But anyways, stepping aside, the reason I started that project was because I actually wanted to prove things about cryptography in Acorn.

>> Ah, >> and originally I wanted to do it in lean because I just wanted to formally verify some papers which some people are like now kind of depending on for cryptographic protocols >> and I wanted to show that like under the standard assumptions that the paper makes actually this is like a this protocol is like a reasonable protocol. So one one version of it is like under the random oracle model, you know, Zoda is like a a protocol that actually does what it states it does, >> right? And it's kind of a pain in the ass to prove in Lena. It's an enormous pain in the ass to prove this. Like I truly like enormous because you have to like define all sorts of nonsense and you have to go all the way back to like really annoying definitions and like rewrite them slightly because they're

like a little bit different than you expect. >> So Acorn was very very appealing in that sense. And so okay so there's like that part which is you know when you construct ZK systems or system proof systems or whatever you have to prove mathematical statements and indeed those mathematical proofs >> uh are perfectly amendable in acorn right you can like write the theorem statement in acorn and the statement could be something like somebody has given you this random linear combination if the following you know things all match up to the way you expect and extra with extraordinary high probability the thing that you are like looking at actually is correct M >> there's a second point which is the practitioner version of it which is cool like I have a system and that I have engineered this system to like run on a

computer >> and the question is is the system is a spec of that system match the like math that we are assuming is correct. We're going to like for now assume somebody wrote an acorn and the math is good. Does this particular implementation of that system match the mathematics? I actually do think it is possible to do some interesting intermediate stuff in Acorn. But as it stands today, it is not currently easily possible >> to translate kind of this code which is like a thing that performs some set of steps into something that you could prove in ACORN to be equivalent to the mathematics >> cuz there you're getting more into formal verification, aren't you? Like

that's more like a different category of it's engineering and it's like security and the engineering front. >> Well, that's exactly it. So like fundamentally interactive theorem proving is formal verification. >> Oh, >> like these two are the same thing. Formal verification but of mathematics as opposed to of programs. Exactly. Okay. >> But but the whole point is that mathematics is a program. like you can write any proof as a program and there's all sorts of nonsense on this and you can >> so you could imagine and actually I suspect it's probably not that difficult but as it stands today it's a little bit annoying >> essentially formally verifying programs inside of ACORN by essentially writing like a spec of the machine that is executing the program inside of Acorn and then showing you know using these

inductive types and all this stuff that you have done something correctly. >> Yeah, >> that is reasonable. I think it's it's hard to even predict what's going to be possible in a couple years because the whole the whole space of both theorem proving and formal verification the tradeoff that has existed since forever is that it's a whole bunch of extra work formally verifying these systems is nice to have but it's a lot more work and so are you going to go and do that and what we're seeing not just for these systems but really for all software engineering is that the cost of doing standard software engineering stuff is dropping rapidly as the AIS get really good at doing it. So things like formal verification, theorem proving or really

any sort of weird model of programming where you want to carry around some extra state all the time and be doing a whole lot of extra bookkeeping um is going to be much more possible in the near future as these tools get better. >> It almost sounds like right now too. Acorn is about adding AI into theorem proving, but eventually it would be like theorem proving would be in the AI itself doing something bigger potentially like if it's generating the code that this theorem proving would be incorporated within it. I wonder >> so as it stands today this is actually kind of what Acorn is doing transparently. So remember that Kevin said like oh if you write some statement

>> right and it's like oh yeah cool like we have like whatever let and let d satisfy whatever >> and it puts a check mark after it you can like actually click on that statement >> and if you actually click on the statement you'll see like on the right hand panel you'll see a list of like things and that's actually like what the AI has done to prove that statement to itself and you >> so in some sense acorn is I would say is the limit of that which is the opposite it's like what happens when you just completely bypass kind of the lean you have to justify every step, right? And just condense that into like look, the AI does this.

Well, we can show it to you when you need it, but like is otherwise irrelevant. Like it doesn't matter. Like it doesn't >> like the AI has proven this. You don't have to worry about it. Don't worry. You know, like your your head like the AI slop is like below the surface. I think this is very interesting here. And I I do agree though like you could imagine like the secondary flywheel here being like as you train models on the standard library these like very fancy models you can then produce new mathematics more easily and it itself can write further proofs which it can then train you know as they become correct. It's like a it's like a mini reinforcement learning loop as like these things are judged to be correct. It can train itself on those things and so on and so forth.

>> And it would have like sort of this theorem prover and formal verification built into how it's working almost >> potentially. >> You can imagine also exactly like what Kevin was saying is putting in programs, right? And then having an LLM translate those to like formal proofs of their correctness, >> right, without kind of doing intermediate work. and you would be sure that it's good because you can read the statements and then you can read the and make sure that it's like actually correctly translated. >> Okay. So, right now we're talking as though AI is for sure going to be better. I think there's some assumptions in this conversation that it is, but there's also I mean at least and maybe it's just in the news right now. There's a little bit of like push back against AI being this beall endall that like

it's still just a copycat machine. at least LLMs are right that it won't ever be able to invent tr truly invent things but we'll always just sort of be emulating and re reproducing and they still hallucinate sometimes. So in that case like knowing what we what we know about AI to date is there a chance that sometimes it acts wrong like is there a chance that it's saying something is proven and it isn't proven? There's definitely the possibility that there are bugs in the system and it proves something that that it's wrong about.

>> Okay. >> Uh I think that the the way you solve this is by finding your bugs and fixing the bugs. But the idea of the theorem prover is that you have this core of the theorem prover which is written by a human and you can verify it in different ways. You can have one theorem proverify the core of the other one. And once you have this trusted verifiable core, you can run it on enormous amounts of stuff that is LM generated or generated by some other sort of AI. And you know, this thing makes errors all the time, but when you have the trusted core thing go through and filter out the errors, you're left with stuff that is just as trustworthy as the trustable core. So

the hallucinations part of it I think that is it's a big problem with modern AI and the idea of the theorem prover is just the precise antidote for this problem. >> Yeah. The cool part here, right, is if you trust this small core of the the theorem prover is correct and that it is indeed verifying what it says that is verifying. But it's the same way like you might want to do with succinct proofs or zk proofs, right? >> In zk proofs, you have to trust the verifier like the verifier has to be correctly written. This is precisely precisely analogous to this trusted core of acorn, right? If that is proven and if that is good, if you like have read it yourself and it's good and it's simple enough to like go through, then

you will accept. It doesn't matter whether the proof is incorrect or correct. If you only accept correct proofs, >> you're golden. Like you're good. You know, like you know that the proof must have been good because the verifier itself has accepted the proof and you know the verifier is good. And so it's analogous in that same way here. And so hallucinations are kind of like a side problem. It's like, yeah, maybe the LM hallucinates 99% of the time, but it doesn't matter because if 1% of the time it's good, right? You know that like that 1% is good. And in fact, you can distinguish the good stuff from the bad stuff without needing to do extra work. >> Huh. I don't really get that. I don't know. To me, it still seems like there could be mistakes or there could be like Yeah. Is it just because you run lots of

instances that they correct themselves so you don't like there couldn't be some consistent problem that always shows up? Imagine a really huge code base like the code for Linux. Are you sure that it compiles? I'm I'm pretty sure it compiles because I can run it and it compiles. Okay. >> And so it's deterministic. So if it compiles for me now, I'm going to run it again a little later and it'll compile again. >> Compile again. Okay. >> Can can I be confident it's deterministic? >> I don't know. There might be someone might have made an error somewhere in the Linux compiler or in the in the C compiler. But since you have this idea of well the compiler is going to validate that all of this is valid C code and we do find compiler bugs over time but we fix them and it's pretty

small and so overall you can be pretty confident that the whole thing works and when you do find a compiler bug it's pretty rare because you really just have this this small core of the compiler that you want to be be trustworthy and good. >> Okay. And this is built in a similar way. It it's very similar to to a compiler. It's the same sort of idea of you have this language and you have a small verifier and then you check it that way. >> It can't exactly lie to you or it can't lie because it just wouldn't work. >> That's right. It wouldn't work in the same way that if you snuck in a parenthesis in the wrong place in the middle of a billion lines of C code, >> it would compiler still gonna catch it.

>> Yeah. Okay. And so to to the other I think you had a second point of feedback there which is you know there's this model that the LLMs are very good imitation machines or copying machines >> and there's some sort of special human spark that it doesn't have because it can only copy what it sees other people doing. >> So it's a philosophical position that I don't really know. Let's consider that to be the pessimistic case. If all we can do is copy, then what we should do is we should look at every single PDF that is submitted by the world's most brilliant mathematicians and we should look at those 100 PDF. Yeah. We should

copy that. And if at the end of the day we sit down and and we're like, you know what, this thing is only as smart as the world's hundth smartest mathematician, but I can run it on everyone's laptop. If you say, okay, still good. >> We're we're living in the failure world. This is depressing. But we can still validate all published mathematics. >> We can still give this ability to anyone who wants to do math. They can have this assistant that's as smart as the smartest math professor at their college.

>> Wow. >> And this this would be an amazing sort of distribution. >> Yeah. >> You know, so even this sort of pessimistic outcome would still be pretty great. >> And you know, what do I ultimately believe? It's like, well, this this AI boom, the AI is getting better and better, and where does it stop? I don't know. We'll just have to see. >> Mhm. >> So, you know, we mentioned before, which is like we talked about all the Acorn stuff and the lean stuff and I guess, you know, how how should people go try this out? Like we talk about it being easy and all the stuff like what what what what should we do here? Well, you should go check out the website at aordpro.org.

And the simplest way to get started is just to try it out yourself. It's a VS Code extension. So if you're familiar with VS Code, it's as easy as finding the Acorn prover extension that'll get the local AI model for you and you can write a few lines of math and and see the feedback that it gets for you. And if you're interested and you have more questions about it, then there's also a link to our Discord from the website and there's people who'd love to help you out or complain about more features that that really should exist. And uh it's a it's a thriving Nessen community there.

So I'd encourage people do those things. Check out the website, check out the extension, do some theorem proving, and come say hi in Discord. The other thing I would mention is the sick and cool part is if you do prove some theorems, go do a pull request to the acorn lib and become part of like the machine god, you know, brain. >> At the very least, like an ultimate imitator. >> Yes. >> And at the very most creator of its own theorems. that that would be great. I mean the more the more people contribute to Acorn Lib when the math library gets larger then the AI that trains on it will get better >> and that means the AI assistant will get better which makes ACORD easier to use

and then when it's easier to use it's easier for people to add more to the library. So it's a self-reinforcing cycle. >> Nice. >> Yes. >> Cool. All right, Kevin, thanks for this journey into theorem proving the acorn system, how AI can be used along with it. Thanks, GMO for walking us through this as well and for that article that kind of drew the attention to this project. Uh, at least for us. Yeah, I mean, as a as a non-dein math person, this was really interesting to hear. I hope I hope our listeners who are much deeper in the math will give it a shot.

>> Well, thanks for having me on the podcast. It was a lot of fun. Cool. >> And definitely go try it out. Try Acorn Prover. It's very very very cool. If you ever tried Lean, it'll be way nicer. >> I'm just I'm just showing this thing because it's like super sick and I just want people using it. >> Cool. >> All right. >> I want to say thank you to the podcast team, Henrik, Rachel, Tanya, and Hector. And to our listeners, thanks for listening. [Music]