First Author Interview: AI & formal math (Formal Mathematics Statement Curriculum Learning)
deep learning machine learning arxiv explained neural networks ai artificial intelligence paper openai formal math ai math ai math prover machine learning for math ml math artificial intelligence math ai mathematics automated proof search mini f2f ai imo ai math olympiad openai mathematics openai formal math language models formal math lean lean prover lean proof lean math ai lean environment ai proves theorems ai theorem prover
#openai #math #imo

This is an interview with Stanislas Polu, research engineer at OpenAI and first author of the paper "Formal Mathematics Statement Curriculum Learning".
Watch the paper review here: https://youtu.be/lvYVuOmUVs8

OUTLINE:
0:00 - Intro
2:00 - How do you explain the big public reaction?
4:00 - What's the history behind the paper?
6:15 - How does algorithmic formal math work?
13:10 - How does expert iteration replace self-play?
22:30 - How is the language model trained and used?
30:50 - Why is every model fine-tuned on the initial state?
33:05 - What if we want to prove something we don't know already?
40:35 - How can machines and humans work together?
43:40 - Aren't most produced statements useless?
46:20 - A deeper look at the experimental results
50:10 - What were the high and low points during the research?
54:25 - Where do we go from here?

Paper: https://arxiv.org/abs/2202.01344
miniF2F benchmark: https://github.com/openai/miniF2F
Follow Stan here: https://twitter.com/spolu

Abstract:
We explore the use of expert iteration in the context of language modeling applied to formal mathematics. We show that at same compute budget, expert iteration, by which we mean proof search interleaved with learning, dramatically outperforms proof search only. We also observe that when applied to a collection of formal statements of sufficiently varied difficulty, expert iteration is capable of finding and solving a curriculum of increasingly difficult problems, without the need for associated ground-truth proofs. Finally, by applying this expert iteration to a manually curated set of problem statements, we achieve state-of-the-art on the miniF2F benchmark, automatically solving multiple challenging problems drawn from high school olympiads.

Authors: Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, Ilya Sutskever


Links:
TabNine Code Completion (Referral): http://bit.ly/tabnine-yannick
YouTube: https://www.youtube.com/c/yannickilcher
Twitter: https://twitter.com/ykilcher
Discord: https://discord.gg/4H8xxDF
BitChute: https://www.bitchute.com/channel/yannic-kilcher
LinkedIn: https://www.linkedin.com/in/ykilcher
BiliBili: https://space.bilibili.com/2017636191

If you want to support me, the best thing to do is to share out the content :)

If you want to support me financially (completely optional and voluntary, but a lot of people have asked for this):
SubscribeStar: https://www.subscribestar.com/yannickilcher
Patreon: https://www.patreon.com/yannickilcher
Bitcoin (BTC): bc1q49lsw3q325tr58ygf8sudx2dqfguclvngvy2cq
Ethereum (ETH): 0x7ad3513E3B8f66799f507Aa7874b1B0eBC7F85e2
Litecoin (LTC): LQW2TRyKYetVC8WjFkhpPhtpbDM4Vw7r9m
Monero (XMR): 4ACL8AGrEo5hAir8A9CeVrW8pEauWvnp1WnSDZxW7tziCDLhZAGsgzhRQABDnFy8yuM9fWJDviJPHKRjV4FWt19CJZN9D4n
 Hello there, this is an interview with the first author of the paper, Formal Mathematics Statement Curriculum Learning, in which an automated system was able to solve two problems of the International Mathematics Olympiad. Now, this is an unprecedented level of skill in formal mathematics for an AI system. The system uses language models in combination with a technique called expert iteration to build itself a harder and harder curriculum of theorems to prove. Now, if you haven't seen it, I've made a comprehensive paper review about this paper in the last video. So be sure to check that out because Stan, the author who I'm interviewing today, has seen that video. So we all start from a common level. Stan is able to directly respond to any criticisms and questions that I had during the paper review. And we go into the details into the behind the scenes of the research, what didn't work out what problems came up, how the project came to be and what this all means beyond the domain of mathematics. It is a huge privilege to have the authors of these papers on here. And I want to get the most information that I can out of them. So please let me know how I can improve these videos. Let me know in the comments, leave a like if you like and I'll see you around. Bye. All right, everyone. Hi. So we're here with Stan Polu, who is the first author of the formal mathematics statement curriculum learning of the paper that uses expert iteration to end up proving two IMO problems, which I think was was very well received by everyone in the community. And we're going to look at the paper, going to go maybe through some of my criticisms that I had and that I just threw out there. And yeah, we're going to have we're going to hopefully inform everyone a little bit more. Stan, welcome to the channel. Thank you, Yannick. Thank you very much for having me. It's a pleasure to be here. So this this obviously the paper, it helps that OpenAI is as a name on the paper, right? It gives it like a little bit of a boost in publicity, but still it was the reception was quite widespread, I want to say, even though it appeared, I think in the same week as some other big papers, like I think AlphaCode was in the same week or so. Yet still you made quite an impression on people. And do you have an idea of why sort of the paper was widely received? There have been other papers in this domain, but this was kind of special. What's your impression? Yeah. So, so first, yeah, you mentioned I work at OpenAI, just to give you a little bit of context. So I'm a research engineer at OpenAI. OpenAI is focused on building and deploying safe and beneficial AI systems. It's a bit part research lab and part deployment company and I myself focus on the research lab part. The release was actually the same day as AlphaCode. We actually decided to go for it right after the release that work and I think it was just fine. We did release a first paper before the first GPTF paper, which is reference from that paper a year ago. And it didn't have much support from OpenAI because it was kind of a shadow release. We just put the paper up there, it was a blog post. And it did bring quite a lot of interest as well. I think people are interested in the domain because mass seems like a frontier that we haven't reached yet. And so any progress in that direction seems is probably exciting to most other people in the community. That would be my kind of main understanding of as to why people reacted positively and are engaging with the work. So you were already in this domain, you said, and I think I've also commented on this a little bit. You had previous work in using language models to guide these provers. Was this sort of a natural continuation for that? Or was there some impulse behind you tackling sort of these more challenging problems? Yes, it's really a continuation of the previous work. And actually, to give you a little bit of color on all of that, I joined OpenAI two years ago, and I actually wanted to work on formal math and AI before I joined OpenAI. And I did have quite an original trajectory within the field. I don't have a PhD in machine learning. I don't have a PhD at all, actually. And I was actually a software engineer at Stripe before and eventually wanted to work on subjects that pertain to AI and decided that formal math was the things that I wanted to work on. And then I found that it was well aligned with OpenAI mission and the way we were executing it. And so I joined and shortly after started working on it. So I've actually been working on this for the last two years. And that paper is really a continuation of the first paper. It's just kind of a real continuous work that we are tackling. And I think we'll definitely continue working on that because those two problems are quite impressive, but we're still far away from being at best students level. It is to some extent mind blowing because that system can prove statements that I'm actually myself not capable of proving. I'm not a math competitor, but I did do quite a lot of math studying for engineering school in France. And there are some things that I just can't prove and that this system can prove. But at the same time, there's so many stuff that I find easy and this kind of proven. So we were still a long way away from being able to be at best human level. But still those progress have been really continuous and continuously exciting over the past two years. You've seen my explanation of the paper. And I think with this paper specifically, I'm not that much of an expert in the domain itself. So I'm not too much into formal math and these sort of proving algorithms, how provers even work. I've tried to explain that a little bit by building this proof tree right here. Do you maybe have any more comments, any insights that could help people understand what is formal math even? How does it look from the inside? What is the main problem? How do you do things there? Of course. To be honest, you really made the explanation. It was really clear and I think it's a really good explanation of what's happening. Formal math was kind of invented when computers came out. The main problem that it tries to solve is that when you have a math paper and a very impressive proof, you only have generally a few people in the world that can review that proof because those proof are generally so complicated that only a few people can just understand those. And so there's actually no way to be sure that those massive proof are indeed true. That's kind of annoying because we're talking about mathematics supposed to be rock solid, yet it's not the case because those subjects are so advanced. And so the motivation for formal math is to say, well, let's actually encode math for computers so that computers can check every step. And we're going to get rid of that problem and forever be confident in our math progress. The only caveat is that because people working in formal math needs to reformat the proof in a way that computers can pass, despite a lot of automation that helps in that process, it's still a very, very, very time consuming effort. And so the advance of formalization of math concepts has been lagging behind the state of the art in math tremendously, but it's still starting to pick up, especially in Lean, where we've seen some recent formalization of very advanced and new work. But the main problem of formal math, I think, is that it's really hard to formalize. And so what is formalization like? It's exactly as you stated. You basically state your statements. Stating statements once you have the right definitions is almost natural. It feels a bit complicated when you look at the statements from the paper, as you mentioned, but it's actually close to what you would write in English. But then the proof is really completely different because you really have to contrive it in a way that the computer can understand. And the way it works is, as you mentioned, it's really an interaction between the human and the machine. You have that first statement, which is your goal. You apply some tactics, which are the automation I mentioned, to try to help in the formalization. To generally provide some direction to tactics. And tactics are meta programs that are taking your directions and trying to generate proof terms, which are much lower level artifacts that are understood by the machine. So they bridge between the human and the machine. And you keep going like that. You generally know the informal proof, of course. You generally have to change it in non-trivial ways to make it provable with all the theories you have available and the constraint of the formal system. And eventually you keep making progress like that with trial and error. So you have the feedback from the formal system, which are your current goals, and you try and make progress this way until you, as you mentioned, you reach something that you know is true because it's already been proven or it's an axiom or it's an hypothesis. You mentioned right now that people formalize by already sort of knowing the proof from the math domain, maybe. Are there people that seriously prove things for the first time in the formal way? Or is it largely just a translation effort? Because I'm wondering the way your system works in proof searching, this is not necessarily this paper alone, but it seems to me proof searching, what it does is it simply traverses the tree of all possible kind of like a chess engine or so would do something like this. And I'm wondering if you think that is similar to how humans try to go about proving mathematical concepts or is there some fundamental difference on how the machine does it and how the humans do it? In my opinion, there are some similarities and some massive difference. If you know what the proof is already, it looks a little bit like a translation exercise, but one that is quite challenging because you really have to generally refactor the proof in non-trivial ways. As an example, Peter Scholes, who is a very well-known mathematician, came to the formal community and said, I have that new proof that I'm super excited about, but it's kind of complicated and I want to make sure that it's true. Please help me or please formalize it so that we can know for sure. And that effort, it's a kind of 10 dozen of page PhD of math, so it's not that big. And I think the effort took six months or a bit more to dozens of people. So it's not just translation because generally you have definitions that are missing and so you need to add them, you need to create the theories that are missing, etc. It's a very complicated book. And so that's one of the main differences between what we're doing and what a mathematician do actually. Today we are really focusing on proving theorems at fixed theories in a sense that we are tackling Olympiad problems for which we know that all the theorems and the definitions that we'll need are already proven in the formal system in a sense. But when a mathematician is doing his job, he's not spending his day proving stuff. What a mathematician do most is actually coming up with new definitions, new objects, finding correlations, finding a link between those definitions and those domains. That's something that we're actually not tackling at all today. We're really focusing on trying to solve exercise rather than creating new theories. And so the main thing is essentially knowing which tactic do I need to apply to use the existing theorems that I have or the existing concepts that I have in order to prove the particular statement. You say there are two main problems right here. So there's first this infinite action space thing. And this can be solved by having this search be guided by whatever language model you use. People I think know this from AlphaZero type algorithms, right, where we use some sort of a neural network to guide that search. And this is already a little bit in your previous work. But then the other thing you mentioned is you have no direct self-play setup, which obviously is very helpful in these types of automated things in these search procedures if you have like some adversary that's playing against you and both get better at the same time. So in this question here, you make a statement that says this paper focuses on the second problem. Our basis for addressing it is the observation that the key role of self-play is to provide an unsupervised curriculum. And the statement just kind of stands here as such. You kind of claim this. Do you want to comment maybe a little bit? I mean, it seems intuitive, right? But how do you arrive at this conclusion? So it's indeed more of an hypothesis than a strong statement. I totally admit and agree. We have some experimental evidence that if you think of AlphaZero, it's actually what's happening. But basically, if you take all the data that has been generated through a training loop of an AlphaGo type algorithm, if you take the final data set and train on it, you'll get the same performance as if you've been training sequentially basically. And so there is nothing kind of special in self-play episodes basically. It's more about generating the right data at the end. And I think it's not just about the difficulty, it's just about creating a lot of diverse data that explores the space quite nicely. And that kind of stems from having a player against which you're playing and by exploration, you dig a little bit and find new strategies that are interesting. And eventually, all that, if you accumulate all that, you train on that, you get a very good policy of value function. And I think that's why we say this is that the self-play that we have in two-player games is really about getting a data generation pipeline that generates good data, right? And that's why we call it an unsupervised curriculum. And in formal math, if you have a bunch of statements that you cannot prove because your program is just not good enough, you're just not going to get any data. You're going to just be stuck at that point. And so that's kind of the main difference. There is no way to reframe. I mean, there's no trivial or easy or obvious to me at least ways to reframe a problem that is just too hard into a set of easier problems. And it makes sense that you're trying to build up a curriculum, but also I've displayed this here with this sort of arrow of complexity that just gets more and more complex. But it is not really the case. It doesn't really look like this because complexity isn't just in one direction. It's not just a statement is more complex than another one, but there's also a direction. I think if I want to work myself up to prove, let's say, the whatever, general Riemann hypothesis or something like this, I can't just prove harder and harder statements in numerics or something because I really want to be in, I don't even know what category the Riemann hypothesis number theory or complex analysis. But the point is I can't just go about just proving any old theorems. I have to have some sort of a direction. So how does your... and you make a little bit of a point in manual curation might help here and so on. But what's the main force in your system driving sort of the direction that the system becomes an expert at? Because there's so many directions in math, right? It's impossible that it just becomes better, right? Yeah, so I mean, we took the very obvious and easy way. Basically you have in a with a formal system, you have a library of theorems that is actually with it. That's what the formal community generally working on. This is what we call mathlib. It's called mathlib in lean. And there is very few exercise or Olympiad type exercise, even exercise in mathlib. It's generally general purpose theorems, right? And so if you train on that data only, you're actually not that good at solving exercise because you haven't seen any. The very easy exercise you'll be able to solve, but the somewhat hard ones not at all. And so we had that mini F2F benchmark, which is made of exercise, Olympiad exercise that we cared about for many reasons that we can dive into. And so we took the easy way, which is let's just formalize a bunch of statements around that benchmark that we care about. And we did the most obvious thing is that we took the textbook that humans use to train for those competitions and formalize everything out of it. And we didn't ask ourselves much more questions than that. And the reason why it works is because it's a textbook. So there is a bunch of easy examples to begin with and the difficulty can have been proved nicely for humans. And so as we formalize the statements, we run our expectation loop on it. And as you mentioned in that illustration, you get a few statements first, but you retrain on them to get a few more, et cetera, et cetera. And as you do it, the way I visualize it is that you're really shifting the distribution of the model away from mathlib and towards mini F2F or towards the group of statements that you provided as a curriculum. And so that is that creation that gives the direction. In terms of direction, you're very right that it's a challenge. Something that you can do as an example with formalize is you can do forward proving. Instead of going backward, as you said, you take things that you know and try to compose them with theorems that unify to the things you know. And you keep going forward like that. And we've tried generating some data this way. And that data is actually, I mean, you cannot direct it easily. And so it goes a little bit all over the place. And we haven't found a way to make it beneficial for targeting a benchmark in particular that we care about. Do you see maybe a future where you mentioned the lack of self play, but there could be some sort of an agent that comes up with these intermediate statements, these these curriculum statements that sort of tries to guess, you know, maybe here is a statement that's kind of in between where you want to go and where you are currently. This could be some sort of, I mean, I'm never sure because a lot of times when people propose these agents, it's like, well, you if you have that agent, you've essentially solved the problem, right? But there could be some sort of thing that replaces you the human as who has to come up with this curriculum. But I guess it's a bit of a future thing. And the other avenue where I see sorry, so I'd like to jump on this one. Just for a second. It is plausible that we could build a model. I mean, it's theoretically plausible that we could build a model that creates those intermediate statements. There's two challenges here is the first one is that the number of statements that we have is actually extremely small. When you look at the proof data in formal math, and I didn't mention it before, right? It's also a good thing to mention it. One challenge of formal math is that data is extremely scarce. The proof data is scarce and the statement data is even scarcer. MassLib is something like 60k, 60k statements, 60k contexts, length things. And the curriculum we use is a few hundred. And so to train the agents to try to simplify statements, the data that you have access to is like in existence by standards, modern language modeling standards. So that's a really big challenge. One thing that I think is extremely exciting, that is, again, same idea, just make it simpler, is probably actually machine translation from informal statements to formal statements. Try the work that we've been doing, try to harvest a lot of informal statements that there are many more out there and try to auto formalize them. Formalizing a statement is actually much easier than formalizing a proof. It's still challenging, but definitely much easier. And no, no, no. Sorry for jumping in. So with respect to, yeah, I was also thinking, yeah, you could take all sort of the math that's out there, but yeah, that's obviously also curated by humans a little bit. The other point of controlling things would be the language model. There's a lot of work in prompt engineering and things like this. Now, your language model, maybe we can go a little bit into how you train and query the language model, which I think might, you know, might need or might benefit from a bit more explanation because I was quite vague here, right? But essentially you have two different types of inputs that you train the language model on. The one you call this proof step objective and the other one you call this proof size objective. And both of them, they have a declaration and the goal. Do you want to maybe give us a little bit, because for the declaration I was like, yeah, it's kind of like the things you have access to. Do you want to maybe give us a bit of insight into what these things are? Yeah, so if we go back to, if we think about your schema about proving backwards, so the goal is the current goal that you want to prove. The proof step is the tactic that you want to apply. So this is really mapping exactly the process of generating a tactic to try to simplify the current goal. Sorry, the goal, so if I'm here, right, the goal would be the top thing, this one right here and the tactic would be one node, one link to a sort of the next node. Okay. To a new goal. Yeah, exactly. But then this could also be the new goal and then these could be the proof steps or, okay, okay. Yes, exactly. In your, here the lines are the tactics and the circles are the goals. And in Lean you actually have just one goal, the tactic goes back to another goal because sometimes some tactic can create multiple sub goals, but because you could say, hey, I want to introduce that cut, the cut is kind of a mini conjecture inside a proof and, but Lean kind of stacks them together. So technically speaking, there's only one node at each end of each line. Okay. Yeah, exactly. The proof looks like a chain, the proof, the final proof looks like a chain. Okay. And the proof search looks like a tree. And so the, the, the decal, we condition on the decal name, so the decal name is the declaration name and it's simply the CRM name or the exercise name. And the, the motivation here is to provide a proxy information for the model as to what is the state of the formal environment at this stage, because the actual formal environment is gigantic. There's no easy way to represent it in a compact way. You have all the inputs, you have all the CRMs that have been defined in the same file before that very CRM, that the CRM you're trying to prove right now, you have a bunch of definitions, et cetera. And so the, if you wanted to represent that to the model, it's technically challenging and more importantly, it's really big. So instead we just give it the name of the CRM and we kind of hope that it'll provide signal as to, to the model as to what are the CRMs that it has access to for this one, because it's trained, it's trained on, on, on CRMs that are close to this one and the names of CRMs are somewhat similar and related. It was in the same file, et cetera, et cetera. So it's really kind of a trick to, to try to infuse a little bit of information about the environment. How can we imagine such a name? Is this like a human readable name or is this more like, you know, theorem two eight four five point eight? No, no, it's somewhat readable for the, for the experts at least it's in the floor smaller than floor positive. Some kind of stuff like that. It's, it's, it's a little bit compact, but it's still readable. And for the exercise that we use, it's actually just the name of the competition, the gear and the exercise number. And the proof step that would be the tactic itself. How is a tactic kind of described? Is this an index into some bucket or is it also a piece of text or? Yeah. So if you're scrolling the appendix, well, I describe it. The tactic is really a function call. You're calling the tactic, which is a meta program. So if you, yeah, as an example, this one apply tactic is very trivial. It just says, try to apply that serum to the current goal, but you have much more advanced tactics. And so that tactic takes an argument. So you not only have to pick your tactic, there's only a few of those, but you actually have to provide an argument. So here it's a serum name. There's many more, but still finite. This here is a theorem. And then you will, oh yeah, here you go. Yeah. Okay. Not prime. I see. Yeah. So that's a typical theorem. So that's the decoration name that we condition on if we wanted to try to prove it. And you have to apply it with here. It's applying the serum by providing a first argument to the serum and then looking at the one side only. And so all of that kind of explodes the action space, obviously. And the action space is actually infinite because some tactic has arguments, mathematical terms. And those mathematical terms, they don't necessarily exist in the context. If you're trying to prove an existential statement, often the easiest way is to provide a witness. The witness is not generally in the statements. And so you have to generate it. And so that's the reason why the action space is actually infinite. And that's the major difference between neural proving techniques and the kind of classical theorem proving automated reasoning techniques. They are extremely powerful, but there's one thing they cannot do. It's generating exogenous mathematical terms. And you would, in this case, your language model would directly suggest you such tactics to apply. So you would sample from the language model and then suggest a bunch of things. The language model generates the full string here, apply, netprime, hpmp. And so we generate a number of those that gives us an approximation of a potential interesting action space to explore. And on top of that, we run a proof search. How does the proof step come into this? Because I was a little bit... You already have some sort of a log likelihood estimation, I would guess, for the things that you sample. But then you also have this value, some sort of a value that you assign to how long you think a proof is going to be. Yeah. So the proof size objective takes the declaration name and the current goal and try to estimate the size of the proof for that goal. And that's really just an instance of a value function. That's the one that we've used here. And it really helps guiding the proof search. When you don't have the value function yet, so in your review, you mentioned that we bootstrap from theta zero, which is the first model that is only trained on proof steps. When we don't have a value function to available, what we do is that we do the same proof search, but we prioritize by log prob, as you said. But what we use is the cumulative log prob that took for us to apply the different tactics all the way to the current goal, which is another flavor of a value function. A bit of a beam search type. That is a... Yeah. Yeah, it's a beam tree depth search. Okay. And, okay, so I think we got a good idea of how the search itself works. And you keep going until you prove statements. And then you do this expert iteration steps, right? Which essentially consists of you try to prove new things, you add them back to the data set, and you train a new model on it. What I was kind of surprised by is that you always train from this sort of this initial model that you have right here. So you create your new data sets and you always train from that. What prevents you or what's the reasoning behind not always just continuing to train from the most recent model? Yeah, there's two motivations, two rational for that. The first one is that it makes controlling for overfit much easier because you're really training from scratch in a sense. And so you control overfit on your validation set much more cleanly. If you iteratively train the behavior of your validation loss, it has a tendency to be quite erratic and unpredictable, which makes controlling for overfit much less obvious. So that's the one thing, it's for basically scientific convenience in a sense. The other thing is that it gives us an opportunity to duplicate aggressively the data. The reason why it's important is because, to be honest, to generate those proofs, we sample proof search a lot. There are some easy statements, we can find thousands of different proofs for it. And so the goal is to retake all those proofs that we found so far and duplicate as much out of it to prevent nefarious overfitting behaviors in the training. So that's really the two main motivations for training from scratch. Again, formal math, data is scarce. So those data sets are not that big, even when we generate a lot of data. And so training is not taking that much time. So it's actually really fine to train from scratch in each iteration. One second. So you say you have easy statements, you're able to find a lot of proofs for them, you have hard statements, and that's difficult to reach. But you still said at the beginning, all the statements you are attempting to prove, you essentially already know that they're provable, right? And even the ones in the curriculum, the ones you take from the textbook, I think textbooks, they don't try to trick you with like exercises that ultimately don't really work out. What would change here if you were to go about proving something you don't know if it's even provable, right? Obviously, you also don't know the statements in between that might lead up to that. Like how would that look like to prove something that isn't proven yet? Okay, so I think there's two questions there. What would happen if you inject statements that are potentially false or even undecidable in the mix? And what would it take to try to prove something that we don't really know is provable yet? I think that's at least the way I understood the question. If we inject statements that are not provable, that are false or undecidable, same difference to us, at least in the context of one formal system, what happens is that nothing happens. There's no data generated. So you're just wasting compute. You're really just wasting compute on the statements. And that's going to be a challenge if we think back about automatizing the generation of statements, that's going to be a noisy imperfect process. And so whether it's going to be useful for that expectation process is really a function of the number of statements that are actually provable versus unprovable. If your automated translation system generates one out of 20 statements that is provable and 19 are unprovable, you're just going to be wasting a lot of computes trying to prove something that's not going to generate any data for you. So that's going to be a challenge there if we want to apply machine translation. And then proving something. What do you mean by proving something that's not always provable? Is it like trying to prove a conjecture? You want to train or you want to solve a conjecture that exists, but no one knows. We think it's provable, which we do with most conjectures, but no one knows. And now it's up to you and someone comes to you and says, well, let's use your system. How would you go about that? How would you build the curriculum? What would change maybe in the data collection? There are some conjectures that we can hope do not require inventing new math. So there may be some conjecture that are eluding humans despite being very close to us. It's just one trick away. And so for such conjecture and imagining a system that is much more powerful than what we have today, let's say it beats human at competitions, then you could just take your best system, take the conjecture and search for a lot of time. And you maybe have a hope of finding a proof that has eluded humans because it was really tricky but you didn't need new theorems. You didn't need new definitions. And for most of conjectures that are out there, there is good reason to believe, at least if we look at this directly, that they're going to require new mathematical concepts to be proved. And so that exercise, which is the mathematician's exercise of defining new concepts, is something that we're not even considering yet as a problem. It's a whole different problem. And to be honest, I think that it's a task that will probably more likely happen in the future in the informal realm more than in the formal realm. It feels like the informal realm seems to be a better space to try to come up with new concepts and maybe then we have good data formalization and then we can use a formal prover to prove all the things that we conjectured, etc. But that's something that is really far away from us. You could sort of abuse the language models maybe to go a step, let's say, further. You always have your declaration and your goal and you generate the proof step. Could you also maybe just input a declaration of a theorem name that you think might conceivably exist and then let the system come up with a goal by itself even? So like even the statement to be proven. We've tried that. It definitely works. You can let the model generate goals that are valid and that can then prove. You can even orient, we were talking about how do you orient your work towards stuff that interests you. You can definitely, in that case, you can definitely prompt the model where you're interested to explore by the declaration name. You can make up kind of funky names that look like analysis or funky names that look like group theory or even funky names that look like math Olympiads. The model will definitely and gladly conjecture statements. It's actually conjecturing all the time in a way that is not leverageable, unfortunately, when we do proof search. When we do proof search, the way we refer to theorems that exist is by declaration name, not by the statement themselves in Lean at least. All the time, every proof search, the model will just invent a theorem by name and the name look really legit. There should be math limb actually because it's just a missing API because the name, it's generally very interpretable, but the model sync should be there. That kind of conjecturing behavior really exists in the model today and is probably leverageable in interesting ways. It's a bit crazy because that is really how I think mathematicians go about proving something. They say they're at some statement and they say, well, here I need some inequality that relates these two things to each other. Essentially that is exactly coming up with a name of a theorem like this. The name would be something like, this greater than this or it's crazy. We actually can extract from math limb what we call the type elaboration. Type elaboration is to take a name of the theorem and you infer the type. The type is in type theory, the type is the statement itself. We can train models and type elaboration. We could have them conjecture names while we proof search and then take the name and try to type elaborate them. That gives us a statement and then try to prove that statement. That's something we haven't explored. It sounds crazy. Given the directions of these automated systems that can essentially generate data for themselves, if you introduce something like this, I'm pretty convinced this can get us a whole lot further. How fast have these Go and Chess algorithms become? They've become human and one month later they were totally superhuman. It happened in an instant, which is crazy. My question would be a little bit, this is a machine, the formal machine, you have the humans on the other side. Is there a good way of the two working together? It seems like they have complementary skills. One can search and try to prove things very quickly. The other one maybe has more of that idea, like introducing new math and so on. Is there a tight way where the two can work together or will it always be in the, well, we have to translate from one domain to the other? Definitely a way. We actually released our early models, it was almost a year ago, to the Lean community through a tactic that is called GPTF and so Formalizer could say GPTF and GPTF would answer with suggestions of things to try. It's broken and clunky in many ways and there's a technical challenge, which is that the mass library advances every day. It's the models are easy to, they can rot quite rapidly. For research purposes, it's very convenient for us to just say for the next three months, we're going to work on that commit and just not look at what's happening out there. But yet if you want to provide value to the community, you have to stay fresh, which is more of an engineering challenge than anything else. But it's definitely a plan to provide our models to the community. To be honest, anybody working on formal math and ML, think about that, that just makes sense. Because formalization is so, it's not that hard, but it's time consuming. So if our models can speed up formalization by another magnitude, that would be just tremendous. Right there, there's already a very nice symbiosis, as you say, because if we speed up formalization by 10x or by 2x, even by 2x, people will formalize much more stuff and we'll get much more data and we'll get better. It's a loop that goes through actually people committing stuff to Mathlib and us injecting it back eventually. So it's kind of a long, very long loop. It's a loop that we plan to try to set up. Yeah, I mean, I think that would be sort of the best case outcome right here, that there is like the symbiosis of just the machine helping the humans and so on, before it eventually will outperform them and make mathematicians useless. Oh yeah, we're far away from that anyway. Maybe last technical question from my side. It seems like in such an iteration process, you said, for example, you know, we can be easy statements, we can find thousands of proofs for them and you do some deduplication, right, to sort of reduce the number of proofs. If two proofs are equivalent, you take the shorter one, which is very sensible. But still, how do you avoid that most data that you add back to the data set is kind of useless? Because given like three basic facts, a mathematician can probably prove 16 things, right? And only very few of them are going to be valuable to advance towards my ultimate goals. Like how do you make sure that what you add back to the data set actually has some sort of value to the expert iteration? So the explosion of statements and proof that goes into a lot of noisy and uninteresting stuff generally comes when you do forward proving. If you do backward proving, you're really bounded by the statements you're trying to prove. So you might find thousands different proofs for something easy and all the thousands vary just because the model decided to name a variable differently and so they're not that interesting. And there we have much more work to do into having smarter deduplication. But really, in a sense, because that's the main advantage of working on formal math, because that data has been verified by the formal system, we know it's legit. It's one key massive advantage that we have to explore interesting research ideas compared to other domains is that we can lean on that verifier to really make sure that we only use legit data, even if it's the model that generated it. And I think that's key here. And generally speaking, empirically, it's always felt like the training, basically gradient descent is about compression and the training process is actually good at sifting through repetitive, not necessarily repetitive, but somewhat similar data. And so having a lot of different proofs is actually generally beneficial. I guess the story of deep learning is that the more the better, whatever it is. I've not gone too much into the results other than saying the expert iteration obviously helps you to prove much harder statements compared to just the solver, whether you adjust for a computer or not. It's also interesting that the larger models, whenever you scale up stuff, essentially, you get better. Is there anything in the experimental results that maybe I haven't touched on that you would like to highlight specifically? Well, I think you really covered it well. One result that I think you almost touched on, one question, and that is unanswered in the paper, is we do include the synthetic inequalities in the final experimental setup to target Mini F2F. And actually, I've run the ablation of that and they don't help that much on Mini F2F. I mean, it's not that much that surprising. So it's really, if you remove them and plot the curves against Mini F2F, you really get somewhat sensibly similar stuff. There is a few inequalities that have been solved that are challenging. And it's always a challenge because the graph tells you that it's roughly the same. But then when you look at the proof, you feel like it's been learned through the curriculum on synthetic inequalities. So that's the reason why we kind of kept it here. And I think it does unlock a few problems, but it's kind of a few problems at the margin. So it's hard to make sure by just looking at averages. And one interesting thing, of course, is as you say, you scale your compute, whether you scale in model size or you scale in number of atoms and you scale in depth of search, you always get better. It really seems to be, and I mean, it's true of most of recent deep learning, there really seems to be performance being really a function of computes that you efficiently pour into the system. Though we've been very surprised many times that model size scaling is hard to leverage. We know those larger models are so much smarter when you interact with them directly. You ask questions with GPT-3, it's qualitatively better than GPT-2, right? And here we are at the GPT-1 or 2 kind of size. And so common wisdom would say GPT-1 or 2, just dumb, right? So why not use GPT-3 size because we're talking about math. And really what we've seen empirically and that's probably and potentially because of bottlenecks in our setup that we haven't yet correctly identified, is that you don't need to have that big of a model to be efficient. It's actually detrimental to scale the model size because then your proof search becomes much more compute intensive. And in terms of Flop's allocation, it's much more efficient to sample many more times from a smaller models. It tells something quite interesting. It tells that the smaller model is basically is not completely, it's not much less smart than a larger model. It's just that the distribution is not as crisp. And here because we have the verifier and we can sample many times, we can choose the good samples out of a small model by trying many times. Maybe that becomes... It's only because we have a verifier.... go to like more like really hard math statements. Maybe at some point you really need sort of the large models, but who knows? Was there... I'm a bit interested also in the process of the research itself. Seeing a final paper is always really nice and cool and wow, you get to... your model does all this thing. Was there particular low points during the research as well, like particular moments where you think, this isn't going to work out after all or things like this? Maybe any you would like to share, maybe so that other people... It helps to identify because I think most people find themselves in spots like that. Yes, definitely. To be honest, I've been quite... We've been quite lucky with that project in the sense that there's been some low points, but at any point of time, looking back three months in the past, we always felt like we had made good motivating progress over those three months. But it's obviously been a lot of struggles at many times. I think research, at least the way I see it, is a lot about struggling for quite some time on some problems. There's a reason why you really want to care about the problem you're working on to be able to go through that struggle. It's actually the same as a startup in a sense. You really have to care enough to be able to go through the struggle. To give you an idea, I started working alone. There's no multiple people working on the project with me, but when I started, I really took a language model and I took a data set of tactics that I exported from... It was Metamask at the time. Nobody had any idea whether a language model was capable of generating a tactic because the syntax was so precise when you're talking about interacting with the formal system. There were no code generation results at the time. It really was an open question whether a language model is good enough to generate synthetically formal sentences in a sense. The first win was really that. Not only you train your model and start sampling and you just look at your sequence accuracy and you see that it's not zero. Right there, it doesn't prove anything and it's far from being able to prove anything, but it's a massive win. You're like, yes, language models can generate formal statements. That was really the start. I think leading to the first paper, the first GPTF paper, the two key moments where, okay, let's try to scale the model size and seeing that scaling is really beneficial. It's not, as we discussed, not as clear, but if you're just looking at performance in terms of model size, you see that very nice scaling if you don't adjust the compute basically. That's something that is quite motivating and exciting because it's the trend of the domain in many aspects. The key finding of the first paper that was really a motivation to continue working was that pre-training. You talked about that in the review and you had some questions, but that pre-training really helps a lot and transfers very beneficially to formal math. That's the bulk of that first paper. Then after the first paper, you're like, oh, we have a nice result. We've shown that language models can do some formal mathematics, but we were still completely unable to prove Olympiad's problems at all, even the really easy ones. That's really what we started working on. There, it's been also a long struggle, I think, until we just decided to bite the bullet and formalize some statements ourselves to generate that curriculum that really unlocks new capabilities and led to the work that we've shared. Is there anything about the paper that you want people to get away or to take away with? Maybe you can look also a little bit beyond math, like what does this tell us or anything you'd like people to know? The main takeaway I think I want to share is why we look at beyond math, but first it's why formal math is awesome. I think we covered that quite nicely, but to me, the main reason is that it's reasoning incomplete. If you get a really impressive result in formal math, you're really confident that you have a very impressive result in reasoning. Other interesting aspects of it is that it's inherently a safe setup. A lot of people are talking about safety, and that's a last harbor where we're not yet at all at human level, yet it's safe to try to push as hard as you can because it's like games. But in a formal system, there is no escape hatch. And finally, the reason why I think it's so exciting is because it lets you combine a language model with a formal verifier. And so you're really getting the best of both worlds. You have language models that are really impressive into what they can generate, but even GPT-3, if you give it a few deductive steps, it falls off really rapidly. And so they are capable of one-step reasoning that are interesting, but not multi-step reasonings. And so that's when you tie it with a verifier that you can basically get the value of multi-step reasoning by interacting with the verifier that is here to verify the prediction. And that's, I think, what is really exciting here. The verifier kind of almost gives you the internal monologue that humans have when they think. It's hard to imagine a language model thinking hard during the duration of one context size, right? Yet here, we do have that kind of property, which is exciting. And finally, the reason why I'm super excited about it goes beyond mass, in a sense. I think that's the reason why it's really... OpenAI is really a great place to work on that because it's really aligned with our mission and how we want to execute it. The reason why is that I think if we crack formal mass, we really will be providing a blueprint on how to infuse much more reasoning in large informal language models. And so I really see it as kind of a small experimental lab where we can study reasoning when we know that reasoning is kind of still lacking in those very large language models. And so that's really that that excites me and I think it will transfer nicely. You have formal mass, you have code generation in the middle because you have unit tests, but beyond unit tests, you cannot know for sure that your program is correct. And then you have fully informal setups where you just cannot verify your predictions. I think that wraps it up pretty nicely. Stan, thank you very much for being here. This was really cool.
 Hello there, this is an interview with the first author of the paper, Formal Mathematics
 Statement Curriculum Learning, in which an automated system was able to solve two problems
 of the International Mathematics Olympiad.
 Now, this is an unprecedented level of skill in formal mathematics for an AI system.
 The system uses language models in combination with a technique called expert iteration to
 build itself a harder and harder curriculum of theorems to prove.
 Now, if you haven't seen it, I've made a comprehensive paper review about this paper in the last
 video.
 So be sure to check that out because Stan, the author who I'm interviewing today, has
 seen that video.
 So we all start from a common level.
 Stan is able to directly respond to any criticisms and questions that I had during the paper
 review.
 And we go into the details into the behind the scenes of the research, what didn't work
 out what problems came up, how the project came to be and what this all means beyond
 the domain of mathematics.
 It is a huge privilege to have the authors of these papers on here.
 And I want to get the most information that I can out of them.
 So please let me know how I can improve these videos.
 Let me know in the comments, leave a like if you like and I'll see you around.
 Bye.
 All right, everyone.
 Hi.
 So we're here with Stan Polu, who is the first author of the formal mathematics statement
 curriculum learning of the paper that uses expert iteration to end up proving two IMO
 problems, which I think was was very well received by everyone in the community.
 And we're going to look at the paper, going to go maybe through some of my criticisms
 that I had and that I just threw out there.
 And yeah, we're going to have we're going to hopefully inform everyone a little bit
 more.
 Stan, welcome to the channel.
 Thank you, Yannick.
 Thank you very much for having me.
 It's a pleasure to be here.
 So this this obviously the paper, it helps that OpenAI is as a name on the paper, right?
 It gives it like a little bit of a boost in publicity, but still it was the reception
 was quite widespread, I want to say, even though it appeared, I think in the same week
 as some other big papers, like I think AlphaCode was in the same week or so.
 Yet still you made quite an impression on people.
 And do you have an idea of why sort of the paper was widely received?
 There have been other papers in this domain, but this was kind of special.
 What's your impression?
 Yeah.
 So, so first, yeah, you mentioned I work at OpenAI, just to give you a little bit of context.
 So I'm a research engineer at OpenAI.
 OpenAI is focused on building and deploying safe and beneficial AI systems.
 It's a bit part research lab and part deployment company and I myself focus on the research
 lab part.
 The release was actually the same day as AlphaCode.
 We actually decided to go for it right after the release that work and I think it was just
 fine.
 We did release a first paper before the first GPTF paper, which is reference from that paper
 a year ago.
 And it didn't have much support from OpenAI because it was kind of a shadow release.
 We just put the paper up there, it was a blog post.
 And it did bring quite a lot of interest as well.
 I think people are interested in the domain because mass seems like a frontier that we
 haven't reached yet.
 And so any progress in that direction seems is probably exciting to most other people
 in the community.
 That would be my kind of main understanding of as to why people reacted positively and
 are engaging with the work.
 So you were already in this domain, you said, and I think I've also commented on this a
 little bit.
 You had previous work in using language models to guide these provers.
 Was this sort of a natural continuation for that?
 Or was there some impulse behind you tackling sort of these more challenging problems?
 Yes, it's really a continuation of the previous work.
 And actually, to give you a little bit of color on all of that, I joined OpenAI two
 years ago, and I actually wanted to work on formal math and AI before I joined OpenAI.
 And I did have quite an original trajectory within the field.
 I don't have a PhD in machine learning.
 I don't have a PhD at all, actually.
 And I was actually a software engineer at Stripe before and eventually wanted to work
 on subjects that pertain to AI and decided that formal math was the things that I wanted
 to work on.
 And then I found that it was well aligned with OpenAI mission and the way we were executing
 it.
 And so I joined and shortly after started working on it.
 So I've actually been working on this for the last two years.
 And that paper is really a continuation of the first paper.
 It's just kind of a real continuous work that we are tackling.
 And I think we'll definitely continue working on that because those two problems are quite
 impressive, but we're still far away from being at best students level.
 It is to some extent mind blowing because that system can prove statements that I'm
 actually myself not capable of proving.
 I'm not a math competitor, but I did do quite a lot of math studying for engineering school
 in France.
 And there are some things that I just can't prove and that this system can prove.
 But at the same time, there's so many stuff that I find easy and this kind of proven.
 So we were still a long way away from being able to be at best human level.
 But still those progress have been really continuous and continuously exciting over
 the past two years.
 You've seen my explanation of the paper.
 And I think with this paper specifically, I'm not that much of an expert in the domain
 itself.
 So I'm not too much into formal math and these sort of proving algorithms, how provers even
 work.
 I've tried to explain that a little bit by building this proof tree right here.
 Do you maybe have any more comments, any insights that could help people understand what is
 formal math even?
 How does it look from the inside?
 What is the main problem?
 How do you do things there?
 Of course.
 To be honest, you really made the explanation.
 It was really clear and I think it's a really good explanation of what's happening.
 Formal math was kind of invented when computers came out.
 The main problem that it tries to solve is that when you have a math paper and a very
 impressive proof, you only have generally a few people in the world that can review
 that proof because those proof are generally so complicated that only a few people can
 just understand those.
 And so there's actually no way to be sure that those massive proof are indeed true.
 That's kind of annoying because we're talking about mathematics supposed to be rock solid,
 yet it's not the case because those subjects are so advanced.
 And so the motivation for formal math is to say, well, let's actually encode math for
 computers so that computers can check every step.
 And we're going to get rid of that problem and forever be confident in our math progress.
 The only caveat is that because people working in formal math needs to reformat the proof
 in a way that computers can pass, despite a lot of automation that helps in that process,
 it's still a very, very, very time consuming effort.
 And so the advance of formalization of math concepts has been lagging behind the state
 of the art in math tremendously, but it's still starting to pick up, especially in Lean,
 where we've seen some recent formalization of very advanced and new work.
 But the main problem of formal math, I think, is that it's really hard to formalize.
 And so what is formalization like?
 It's exactly as you stated.
 You basically state your statements.
 Stating statements once you have the right definitions is almost natural.
 It feels a bit complicated when you look at the statements from the paper, as you mentioned,
 but it's actually close to what you would write in English.
 But then the proof is really completely different because you really have to contrive it in
 a way that the computer can understand.
 And the way it works is, as you mentioned, it's really an interaction between the human
 and the machine.
 You have that first statement, which is your goal.
 You apply some tactics, which are the automation I mentioned, to try to help in the formalization.
 To generally provide some direction to tactics.
 And tactics are meta programs that are taking your directions and trying to generate proof
 terms, which are much lower level artifacts that are understood by the machine.
 So they bridge between the human and the machine.
 And you keep going like that.
 You generally know the informal proof, of course.
 You generally have to change it in non-trivial ways to make it provable with all the theories
 you have available and the constraint of the formal system.
 And eventually you keep making progress like that with trial and error.
 So you have the feedback from the formal system, which are your current goals, and you try
 and make progress this way until you, as you mentioned, you reach something that you know
 is true because it's already been proven or it's an axiom or it's an hypothesis.
 You mentioned right now that people formalize by already sort of knowing the proof from
 the math domain, maybe.
 Are there people that seriously prove things for the first time in the formal way?
 Or is it largely just a translation effort?
 Because I'm wondering the way your system works in proof searching, this is not necessarily
 this paper alone, but it seems to me proof searching, what it does is it simply traverses
 the tree of all possible kind of like a chess engine or so would do something like this.
 And I'm wondering if you think that is similar to how humans try to go about proving mathematical
 concepts or is there some fundamental difference on how the machine does it and how the humans
 do it?
 In my opinion, there are some similarities and some massive difference.
 If you know what the proof is already, it looks a little bit like a translation exercise,
 but one that is quite challenging because you really have to generally refactor the
 proof in non-trivial ways.
 As an example, Peter Scholes, who is a very well-known mathematician, came to the formal
 community and said, I have that new proof that I'm super excited about, but it's kind
 of complicated and I want to make sure that it's true.
 Please help me or please formalize it so that we can know for sure.
 And that effort, it's a kind of 10 dozen of page PhD of math, so it's not that big.
 And I think the effort took six months or a bit more to dozens of people.
 So it's not just translation because generally you have definitions that are missing and
 so you need to add them, you need to create the theories that are missing, etc.
 It's a very complicated book.
 And so that's one of the main differences between what we're doing and what a mathematician
 do actually.
 Today we are really focusing on proving theorems at fixed theories in a sense that we are
 tackling Olympiad problems for which we know that all the theorems and the definitions
 that we'll need are already proven in the formal system in a sense.
 But when a mathematician is doing his job, he's not spending his day proving stuff.
 What a mathematician do most is actually coming up with new definitions, new objects, finding
 correlations, finding a link between those definitions and those domains.
 That's something that we're actually not tackling at all today.
 We're really focusing on trying to solve exercise rather than creating new theories.
 And so the main thing is essentially knowing which tactic do I need to apply to use the
 existing theorems that I have or the existing concepts that I have in order to prove the
 particular statement.
 You say there are two main problems right here.
 So there's first this infinite action space thing.
 And this can be solved by having this search be guided by whatever language model you use.
 People I think know this from AlphaZero type algorithms, right, where we use some sort
 of a neural network to guide that search.
 And this is already a little bit in your previous work.
 But then the other thing you mentioned is you have no direct self-play setup, which
 obviously is very helpful in these types of automated things in these search procedures
 if you have like some adversary that's playing against you and both get better at the same
 time.
 So in this question here, you make a statement that says this paper focuses on the second
 problem.
 Our basis for addressing it is the observation that the key role of self-play is to provide
 an unsupervised curriculum.
 And the statement just kind of stands here as such.
 You kind of claim this.
 Do you want to comment maybe a little bit?
 I mean, it seems intuitive, right?
 But how do you arrive at this conclusion?
 So it's indeed more of an hypothesis than a strong statement.
 I totally admit and agree.
 We have some experimental evidence that if you think of AlphaZero, it's actually what's
 happening.
 But basically, if you take all the data that has been generated through a training loop
 of an AlphaGo type algorithm, if you take the final data set and train on it, you'll
 get the same performance as if you've been training sequentially basically.
 And so there is nothing kind of special in self-play episodes basically.
 It's more about generating the right data at the end.
 And I think it's not just about the difficulty, it's just about creating a lot of diverse
 data that explores the space quite nicely.
 And that kind of stems from having a player against which you're playing and by exploration,
 you dig a little bit and find new strategies that are interesting.
 And eventually, all that, if you accumulate all that, you train on that, you get a very
 good policy of value function.
 And I think that's why we say this is that the self-play that we have in two-player games
 is really about getting a data generation pipeline that generates good data, right?
 And that's why we call it an unsupervised curriculum.
 And in formal math, if you have a bunch of statements that you cannot prove because your
 program is just not good enough, you're just not going to get any data.
 You're going to just be stuck at that point.
 And so that's kind of the main difference.
 There is no way to reframe.
 I mean, there's no trivial or easy or obvious to me at least ways to reframe a problem that
 is just too hard into a set of easier problems.
 And it makes sense that you're trying to build up a curriculum, but also I've displayed this
 here with this sort of arrow of complexity that just gets more and more complex.
 But it is not really the case.
 It doesn't really look like this because complexity isn't just in one direction.
 It's not just a statement is more complex than another one, but there's also a direction.
 I think if I want to work myself up to prove, let's say, the whatever, general Riemann hypothesis
 or something like this, I can't just prove harder and harder statements in numerics or
 something because I really want to be in, I don't even know what category the Riemann
 hypothesis number theory or complex analysis.
 But the point is I can't just go about just proving any old theorems.
 I have to have some sort of a direction.
 So how does your... and you make a little bit of a point in manual curation might help
 here and so on.
 But what's the main force in your system driving sort of the direction that the system becomes
 an expert at?
 Because there's so many directions in math, right?
 It's impossible that it just becomes better, right?
 Yeah, so I mean, we took the very obvious and easy way.
 Basically you have in a with a formal system, you have a library of theorems that is actually
 with it.
 That's what the formal community generally working on.
 This is what we call mathlib.
 It's called mathlib in lean.
 And there is very few exercise or Olympiad type exercise, even exercise in mathlib.
 It's generally general purpose theorems, right?
 And so if you train on that data only, you're actually not that good at solving exercise
 because you haven't seen any.
 The very easy exercise you'll be able to solve, but the somewhat hard ones not at all.
 And so we had that mini F2F benchmark, which is made of exercise, Olympiad exercise that
 we cared about for many reasons that we can dive into.
 And so we took the easy way, which is let's just formalize a bunch of statements around
 that benchmark that we care about.
 And we did the most obvious thing is that we took the textbook that humans use to train
 for those competitions and formalize everything out of it.
 And we didn't ask ourselves much more questions than that.
 And the reason why it works is because it's a textbook.
 So there is a bunch of easy examples to begin with and the difficulty can have been proved
 nicely for humans.
 And so as we formalize the statements, we run our expectation loop on it.
 And as you mentioned in that illustration, you get a few statements first, but you retrain
 on them to get a few more, et cetera, et cetera.
 And as you do it, the way I visualize it is that you're really shifting the distribution
 of the model away from mathlib and towards mini F2F or towards the group of statements
 that you provided as a curriculum.
 And so that is that creation that gives the direction.
 In terms of direction, you're very right that it's a challenge.
 Something that you can do as an example with formalize is you can do forward proving.
 Instead of going backward, as you said, you take things that you know and try to compose
 them with theorems that unify to the things you know.
 And you keep going forward like that.
 And we've tried generating some data this way.
 And that data is actually, I mean, you cannot direct it easily.
 And so it goes a little bit all over the place.
 And we haven't found a way to make it beneficial for targeting a benchmark in particular that
 we care about.
 Do you see maybe a future where you mentioned the lack of self play, but there could be
 some sort of an agent that comes up with these intermediate statements, these these curriculum
 statements that sort of tries to guess, you know, maybe here is a statement that's kind
 of in between where you want to go and where you are currently.
 This could be some sort of, I mean, I'm never sure because a lot of times when people propose
 these agents, it's like, well, you if you have that agent, you've essentially solved
 the problem, right?
 But there could be some sort of thing that replaces you the human as who has to come
 up with this curriculum.
 But I guess it's a bit of a future thing.
 And the other avenue where I see sorry, so I'd like to jump on this one.
 Just for a second.
 It is plausible that we could build a model.
 I mean, it's theoretically plausible that we could build a model that creates those
 intermediate statements.
 There's two challenges here is the first one is that the number of statements that we have
 is actually extremely small.
 When you look at the proof data in formal math, and I didn't mention it before, right?
 It's also a good thing to mention it.
 One challenge of formal math is that data is extremely scarce.
 The proof data is scarce and the statement data is even scarcer.
 MassLib is something like 60k, 60k statements, 60k contexts, length things.
 And the curriculum we use is a few hundred.
 And so to train the agents to try to simplify statements, the data that you have access
 to is like in existence by standards, modern language modeling standards.
 So that's a really big challenge.
 One thing that I think is extremely exciting, that is, again, same idea, just make it simpler,
 is probably actually machine translation from informal statements to formal statements.
 Try the work that we've been doing, try to harvest a lot of informal statements that
 there are many more out there and try to auto formalize them.
 Formalizing a statement is actually much easier than formalizing a proof.
 It's still challenging, but definitely much easier.
 And no, no, no.
 Sorry for jumping in.
 So with respect to, yeah, I was also thinking, yeah, you could take all sort of the math
 that's out there, but yeah, that's obviously also curated by humans a little bit.
 The other point of controlling things would be the language model.
 There's a lot of work in prompt engineering and things like this.
 Now, your language model, maybe we can go a little bit into how you train and query
 the language model, which I think might, you know, might need or might benefit from a bit
 more explanation because I was quite vague here, right?
 But essentially you have two different types of inputs that you train the language model
 on.
 The one you call this proof step objective and the other one you call this proof size
 objective.
 And both of them, they have a declaration and the goal.
 Do you want to maybe give us a little bit, because for the declaration I was like, yeah,
 it's kind of like the things you have access to.
 Do you want to maybe give us a bit of insight into what these things are?
 Yeah, so if we go back to, if we think about your schema about proving backwards, so the
 goal is the current goal that you want to prove.
 The proof step is the tactic that you want to apply.
 So this is really mapping exactly the process of generating a tactic to try to simplify
 the current goal.
 Sorry, the goal, so if I'm here, right, the goal would be the top thing, this one right
 here and the tactic would be one node, one link to a sort of the next node.
 Okay.
 To a new goal.
 Yeah, exactly.
 But then this could also be the new goal and then these could be the proof steps or, okay,
 okay.
 Yes, exactly.
 In your, here the lines are the tactics and the circles are the goals.
 And in Lean you actually have just one goal, the tactic goes back to another goal because
 sometimes some tactic can create multiple sub goals, but because you could say, hey,
 I want to introduce that cut, the cut is kind of a mini conjecture inside a proof and, but
 Lean kind of stacks them together.
 So technically speaking, there's only one node at each end of each line.
 Okay.
 Yeah, exactly.
 The proof looks like a chain, the proof, the final proof looks like a chain.
 Okay.
 And the proof search looks like a tree.
 And so the, the, the decal, we condition on the decal name, so the decal name is the declaration
 name and it's simply the CRM name or the exercise name.
 And the, the motivation here is to provide a proxy information for the model as to what
 is the state of the formal environment at this stage, because the actual formal environment
 is gigantic.
 There's no easy way to represent it in a compact way.
 You have all the inputs, you have all the CRMs that have been defined in the same file
 before that very CRM, that the CRM you're trying to prove right now, you have a bunch
 of definitions, et cetera.
 And so the, if you wanted to represent that to the model, it's technically challenging
 and more importantly, it's really big.
 So instead we just give it the name of the CRM and we kind of hope that it'll provide
 signal as to, to the model as to what are the CRMs that it has access to for this one,
 because it's trained, it's trained on, on, on CRMs that are close to this one and the
 names of CRMs are somewhat similar and related.
 It was in the same file, et cetera, et cetera.
 So it's really kind of a trick to, to try to infuse a little bit of information about
 the environment.
 How can we imagine such a name?
 Is this like a human readable name or is this more like, you know, theorem two eight four
 five point eight?
 No, no, it's somewhat readable for the, for the experts at least it's in the floor smaller
 than floor positive.
 Some kind of stuff like that.
 It's, it's, it's a little bit compact, but it's still readable.
 And for the exercise that we use, it's actually just the name of the competition, the gear
 and the exercise number.
 And the proof step that would be the tactic itself.
 How is a tactic kind of described?
 Is this an index into some bucket or is it also a piece of text or?
 Yeah.
 So if you're scrolling the appendix, well, I describe it.
 The tactic is really a function call.
 You're calling the tactic, which is a meta program.
 So if you, yeah, as an example, this one apply tactic is very trivial.
 It just says, try to apply that serum to the current goal, but you have much more advanced
 tactics.
 And so that tactic takes an argument.
 So you not only have to pick your tactic, there's only a few of those, but you actually
 have to provide an argument.
 So here it's a serum name.
 There's many more, but still finite.
 This here is a theorem.
 And then you will, oh yeah, here you go.
 Yeah.
 Okay.
 Not prime.
 I see.
 Yeah.
 So that's a typical theorem.
 So that's the decoration name that we condition on if we wanted to try to prove it.
 And you have to apply it with here.
 It's applying the serum by providing a first argument to the serum and then looking at
 the one side only.
 And so all of that kind of explodes the action space, obviously.
 And the action space is actually infinite because some tactic has arguments, mathematical
 terms.
 And those mathematical terms, they don't necessarily exist in the context.
 If you're trying to prove an existential statement, often the easiest way is to provide a witness.
 The witness is not generally in the statements.
 And so you have to generate it.
 And so that's the reason why the action space is actually infinite.
 And that's the major difference between neural proving techniques and the kind of classical
 theorem proving automated reasoning techniques.
 They are extremely powerful, but there's one thing they cannot do.
 It's generating exogenous mathematical terms.
 And you would, in this case, your language model would directly suggest you such tactics
 to apply.
 So you would sample from the language model and then suggest a bunch of things.
 The language model generates the full string here, apply, netprime, hpmp.
 And so we generate a number of those that gives us an approximation of a potential interesting
 action space to explore.
 And on top of that, we run a proof search.
 How does the proof step come into this?
 Because I was a little bit...
 You already have some sort of a log likelihood estimation, I would guess, for the things
 that you sample.
 But then you also have this value, some sort of a value that you assign to how long you
 think a proof is going to be.
 Yeah.
 So the proof size objective takes the declaration name and the current goal and try to estimate
 the size of the proof for that goal.
 And that's really just an instance of a value function.
 That's the one that we've used here.
 And it really helps guiding the proof search.
 When you don't have the value function yet, so in your review, you mentioned that we bootstrap
 from theta zero, which is the first model that is only trained on proof steps.
 When we don't have a value function to available, what we do is that we do the same proof search,
 but we prioritize by log prob, as you said.
 But what we use is the cumulative log prob that took for us to apply the different tactics
 all the way to the current goal, which is another flavor of a value function.
 A bit of a beam search type.
 That is a...
 Yeah.
 Yeah, it's a beam tree depth search.
 Okay.
 And, okay, so I think we got a good idea of how the search itself works.
 And you keep going until you prove statements.
 And then you do this expert iteration steps, right?
 Which essentially consists of you try to prove new things, you add them back to the data
 set, and you train a new model on it.
 What I was kind of surprised by is that you always train from this sort of this initial
 model that you have right here.
 So you create your new data sets and you always train from that.
 What prevents you or what's the reasoning behind not always just continuing to train
 from the most recent model?
 Yeah, there's two motivations, two rational for that.
 The first one is that it makes controlling for overfit much easier because you're really
 training from scratch in a sense.
 And so you control overfit on your validation set much more cleanly.
 If you iteratively train the behavior of your validation loss, it has a tendency to be quite
 erratic and unpredictable, which makes controlling for overfit much less obvious.
 So that's the one thing, it's for basically scientific convenience in a sense.
 The other thing is that it gives us an opportunity to duplicate aggressively the data.
 The reason why it's important is because, to be honest, to generate those proofs, we
 sample proof search a lot.
 There are some easy statements, we can find thousands of different proofs for it.
 And so the goal is to retake all those proofs that we found so far and duplicate as much
 out of it to prevent nefarious overfitting behaviors in the training.
 So that's really the two main motivations for training from scratch.
 Again, formal math, data is scarce.
 So those data sets are not that big, even when we generate a lot of data.
 And so training is not taking that much time.
 So it's actually really fine to train from scratch in each iteration.
 One second.
 So you say you have easy statements, you're able to find a lot of proofs for them, you
 have hard statements, and that's difficult to reach.
 But you still said at the beginning, all the statements you are attempting to prove, you
 essentially already know that they're provable, right?
 And even the ones in the curriculum, the ones you take from the textbook, I think textbooks,
 they don't try to trick you with like exercises that ultimately don't really work out.
 What would change here if you were to go about proving something you don't know if it's even
 provable, right?
 Obviously, you also don't know the statements in between that might lead up to that.
 Like how would that look like to prove something that isn't proven yet?
 Okay, so I think there's two questions there.
 What would happen if you inject statements that are potentially false or even undecidable
 in the mix?
 And what would it take to try to prove something that we don't really know is provable yet?
 I think that's at least the way I understood the question.
 If we inject statements that are not provable, that are false or undecidable, same difference
 to us, at least in the context of one formal system, what happens is that nothing happens.
 There's no data generated.
 So you're just wasting compute.
 You're really just wasting compute on the statements.
 And that's going to be a challenge if we think back about automatizing the generation of
 statements, that's going to be a noisy imperfect process.
 And so whether it's going to be useful for that expectation process is really a function
 of the number of statements that are actually provable versus unprovable.
 If your automated translation system generates one out of 20 statements that is provable
 and 19 are unprovable, you're just going to be wasting a lot of computes trying to prove
 something that's not going to generate any data for you.
 So that's going to be a challenge there if we want to apply machine translation.
 And then proving something.
 What do you mean by proving something that's not always provable?
 Is it like trying to prove a conjecture?
 You want to train or you want to solve a conjecture that exists, but no one knows.
 We think it's provable, which we do with most conjectures, but no one knows.
 And now it's up to you and someone comes to you and says, well, let's use your system.
 How would you go about that?
 How would you build the curriculum?
 What would change maybe in the data collection?
 There are some conjectures that we can hope do not require inventing new math.
 So there may be some conjecture that are eluding humans despite being very close to us.
 It's just one trick away.
 And so for such conjecture and imagining a system that is much more powerful than what
 we have today, let's say it beats human at competitions, then you could just take your
 best system, take the conjecture and search for a lot of time.
 And you maybe have a hope of finding a proof that has eluded humans because it was really
 tricky but you didn't need new theorems.
 You didn't need new definitions.
 And for most of conjectures that are out there, there is good reason to believe, at least
 if we look at this directly, that they're going to require new mathematical concepts
 to be proved.
 And so that exercise, which is the mathematician's exercise of defining new concepts, is something
 that we're not even considering yet as a problem.
 It's a whole different problem.
 And to be honest, I think that it's a task that will probably more likely happen in the
 future in the informal realm more than in the formal realm.
 It feels like the informal realm seems to be a better space to try to come up with new
 concepts and maybe then we have good data formalization and then we can use a formal
 prover to prove all the things that we conjectured, etc.
 But that's something that is really far away from us.
 You could sort of abuse the language models maybe to go a step, let's say, further.
 You always have your declaration and your goal and you generate the proof step.
 Could you also maybe just input a declaration of a theorem name that you think might conceivably
 exist and then let the system come up with a goal by itself even?
 So like even the statement to be proven.
 We've tried that.
 It definitely works.
 You can let the model generate goals that are valid and that can then prove.
 You can even orient, we were talking about how do you orient your work towards stuff
 that interests you.
 You can definitely, in that case, you can definitely prompt the model where you're interested
 to explore by the declaration name.
 You can make up kind of funky names that look like analysis or funky names that look like
 group theory or even funky names that look like math Olympiads.
 The model will definitely and gladly conjecture statements.
 It's actually conjecturing all the time in a way that is not leverageable, unfortunately,
 when we do proof search.
 When we do proof search, the way we refer to theorems that exist is by declaration name,
 not by the statement themselves in Lean at least.
 All the time, every proof search, the model will just invent a theorem by name and the
 name look really legit.
 There should be math limb actually because it's just a missing API because the name,
 it's generally very interpretable, but the model sync should be there.
 That kind of conjecturing behavior really exists in the model today and is probably
 leverageable in interesting ways.
 It's a bit crazy because that is really how I think mathematicians go about proving something.
 They say they're at some statement and they say, well, here I need some inequality that
 relates these two things to each other.
 Essentially that is exactly coming up with a name of a theorem like this.
 The name would be something like, this greater than this or it's crazy.
 We actually can extract from math limb what we call the type elaboration.
 Type elaboration is to take a name of the theorem and you infer the type.
 The type is in type theory, the type is the statement itself.
 We can train models and type elaboration.
 We could have them conjecture names while we proof search and then take the name and
 try to type elaborate them.
 That gives us a statement and then try to prove that statement.
 That's something we haven't explored.
 It sounds crazy.
 Given the directions of these automated systems that can essentially generate data for themselves,
 if you introduce something like this, I'm pretty convinced this can get us a whole lot
 further.
 How fast have these Go and Chess algorithms become?
 They've become human and one month later they were totally superhuman.
 It happened in an instant, which is crazy.
 My question would be a little bit, this is a machine, the formal machine, you have the
 humans on the other side.
 Is there a good way of the two working together?
 It seems like they have complementary skills.
 One can search and try to prove things very quickly.
 The other one maybe has more of that idea, like introducing new math and so on.
 Is there a tight way where the two can work together or will it always be in the, well,
 we have to translate from one domain to the other?
 Definitely a way.
 We actually released our early models, it was almost a year ago, to the Lean community
 through a tactic that is called GPTF and so Formalizer could say GPTF and GPTF would answer
 with suggestions of things to try.
 It's broken and clunky in many ways and there's a technical challenge, which is that the mass
 library advances every day.
 It's the models are easy to, they can rot quite rapidly.
 For research purposes, it's very convenient for us to just say for the next three months,
 we're going to work on that commit and just not look at what's happening out there.
 But yet if you want to provide value to the community, you have to stay fresh, which is
 more of an engineering challenge than anything else.
 But it's definitely a plan to provide our models to the community.
 To be honest, anybody working on formal math and ML, think about that, that just makes
 sense.
 Because formalization is so, it's not that hard, but it's time consuming.
 So if our models can speed up formalization by another magnitude, that would be just tremendous.
 Right there, there's already a very nice symbiosis, as you say, because if we speed up formalization
 by 10x or by 2x, even by 2x, people will formalize much more stuff and we'll get much more data
 and we'll get better.
 It's a loop that goes through actually people committing stuff to Mathlib and us injecting
 it back eventually.
 So it's kind of a long, very long loop.
 It's a loop that we plan to try to set up.
 Yeah, I mean, I think that would be sort of the best case outcome right here, that there
 is like the symbiosis of just the machine helping the humans and so on, before it eventually
 will outperform them and make mathematicians useless.
 Oh yeah, we're far away from that anyway.
 Maybe last technical question from my side.
 It seems like in such an iteration process, you said, for example, you know, we can be
 easy statements, we can find thousands of proofs for them and you do some deduplication,
 right, to sort of reduce the number of proofs.
 If two proofs are equivalent, you take the shorter one, which is very sensible.
 But still, how do you avoid that most data that you add back to the data set is kind
 of useless?
 Because given like three basic facts, a mathematician can probably prove 16 things, right?
 And only very few of them are going to be valuable to advance towards my ultimate goals.
 Like how do you make sure that what you add back to the data set actually has some sort
 of value to the expert iteration?
 So the explosion of statements and proof that goes into a lot of noisy and uninteresting
 stuff generally comes when you do forward proving.
 If you do backward proving, you're really bounded by the statements you're trying to
 prove.
 So you might find thousands different proofs for something easy and all the thousands vary
 just because the model decided to name a variable differently and so they're not that interesting.
 And there we have much more work to do into having smarter deduplication.
 But really, in a sense, because that's the main advantage of working on formal math,
 because that data has been verified by the formal system, we know it's legit.
 It's one key massive advantage that we have to explore interesting research ideas compared
 to other domains is that we can lean on that verifier to really make sure that we only
 use legit data, even if it's the model that generated it.
 And I think that's key here.
 And generally speaking, empirically, it's always felt like the training, basically gradient
 descent is about compression and the training process is actually good at sifting through
 repetitive, not necessarily repetitive, but somewhat similar data.
 And so having a lot of different proofs is actually generally beneficial.
 I guess the story of deep learning is that the more the better, whatever it is.
 I've not gone too much into the results other than saying the expert iteration obviously
 helps you to prove much harder statements compared to just the solver, whether you adjust
 for a computer or not.
 It's also interesting that the larger models, whenever you scale up stuff, essentially,
 you get better.
 Is there anything in the experimental results that maybe I haven't touched on that you would
 like to highlight specifically?
 Well, I think you really covered it well.
 One result that I think you almost touched on, one question, and that is unanswered in
 the paper, is we do include the synthetic inequalities in the final experimental setup
 to target Mini F2F.
 And actually, I've run the ablation of that and they don't help that much on Mini F2F.
 I mean, it's not that much that surprising.
 So it's really, if you remove them and plot the curves against Mini F2F, you really get
 somewhat sensibly similar stuff.
 There is a few inequalities that have been solved that are challenging.
 And it's always a challenge because the graph tells you that it's roughly the same.
 But then when you look at the proof, you feel like it's been learned through the curriculum
 on synthetic inequalities.
 So that's the reason why we kind of kept it here.
 And I think it does unlock a few problems, but it's kind of a few problems at the margin.
 So it's hard to make sure by just looking at averages.
 And one interesting thing, of course, is as you say, you scale your compute, whether you
 scale in model size or you scale in number of atoms and you scale in depth of search,
 you always get better.
 It really seems to be, and I mean, it's true of most of recent deep learning, there really
 seems to be performance being really a function of computes that you efficiently pour into
 the system.
 Though we've been very surprised many times that model size scaling is hard to leverage.
 We know those larger models are so much smarter when you interact with them directly.
 You ask questions with GPT-3, it's qualitatively better than GPT-2, right?
 And here we are at the GPT-1 or 2 kind of size.
 And so common wisdom would say GPT-1 or 2, just dumb, right?
 So why not use GPT-3 size because we're talking about math.
 And really what we've seen empirically and that's probably and potentially because of
 bottlenecks in our setup that we haven't yet correctly identified, is that you don't need
 to have that big of a model to be efficient.
 It's actually detrimental to scale the model size because then your proof search becomes
 much more compute intensive.
 And in terms of Flop's allocation, it's much more efficient to sample many more times from
 a smaller models.
 It tells something quite interesting.
 It tells that the smaller model is basically is not completely, it's not much less smart
 than a larger model.
 It's just that the distribution is not as crisp.
 And here because we have the verifier and we can sample many times, we can choose the
 good samples out of a small model by trying many times.
 Maybe that becomes...
 It's only because we have a verifier.
... go to like more like really hard math statements.
 Maybe at some point you really need sort of the large models, but who knows?
 Was there... I'm a bit interested also in the process of the research itself.
 Seeing a final paper is always really nice and cool and wow, you get to... your model
 does all this thing.
 Was there particular low points during the research as well, like particular moments
 where you think, this isn't going to work out after all or things like this?
 Maybe any you would like to share, maybe so that other people...
 It helps to identify because I think most people find themselves in spots like that.
 Yes, definitely.
 To be honest, I've been quite...
 We've been quite lucky with that project in the sense that there's been some low points,
 but at any point of time, looking back three months in the past, we always felt like we
 had made good motivating progress over those three months.
 But it's obviously been a lot of struggles at many times.
 I think research, at least the way I see it, is a lot about struggling for quite some time
 on some problems.
 There's a reason why you really want to care about the problem you're working on to be
 able to go through that struggle.
 It's actually the same as a startup in a sense.
 You really have to care enough to be able to go through the struggle.
 To give you an idea, I started working alone.
 There's no multiple people working on the project with me, but when I started, I really
 took a language model and I took a data set of tactics that I exported from...
 It was Metamask at the time.
 Nobody had any idea whether a language model was capable of generating a tactic because
 the syntax was so precise when you're talking about interacting with the formal system.
 There were no code generation results at the time.
 It really was an open question whether a language model is good enough to generate synthetically
 formal sentences in a sense.
 The first win was really that.
 Not only you train your model and start sampling and you just look at your sequence accuracy
 and you see that it's not zero.
 Right there, it doesn't prove anything and it's far from being able to prove anything,
 but it's a massive win.
 You're like, yes, language models can generate formal statements.
 That was really the start.
 I think leading to the first paper, the first GPTF paper, the two key moments where, okay,
 let's try to scale the model size and seeing that scaling is really beneficial.
 It's not, as we discussed, not as clear, but if you're just looking at performance in terms
 of model size, you see that very nice scaling if you don't adjust the compute basically.
 That's something that is quite motivating and exciting because it's the trend of the
 domain in many aspects.
 The key finding of the first paper that was really a motivation to continue working was
 that pre-training.
 You talked about that in the review and you had some questions, but that pre-training
 really helps a lot and transfers very beneficially to formal math.
 That's the bulk of that first paper.
 Then after the first paper, you're like, oh, we have a nice result.
 We've shown that language models can do some formal mathematics, but we were still completely
 unable to prove Olympiad's problems at all, even the really easy ones.
 That's really what we started working on.
 There, it's been also a long struggle, I think, until we just decided to bite the bullet
 and formalize some statements ourselves to generate that curriculum that really unlocks
 new capabilities and led to the work that we've shared.
 Is there anything about the paper that you want people to get away or to take away with?
 Maybe you can look also a little bit beyond math, like what does this tell us or anything
 you'd like people to know?
 The main takeaway I think I want to share is why we look at beyond math, but first it's
 why formal math is awesome.
 I think we covered that quite nicely, but to me, the main reason is that it's reasoning
 incomplete.
 If you get a really impressive result in formal math, you're really confident that you have
 a very impressive result in reasoning.
 Other interesting aspects of it is that it's inherently a safe setup.
 A lot of people are talking about safety, and that's a last harbor where we're not yet
 at all at human level, yet it's safe to try to push as hard as you can because it's like
 games.
 But in a formal system, there is no escape hatch.
 And finally, the reason why I think it's so exciting is because it lets you combine a
 language model with a formal verifier.
 And so you're really getting the best of both worlds.
 You have language models that are really impressive into what they can generate, but even GPT-3,
 if you give it a few deductive steps, it falls off really rapidly.
 And so they are capable of one-step reasoning that are interesting, but not multi-step reasonings.
 And so that's when you tie it with a verifier that you can basically get the value of multi-step
 reasoning by interacting with the verifier that is here to verify the prediction.
 And that's, I think, what is really exciting here.
 The verifier kind of almost gives you the internal monologue that humans have when they
 think.
 It's hard to imagine a language model thinking hard during the duration of one context size,
 right?
 Yet here, we do have that kind of property, which is exciting.
 And finally, the reason why I'm super excited about it goes beyond mass, in a sense.
 I think that's the reason why it's really...
 OpenAI is really a great place to work on that because it's really aligned with our mission
 and how we want to execute it.
 The reason why is that I think if we crack formal mass, we really will be providing a
 blueprint on how to infuse much more reasoning in large informal language models.
 And so I really see it as kind of a small experimental lab where we can study reasoning
 when we know that reasoning is kind of still lacking in those very large language models.
 And so that's really that that excites me and I think it will transfer nicely.
 You have formal mass, you have code generation in the middle because you have unit tests,
 but beyond unit tests, you cannot know for sure that your program is correct.
 And then you have fully informal setups where you just cannot verify your predictions.
 I think that wraps it up pretty nicely.
 Stan, thank you very much for being here.
 This was really cool.