The $64M Bet on an AI That Has to Be Right | Carina Hong, CEO of Axiom

Formal verification already consumes years of human effort. In this episode, Lukas Biewald talks with Carina Hong, Founder & CEO of Axiom, about why verification is becoming the real bottleneck in high stakes AI systems. They discuss how Axiom uses AI to take on the tedious checking that stretches verification cycles across years, starting with formal mathematics and extending to hardware and software. Carina also explains why Axiom’s approach to auto-formalization mirrors spec driven models like Kiro from AWS. Connect with us here: Carina Hong: https://www.linkedin.com/in/carina-hong/ Axiom:https://www.linkedin.com/company/axiommath/ Lukas Biewald: https://www.linkedin.com/in/lbiewald/ Weights & Biases: https://www.linkedin.com/company/wandb/

Speaker names marked ? are inferred from speaking time and the show’s known hosts — they are not voice-verified.

• 0:00Speaker 00

  Axiom's mission is to build a reasoning engine that is self-improving and that combines generation and verification.

• 0:06Lukas Biewald?

  For Putnam, for people who aren't like math nerds, there's like a contest among math undergraduates. That's incredibly hard. The median score is like a zero.

• 0:12Speaker 00

  We recently, Axiom Pro, we got eight out of 12. We use formal languages like Lean to ground the natural language counterpart. And because we are doing that, we witnessed the power of deterministic tooling and probabilistic system working together.

• 0:27Lukas Biewald?

  You were on an academic path and now you're running this company. What made you decide to shift gears like this?

• 0:33Speaker 00

  When I was five, I would listen to like underground rock and roll music. They are obviously very politically rebellious and also like the contrarian appeal. I do think that this startup is like really fun as in it's such a brand new adventure. And you're a bit living like the rock and roll day every day.

• 0:50Lukas Biewald?

  What do you really predict for mathematics going forward?

• 0:53Speaker 00

  Mathematicians will learn to work on a different abstraction than they are used to before. And so if you're a great mathematician, just let your intuition take you to wherever you want and have the AI mathematician be the diligent grad student trying to prove the intuitions you have.

• 1:12Lukas Biewald?

  You're listening to Gradient Dissent, a show about making machine learning work in the real world. And I'm your host, Lukas Biewald. Carina Hong is the CEO and founder of Axiom Math, which is a company that calls itself a self-reasoning system and is currently on the cutting edge of building an AI mathematician. They've had astonishingly strong results on Math Olympiad problems and recently got the highest score on the Putnam test, which we talk about. Karina is super interesting. She was a star academic mathematician, now turned into a founder. Axiom Math came out of stealth, having raised $64 million. She talks in detail about how Axiom works, how she think it applies to more than math over time,

• 1:57Lukas Biewald?

  and also how rock and roll or hardcore rock and roll music in China influenced her thinking around management and staying hungry. I hope you enjoy this interview.

• 2:08Lukas Biewald?

  Karina, why don't we start by the most basic question, which is what is Axiom? And how does it work at a high level?

• 2:16Speaker 00

  Yeah, so Axiom's mission is to build a reasoning engine that is self-improving, and that combines like generation and verification, which we think is like an overlooked component in the current AI landscape. And we want to start with an AI mathematician, because math is a really good testing ground for this sort of self-help loop. We use formal languages like Lean to ground the natural language counterpart. And because we are doing that, there are a lot of, you know, interesting capabilities we can unlock with much higher sample efficiency. So the general, I think, vision of Axiom is there is a prover, you

• 2:58Speaker 00

  know, a system that can prove theorems, and also a conjecturer, so a system that can propose interesting conjectures, and they talk to each other. And they talk to each other, you have this third component called knowledge base. So if I am a prover, then I would like to know sort of what are already proven and what I can use. I would also, if I'm a conjecturer, like to stress test whether this conjecture is reasonable. So perhaps some counter example will help me out by just not suggesting that at all. I mean, the knowledge base is a very, very important component, you know, kind of supporting these two. And then auto-formalization, which is the system that can, you know, automatically

• 3:39Speaker 00

  formalize natural language stuff into formal language stuff. It's kind of weaving all three. So that's kind of the basic setup of Axiom.

• 3:47Lukas Biewald?

  So can we like break it down in the context of, you know, something simple that everyone, you know, could understand, like, you know, like take like, you know, if we're going to try to prove like Isagrian theorem, you know, for example, assuming if it's not in your knowledge database, like, how would that, how would that actually work practically?

• 4:04Speaker 00

  Right, so I think if it's um Pythagorean theorem, which is I think already proven, like hopefully I think that

• 4:11Lukas Biewald?

  Those times, yeah.

• 4:12Speaker 00

  Just do it. But if we do, you know, like a de novo math problem, like we recently, Action Pruer um got really strong score, winning score on Punam exam twenty twenty twenty six, because they name it, it's in December, they name it by the next year.

• 4:27Lukas Biewald?

  So you beat everyone on them?

• 4:29Speaker 00

  So we, within the exam time limit, we got eight out of twelve.

• 4:33Lukas Biewald?

  Amazing.

• 4:34Speaker 00

  We are going to announce, you know, our actual final score, but we also announced nine out of twelve, because I think the ninth problem came two hours after my tweet, which is a little bit awkward, so you're like, oh, wait a second, everyone, don't, don't repost that tweet, you know, repost this one.

• 4:48Lukas Biewald?

  Nice, nice.

• 4:49Speaker 00

  Uh, but

• 4:50Lukas Biewald?

  Sort of breaking news here on this podcast, yeah.

• 4:52Speaker 00

  Yeah, nine, nine out of twelve was, nine out of twelve was last year's number one among all human, four thousand human participants. Um, and it's Punam fellow, which is top honor, top five, um, every year, like almost every year consistently, beyond some years where the problem some, somehow got really easy. Um, this year's Punam, we, we find that result very encouraging, um, especially given that the, you know, final proof release, we're gonna say kind of exactly how many were solved. Um, so I think that's very uh exciting. We, we kind of, I think, witness the power of deterministic uh tooling and probabilistic system that kind of working together and, and the capability out of because of that.

• 5:34Lukas Biewald?

  Okay, so

• 5:34Speaker 00

  And so, sorry, go back to your question.

• 5:36Lukas Biewald?

  Maybe we just say first of all, so for Punam, for people who aren't like, you know, math nerds, is like a contest among, I think, math undergraduates, that's incredibly hard, right? I think the, the median score is like a zero, and it's like the best, you know, math undergrads are like doing it, so it's, you know, getting um, any of the problems right is a, is a real accomplishment, and, and beating everyone is kind of amazing, right? Like, all the best mathematicians did super well on this stuff. Tell me if, if I, if that's a good description.

• 6:00Speaker 00

  Yeah, that's right. I, I personally got a, you know, much worse score than, than, than, than our, our pruer system, so it's a, it's a very interesting.

• 6:08Lukas Biewald?

  Wait, let's brag a little bit, what did you get?

• 6:10Speaker 00

  Yeah, well, so I, so I got four out of twelve, uh, which, you know, it's, it's not that great. I got some top two fifty honorable mention only, so not, not necessarily, but, and, and that's like, you know, Action Pruer's final score will potentially triple me, so. Um, and, and, and I think we should have a beat Karina kind of party, which is, which is always fun.

• 6:32Lukas Biewald?

  You know, I've noticed, um, Like using L L M's, like, say, like, you know, G P T or Gemini or whatever directly without your, you know, your technology, they seem, you know, kind of surprisingly good, maybe it's sort of like Math Olympiad kind of question, not the part of them, but you know, the scores are like, wow, you know, this is like pretty impressive. But then, you know, I think I have a mutual friend, Robert Nishihara, I think, you know, anyway, he's, he's given me a bunch of different,

• 7:03Lukas Biewald?

  he kind of brain teaser questions. And, you know, one of them I got with, and it was a pretty simple, you know, kind of fun question. I put it in, you know, G P T and Gemini, and it actually couldn't solve it.

• 7:14Speaker 00

  Couldn't do it? Oh, interesting.

• 7:15Lukas Biewald?

  Interesting, like, you know, like, you know, to me, like, you know, Math Olympiad is so much harder than the kinds of like, you know, questions you might get in a Google interview. But it seems like maybe for L L M's, they don't have the same hierarchy of difficulty. Like, do you have an intuition for like, what's easy and what's hard for? And your system's similar, like, would you find maybe some things that might feel more trivial to like a junior mathematician, hard for your?

• 7:45Speaker 00

  I think, I think it's fascinating to kind of think about, like, you know, L L M's doing things like math and sometimes in safety critical domains, code, in some cases, like high stakes scenarios, writing code statistically just doesn't work in a way that you want to make sure that you have provable guarantee of edge cases. This is similar to, say, in math, like, a proof is a proof. It must be sort of sound proof and, and not have any, you know, like, critical flaw. I think that, which is why I think like informal, kind of scaling the informal models to math A G I just isn't something that we believe in. I think that as to certain, like,

• 8:28Speaker 00

  different math questions, it's very, you know, easy to make a case for those that require, like, say, you know, the very fine grained checking, those things I think Ling will be very good at. For things that rely on, like, high level intuitions and probably don't have the sort of detailed part, I think the recent or the informal model will probably have a pretty good contribution. Um. When it comes to I think computations, I think that certain tools are probably helpful. Like, you know, the Mathematica sector, like these plugins. Uh, I think just it it's very interesting to see, for example, like a simple positivity argument in analysis.

• 9:12Speaker 00

  Uh, we're actually planning to do a put an improved release and commentary so that we are kind of looking at each problem and uh how the AI solve it, whether that's expected, um given how a human might think about it. The analysis part, you can see like the AI are doing a lot of work for something that the human student or, you know, researcher would just write off. Uh, it will it will like do like chunks of code to rigorously ensure that, you know, things around convergence, exacture limit are very carefully handled. And that is actually why the initial days of MATLAB, uh, funny enough, um, the undergraduate algebra text are all formalized, like rather straightforward slash quickly.

• 9:55Speaker 00

  And it took them a long time to do the analysis. Analysis and algebra are usually the two subjects for the undergrad um level. I actually found the graph that I would like to show. Okay, so basically what I'm talking about is this is not a problem. This is a, this is Erdos problem four hundred and eighty-one. Um, a Twitter user, I think, a uh, you know, undergraduate math student uh, solved this problem uh by himself and then um, very excited about it and post about it. And then I think we are trying to kind of see whether our system can solve it as well, just as like a, you know, Twitter daily engagement thing. And this is what the system does.

• 10:36Speaker 00

  It kind of break down into different um subgoals, results or lemmas um that will, it actually start from like this one being not green and then, you know, until everything is like hit green at the very end. Every other node is hit green, this node will turn green.

• 10:53Lukas Biewald?

  Do you um, like, can you turn that into something that's like interpretable by um by a human?

• 11:01Speaker 00

  Uh, yes, I think you can. I mean, in fact, the the goal is for each of the node, you can click into it and then you will see the link code. And because auto informalization, which is converting lean back into natural language, is significantly easier than the other way, auto formalization. And I think this because like people have seen a lot of like models have seen a lot of English, not a lot of lean. So one direction, it's like in translation days, I think from, you know, English to another very niche language, like there's one direction that's significantly easier. So I think, yes, in in fact, I think you can poke into it, that that will be something very exciting for someone to sort of interact with the system when it's doing the proving work.

• 11:44Lukas Biewald?

  Cool. I mean, I want to ask you, one of the things that I noticed with you know, code generation is it seems like L L M's today are better at you know, generating code that works than generating, you know, code that feels like easily interpretable by a human. It's really makes sense with like the reinforcement learning that surely, you know, they're they're using. And I would think that you might have a similar issue where, you know, generating like lean that like, you know, is like proves to be true. It's probably easier to check than like, could a human like, understand it? And I would think your models would probably generate things in different ways than humans. And I feel like already some of the more technical math proofs are really hard to, you know, to process. Do you think that?

• 12:24Speaker 00

  Yeah.

• 12:25Lukas Biewald?

  I don't know. Do you think we're entering a world where models might like prove the Riemann hypothesis, but no one can understand, you know, everyone might agree with every step. No one can like actually get an intuition for what happened.

• 12:36Speaker 00

  Right, right. So I think it's a it's a fascinating question, because if, say, a human proved Riemann hypothesis, in certain cases, I remember back then when Yitan Zhao, Professor Yitan Zhao announced he proved a math result.

• 12:53Speaker 00

  People were not sure what happened either. I think they kind of very quickly assembled an expert panel. And I was at Oxford at the time. So some of the professor I was intervening with were telling us about how they got caught together to try to examine the proof. And because certain mathematicians write in a way that's very obscure, the experts couldn't quite, you know, immediately know what's going on either. So I think I will start with that. I do think that for Lean proofs, which have this sort of verifiability, you know, feature, it's really good, good news. Because if you imagine, like, suppose GPT one day produce a 10,000 line Lean proof,

• 13:37Speaker 00

  claiming that it has solved an open conjecture, especially because it's trained, you know, trained on like chain of thought data among other things. We really can't be sure. So I think the scenario happened in 2024, so December 2024, about the 2025 put them. I remember Dan Hendrix posted on Twitter about, hey, I feed these problems into, I think it was O1 Pro or O3 Pro Preview, I forget, I forget. And then O3 Preview. And then people were like grading those model outputs, widely different grades. Like, no one in the Twitter commentary area was able to say for sure whether that's a correct solution or not. The consensus was something like, no, it's not correct.

• 14:20Speaker 00

  Because for all these problems, there's like a significant hole that the model tried to hand wave. The, the, the power of formal systems, you cannot hand wave. In fact, it's doing a little bit too much of the opposite, which is that it's, it's almost annoying that it's like rigorously checking down to every fine-grained detail, like the convergence and limit. Like, I'm like, you really don't need to spend that amount of, you know, space to, to prove the simple positivity lemma. But, but it does, and it's actually one of the heaviest node in the proof graph that we produce. So I think that's, that's interesting. So you have that sort of, at least, peace of mind. When it comes to elegance and intuition, I do think, first of all, for a lot of the problems,

• 15:02Speaker 00

  it is very hard to produce humans or sort of just the intellectual, you know, ceiling, very hard to produce two proofs. So if someone tells me that, hey, I have two proofs for Riemann hypothesis, I think that's like a much more unlikely statement than say I have one proof of Riemann. Like, there are certain problems that you just feel like, you know, there is bound to be one proof. So that would probably mean that what the AI finds, you know, minus the part where it might be doing redundant stuff, like, it might be like, you know, repeating the same thing again and again. You can call that ugly. But if you kind of take those out, the streamlined version of that, it could, there's a good case to be made that it might be convergent to what a human would possibly find. And I think that's extremely exciting.

• 15:45Speaker 00

  So kind of treating AI as not some sort of second-class citizen, but as just another, like, you know, mathematician collaborator, maybe one that you have not heard of. Maybe it's like similar to the Ramanujan case, where Hardy and Littlewood at Cambridge just discovered this self-taught genius from India. I do think that's a very interesting mindset to think about AI, you know, mathematician. And, and I also, speaking of here, I also found the other, like, kind of proof tree. So I'm, I'm sorry for like the, I hope this can be cut out. Okay, so I'm sharing the host screen again. So this is how like the system is proving problem A1.

• 16:27Speaker 00

  And then there are problems. This is like a really complicated one. Obviously, it's not proving it this fast. We kind of have like a time acceleration. But, um, and I think this, this is like, if I don't refresh it, it kind of, yeah. So this is what it's doing. I don't know how I can make this easier for.

• 16:47Lukas Biewald?

  Like, one of the button questions, just so people can see, like, what that looks like?

• 16:51Speaker 00

  Yeah.

• 16:53Speaker 00

  I think I can. A3 is like a problem where people can definitely understand. You know, it's like a game problem where Alice and Bob, you know, the standard Alice and Bob, plays a game for a string of N, N numbers, and then it can only be zero, one, or two. And in the, in the beginning, everything's zero, that's the start state. And then so you can, you know, at each move, either add or subtract one from one digit to create like. A new string that has not appeared before. Um. If you cannot do that, um, as in like you have run out of uh all the possible strings, then the other player wins and Alice always goes first. So um kind of which player has a winning strategy?

• 17:36Speaker 00

  That's like a standard sort of game theory problem um in competition math. And uh I think a lot of the, you know, students when look at it will probably have about two or three, you know, very um, you know, widely used results in competition math to to kind of attack this kind of problem. So for example, you are guaranteed, I think, in a game of no ties, you know, a winning strategy. Um. And then so it's just like which player, which is what is asking. And then like I think students will try to kind of write down the string and imagine they are Alice or Bob to try to see, you know, how they would attack the game and try to see if there's any pattern they can find.

• 18:17Speaker 00

  So this is really the part about like intuition discovery. So, you know, I I if I'm Alison or Bob, like, what would I do? And I think people, you know, actually solving the problem will try to figure out, hey, are there certain states that are just a lot worse than others? So if I'm, you know, faced with like a string, um, I would probably think that if I have, you know, zero on one number, then I I cannot subtract, right? I can only add. Um. And then if I have two, I cannot add. So like potentially one, you know, at a place will give me a lot more flexibility and try to kind of like generalize these sort of really bad states or some really good states into, you know, determining the sequence of things or, you know, what the rational

• 19:00Speaker 00

  move for the the the the opponent is when I kind of um put them in in that situation. So I think these are very interesting sort of like, it's a very fun problem. And there are obviously more tedious problems, like um if you look at say like A two and um B two, there's a lot of calculus involved because Pan Am is the hardest um undergraduate level exam, unlike the I M O being high school level um calculus is seen. And I think for people who are very proficient with um integration, I don't think. A two or B two will pose any significant challenge. However, for the axiom prover, I don't think it's challenging at all, but it just does take a lot of lines of link code to solve some of the, you know, take it as a given issues.

• 19:44Speaker 00

  For some cases, we have the, you know, AI proof very different, very different sort of thing. As in like have a very different solution from what our human mathematician experts expect, which is, you know, the most fun to watch cases.

• 19:58Lukas Biewald?

  Well, so let's talk about A three, because that's a great one, right? It's so easy to understand, like where my brain goes is like, okay, like, let me try one. Like, it looks like, you know, all you can do is add one. So Alice adds one, now you get one. Obviously, Bob can't subtract one, so Bob adds one. Okay, so player two wins, I guess, right? Is that like, is that accurate? Actually, first of all.

• 20:20Speaker 00

  Sorry, so you say player two.

• 20:22Lukas Biewald?

  So Alice's first thing can add one to get one, and then Bob goes and adds one and gets two.

• 20:28Speaker 00

  Yeah.

• 20:28Lukas Biewald?

  And then.

• 20:29Speaker 00

  Yeah, I think, I think, I think, I think that's, that's right. So actually, Bob always wins.

• 20:34Lukas Biewald?

  Bob wins at one.

• 20:36Speaker 00

  Yeah, there is a very clean, like, winning strategy for Bob that can be described like succinctly. So if you, once you see it, like, Bob doesn't need to respond with much care to, you know, Alice moves at all, which is, I think, what's kind of making this problem slightly easier than I would say a last, you know, pun and problem level. So it's, it's only A three. So there are six problems for each session. Usually we'll expect four, five, six to be harder than one, two, three, I would say. And yeah, so basically Bob can just execute that strategy without thinking much. So that makes it also much more trackable for a lean as well. So there's like very little state to track and there's no like complicated branching to reason about.

• 21:17Lukas Biewald?

  But I guess like I don't, you know, like when I, I mean, it's always dangerous to like introspect your own brain here, right? But like, I, I think that this human approach here is to like, kind of like think about cases, kind of like look for like a strategy that makes sense. Not like, you know, formal mathematical proof. So is, do you think that axiom is actually like taking a different approach than a human approach or?

• 21:42Speaker 00

  You mean for this, for this problem?

• 21:44Lukas Biewald?

  For the specific A3 problem, yeah.

• 21:46Speaker 00

  For this specific A3 problem, I would say that it's kind of, you know, aligned, like how the AI think about this problem and how humans think about it. There are other like, you know, scenarios where we can see the sort of AI taking a different path from, from humans. Because like it knows that it can kind of brute force through things where the human, if you are like, you know, actual task taker and you want to avoid brute force, if you know the brute force might not work, like if you don't, as in like, if I'm in, you know, doing Euclidean geometry problem and I have no idea how to solve this and I know that brute, brute force is kind of the complex coordinate method like can definitely get me there.

• 22:30Speaker 00

  I am probably willing to sink one hour into brute forcing that, but not necessarily for some of the non-geometry cases. I think the, the human will find a clever sort of one diagram proof even.

• 22:46Lukas Biewald?

  So that's a good segue. I mean, I want to ask you about the, you know, the applications of this, like, like what are the, like, what, are there like milestones along the way? I mean, you know, my former, you know, CRO is, is on your board and, and one of your investors. I'm kind of curious like how you, you know, pitched this, you know, math element to.

• 23:06Speaker 00

  Yeah, I think people saw it themselves as well. So this is something that I find really amazing is that when I'm talking to investors, there are real intellectual alignments like with certain fonts. I think fonts even have internal memo, like just marking that this category is, it's not even like a category where it's good to battle. It's something that they consider inevitable to, to the future. So if you think about like the lag of verification and hardware and software, where design teams are one third or one fourth of the size of verification teams. Verification could take, as I said, three years in the hardware scenario.

• 23:48Speaker 00

  And if you think about in software, for example, before we have a lot of the prosumers, people who are native programmers using. Various sorts of coding models like Cursor. But there's like, you know, a lot of need for code review. And in kind of safety critical cases, I do think that customers, enterprise are facing this really, you know, unfortunate choice between, hey, I just want this to not be wrong. So I might have just a human to eyeball or like manually do it instead of relying on AI to do it. But that's also very painful for the reasons we kind of described, like the time, the resources, the inability, how unaccessible certain experts are.

• 24:33Speaker 00

  So like, I think the difference between the high, you know, expertise, like formal verification expert in chips and like a medium expertise one, if you can somehow, you know, make it a case that the AI can handle the, the, the, the very sort of notorious cases. And so you lower the bar for hiring. I think that would also be incredibly valuable. For example, I think for, I see that AWS, which has like the, you know, one of the best automated reasoning teams, took some, I think, five years to formalize the memory isolation component of the hypervisor by hand.

• 25:11Speaker 00

  That's a shocking number. It's not the entire hypervisor, it's one part. I think also with now kind of more vibe coding and more like agents generating code, verifying that the edge cases are covered, it's gonna be also very important. Another, I think, use case is code migration. So if you have legacy code and you want to make sure that, hey, this new code, I want to upgrade it and I want to, you know, make sure this new code are completely equivalent to my legacy code. No, it's not doing better, it's not doing worse, like, because those legacy code are serving important business functions. That's another very interesting use case.

• 25:52Speaker 00

  In the database scenario, if there are like bad actor, then sort of, you know, proving that, you know, it is, it is actually consistent. So there's kind of, currently databases are kind of sharded from each other and they are, you know, inconsistent in that sense because they have this sort of, you know, problem where there might be bad actor. All these can be, you know, the sort of formal verification can provide a very interesting solution too.

• 26:22Lukas Biewald?

  Yeah, I mean, I guess like, you know, in the domains that like I'm more, you know, familiar with in software, I feel like the, um, you know, the, the test cases are not quite as black and white as like with the formal proof. And it might be like kind of over constrained. Or I think the real challenge would be like, you know, formalizing, you know, what it means to be wrong, you know, clearly enough that you could actually.

• 26:48Speaker 00

  Yeah, I do. I do think it's very interesting in that, you know, I think for the database case specifically, um, I think having some sort of, you know, abstraction that is easy to interface with will be, I think, a big unlock. So, um, basically what I think is going on is that there are certain like use cases where this is a dire need, like we really, really need to verify everything, maybe because, you know, regulation like kind of, you know, like mandates that maybe because I just can't put that into deployment. So currently we're having humans to do it to make sure that like, to the best extent possible, we are everything soundproof. And then there are kind of like good to have cases that it's really, really good to have, say, in the database case. And I think like

• 27:33Speaker 00

  if you don't have it, maybe we can live without. But like, obviously, I think having it and that's like kind of a weighing of like, you know, how painful it is to use versus how much like capability, um, like, you know, it will unlock when I use it. Um, I think all these are like interesting trade off. And then there's like this final group of maybe, you know, like web coding, like a lovable website wouldn't necessarily need formal verification. I don't think, just like, you know, the AI mathematician we are building cannot write poetry. I think there is like this sort of like three tier thing. And our goal is obviously to start from the first tier and then like kind of like eventually take second. And I think like by the time we take the second kind of group, it will

• 28:14Speaker 00

  be like a big moment in, in just the broader landscape of AI, like much beyond math. You think about. For example, right, like if I, in the, in the first case, what is an example? If there's like a proof of the consistency of the Paxos protocol, you know, like written by, say, like Leslie Lampard, and then you can like auto-formalize that both in link of the proof and also part of this formalization, the system can generate a code in a strongly typed language, like Rust, for example, to execute this protocol. This sort of unifying of generation at like, I think like, what is the implementation and the verification in one is going to be a powerful idea.

• 28:58Speaker 00

  And then, you know, one question you might ask is like, how much can I kind of migrate that from, not migrate necessarily, but extend that from Rust to some weekly type languages? And kind of trying to slowly close the gap, knowing that, you know, it's not possible to formally verify our code in, in Python, like, but you can do a majority of it. And, you know, which programming language will be people's choice is also by itself an uncertain question.

• 29:24Speaker 00

  So I think, I think kind of like, and then talking about the, you know, the, the sort of, you know, trip verification use cases. I think that like in 1980s, for example, a lot of trip companies tried to do for verification was humans who are very good at writing their improving languages, right, in, in like much more ancient counterpart of lean. And then, you know, back then it didn't quite scale because obviously I think the, you know, humans are a bit, you know, that's a bottleneck factor. Perhaps like AI formal verification can have a huge comeback here at Axiom, starting with an AI mathematician.

• 30:02Lukas Biewald?

  Yeah, it's funny. I mean, it feels very old fashioned in a way, right? Like I remember, you know, in like the 90s, there was a lot of enthusiasm around the sort of like formal, you know, proving in AI. And you don't hear about it much, you know, the last few decades. It's kind of interesting. I imagine you're probably pulling things, you know, from the 80s and 90s in terms of this like searching over theorems and trying to. Trying to build proofs.

• 30:24Speaker 00

  I I think there are a lot more like modern research as well on the, I think specifically the timing of like reasoning models, code generation ability, having great, you know, improvement, applying RL in a verifiable domain. And the, you know, Lean becoming a widely celebrated language with more developers than ever excited about it, mathematicians willing to embrace it. I think all these three things coming together make now a really good timing in these sort of software and hardware verification landscape. In software, for example, there's CSlib that is under development. You know, I think Stanford's Automated Reasoning Lab, led by Professor Clark Barrett, is doing

• 31:09Speaker 00

  it, supported by industry partners such as DeepMind and AWS. They are trying to formalize all the CS literature undergrad in Lean. There are people trying to kind of formalize machine learning things in Lean. It's a very sort of interesting moment, I think, that we are living in. Kind of going back to the database, I do, I do, I'm curious about your thought, right? Like, for example, I think all databases have to solve the Byzantine general problem, like consistency of those solutions need to be formally proven. Don't know if like something like that being, is that of interest or can people live with that? I'm actually quite curious about that myself.

• 31:48Lukas Biewald?

  Well, I always wonder, I mean, I feel like, you know, I'm also not a database expert, but it does, does make me think like, I mean, I feel like, you know, there was a time when, you know, the big application of databases was more like, you know, financial services and, you know, people really focused on, you know, you know, making sure that like things are completely consistent and you could, you know, have like, you know, like real invariance. And then I think what I've seen in my life is this sort of explosion of interest in, you know, NoSQL and databases sort of like relax these consistency, you know, constraints because, you know, they, they wanted to operate more efficiently. They wanted to like, you know, save all user data and be able to query it.

• 32:28Speaker 00

  Yeah.

• 32:28Lukas Biewald?

  There are kind of these other, you know, kind of competing things that I think are sort of different than, you know, it seems like the, the, the majority of applications for databases maybe didn't need the level of, you know, formal consistency. I don't know if that, I wonder how that sort of um.

• 32:46Speaker 00

  Yeah.

• 32:46Lukas Biewald?

  Actually, there are always going to be applications where, you know, you you want to be like incredibly careful. But that does seem like there there always are kind of trade offs, you know, that that in certain applications you wouldn't.

• 32:57Speaker 00

  I agree, I agree. I think the the interesting, I think, like response have to that is that like you don't, almost like you don't have to um give up the, you know, uh if there's because of the strong reasoning component in the system. So it will be a very different, I think. So again, the recent improver framework, I think, for example, the older alpha proof system, which by the way, one the. To that, to me, was the IMO moment, to be honest with you, the twenty eight um score of Silver Meadow, um with twenty nine being the goat cutoff. But they have got every single question about the commentary one, which is the same as the twenty twenty five IMO, where, you know, a lot of the companies got um thirty five, like missing the one commentary.

• 33:40Speaker 00

  The difference between the two years is twenty twenty four, there are two commentaries, and twenty twenty five, there's one. Um like in alpha proof system, just a lot of, you know, it's a it's a formal system. Um that might, for example, we see that trade off. If you have only an informal system, it cannot formally prove. I think combining these two is going to be just game changing for even in the sort of like, you know, um customer perspective. Because of the natural language part, you don't actually need to painstakingly, you know, ask a customer spell out exactly what you want.

• 34:17Speaker 00

  Um I think part of the goals of the capability of auto formalization is that when facing ambiguity, what does the system do? Like this, it will be, it will be not very fun if, you know, just like, I really like deep research, I use that a lot. Um it it will, or like, I mean, even like some agents like Menace, they will ask me kind of for my, you know, preference for this or that exactly. That is good. I think that's interactive feedback. But, you know, once that list gets to like five hundred, then I will like obviously lose uh patients. Um, you know, what you do when facing ambiguity, I think is a very important part for auto formalization.

• 34:58Speaker 00

  And again, auto formalization, most people think about it as a data generation, you know, a data generation way. But for us, it's a core technology. We think of auto formalization as harder potentially than proving similar problem to proving it's a core technology and they can't be almost separated. And also for us, auto formalization, the difficulty is always the statement. Because if you can like, you know, if you want to auto formalize a proof because you have the link checker, you know, signal, that that's fine. Auto formalizing the statement correctly is going to be challenging because, you know, by definition, you don't have the solution to prove yet.

• 35:40Speaker 00

  It's very good in the code verification setting to try to auto formalize because you have the test cases of input-output pairs as a proxy to ground your formal spec. And I think this sort of like spec-based programming, I think similar product like Carol from AWS, like we think that's just very valuable and visionary thinking.

• 36:05Lukas Biewald?

  I mean, I'm a little bit out of my depth here, but isn't there like a, like a kind of halting problem here that sort of limits like where this can possibly go? I mean, just because you have this case, it doesn't mean you'll know.

• 36:14Speaker 00

  You cannot, you cannot verify all code in Python. Like that's, or like, you know, that's, that's not possible. But you can do for majority of it. You can do like things that can make people's life easier, just with the, with the, you know, capability you have. I think I have sort of, you know, before, I think it's about like, you know, a couple, like 10 minutes ago. I think I said that was an important qualification. Yeah, you cannot do all code, but you can do quite a lot.

• 36:47Lukas Biewald?

  Cool. Are you already working on, you know, commercialization of your technology? Or are you still in like the research phase?

• 36:56Speaker 00

  So we are, we were actually, I think after the holiday, we're like a six-month-old company now. We thought that the R and D stage will take a long time. And I still today think we are only at day zero. There's so much to do. But that doesn't mean, you know, I think we are in active conversations with some trusted partners about, you know, what this technology could solve for them. And I think through these conversations, first of all, it's just very intellectually expanding and it's really great to feel like, similar with, I think, my seed round fundraising process is that there's like real intellectual alignment with people you're talking to and

• 37:40Speaker 00

  everyone feels a bit like a, it's almost like a secret keeper. It's like, I feel like we see something that the world doesn't see yet. And that that feeling, I think, when you're talking to the right people is just exhilarating. We are doing, you know, obviously some early conversations on that on the upfront.

• 37:59Lukas Biewald?

  What do you think like, what do you really predict for like mathematics going forward? I mean, of course, it's sort of nice to say that, hey, this is like a helpful, you know, friend and collaborator, but of course, this is going to get, you know, better and better. I imagine like, you know, and some amount of time, you know, all new proofs will be, you know, generated in this manner. Do you, I don't know, do you think like academic mathematics continues or?

• 38:27Speaker 00

  I think mathematics will continue. I think mathematicians will learn to work on a different abstraction than they are used to before. I think the change of abstraction is going to be having less resistance than people think it will have. Let's, let's take an, take an example. I think back then, before LaTeX, you'll have a typewriter, right? You're like, like kind of like types at your math paper, like the secretary, I think. I'm not, I'm not sure. I don't know. But after LaTeX kind of came out, mathematicians like welcome the use that this can be a really good tool. I think for Like also, by the way, I think having kind of computer help with some part of the mathematics

• 39:12Speaker 00

  research, it's not new. I mean, computer algebra systems have been, you know, aiding a lot of the more computational work. We find that probably this were free mathematicians who have already developed very good intuitions, the like manual labor needed to painstakingly check every technical lema. And so if you're someone like, you know, Terence Tao, really great mathematician, just let your intuition take you to wherever you want and have the AI mathematician be the diligent grad student or postdoc, you know, trying to prove the

• 39:56Speaker 00

  intuitions you have. Or, and I think one very important part is, a lot of the AI for math, I think, efforts overlook the construction part. So kind of proving and construction, to me, are very important part of mathematical research. Constructing interesting examples as a pre-conjecturing step, you know, as we set right down a few sequences and see, you know, whether it will give you some ideas as to what's the right lema to kind of formulate next. Or, kind of constructing counterexamples to say, hey, like, just don't go that direction. It's, you know, it's insane. Like, it's sanity check doesn't pass. I think that will rely,

• 40:39Speaker 00

  not on the formal proving things we talked about, but on mathematical discovery, like pattern boost, being able to generate interesting patterns. And we have that part of action we kind of haven't quite touched on. And I think that will be a really interesting loop where there's say, like, a conjecture led by intuitions of mathematician. And then you have the action prover prove it. And then you generate more conjectures, one way or another. So formal conjecturing also the sort of even end to end, which is the transitive codebase in mass discovery. And then you discover more conjectures and you prove that. And then you start having

• 41:19Speaker 00

  this sort of loop. Mathematicians can be good sort of guardians of, of, you know, the sort of intuitions guiding, guiding every step of the loop.

• 41:31Lukas Biewald?

  Sure, but I mean, I guess it doesn't take much imagination to also imagine that, you know, the system you're building could, you know, have intuition, better intuitions than mathematicians about, you know, what to try and even, you know, what's interesting to humans, which is kind of a funny, I feel like mathematics-

• 41:48Speaker 00

  Different intuitions, different intuitions. I think the interesting thing is, it would be probably a more of a case where, you know, as a kind of "we are doomed" narrative, if we think that the, what's difficult and easy for machines are the same as what's difficult and easy for humans, that's not the case, right? We think that this, oh, I mean, you do have the reasoner kind of learning a lot from humans as well, but I do think that there is this sort of top zero point zero zero zero one percent of mathematicians, they are like intellectual powerhouse. I think for an AI to catch up to that takes a long time.

• 42:26Lukas Biewald?

  Interesting. So you think there's like a bigger gap between like a Terrence Tao and like an average like academic, you know, mathematician than between, you know, someone with like a math undergrad and the average academic mathematician?

• 42:41Speaker 00

  I would think so. I would think so. But I also think that even when we talk about the Terrence Taos, there are like many styles of mathematicians. There are mathematicians who are theory builders. They like are not the best problem solvers, but they are able to open up completely new fields by connecting the dots of things that are deep in the theory literature. And there are people who are problem solvers type mathematicians. I do think that the problem solver type of mathematicians in domains that do not require a lot of deep theory, which by the way, very much narrows the fields we're talking about, because even in common taurics that, there are a lot of common taurics that are currently connected

• 43:26Speaker 00

  to analysis, very deep analysis. And so making it, you know, not a shallow subject at all. I do think there are certain type of mathematicians that will, you know, see AI serving an equivalent function more than, more than the other types.

• 43:43Lukas Biewald?

  Interesting. Do you have you tried putting in like P versus NP or Raman hypothesis into your system?

• 43:49Speaker 00

  Oh, I don't think we are there yet.

• 43:50Lukas Biewald?

  See what comes out.

• 43:51Speaker 00

  I don't think we are there yet, but I do think that there are interesting results we're gonna put out soon. Um, about sort of surprising capabilities um that we didn't expect certainly. To be very frank with you, we did not expect Putnam to be that well, that like the result to be that good as well. Um, constantly seeing that the capability of the technology um compress the timeline prediction of even the ones building it is a very good sign, I think, for a startup like us in this early stage.

• 44:24Lukas Biewald?

  Totally. I guess one more thing I was curious about, you know, you were on a um, you know, kind of academic path and now, you know, you're kind of running this company. Could you talk a little bit about the transition? Like what, you know, what made you decide to um to shift gears like this?

• 44:40Speaker 00

  I like grew up listening to like hardcore rock and roll music, talking about like, when I was five, I would listen to like underground rock and roll music with a lot of curse words in it. So I don't know why my mom like does not do the parent control.

• 44:55Lukas Biewald?

  What are you talking about?

• 44:57Speaker 00

  Uh, like there are some like really like secret like bands, rock and roll bands in in China. They are obviously very uh politically rebellious and also uh very, you know, writes about all topics, the lyrics are quite interesting for a five year old to listen to. There is this part of I really appreciate a diverse range of things happening in my life going on. And also like the contrarian appeal. So I I don't actually think of myself as the most academic academic when I was in academia. And I'm definitely also not the most founder founder, somewhat in between. Um.

• 45:39Speaker 00

  I do think that this startup is like really fun as in it's such a broad new like brand new adventure. And you're a bit living like the rock and roll day every day and you know, it's very high entropy. And things are wildly exhilarating. You're empowering others to do their like, you know, research of their dream. Um, to build their legacy of scientific, um, or like achieve their scientific ambition. I also think this sort of, you know, making sure things run and serving the work class researchers we have. Uh, it's another part that I really greatly enjoy. Um, I, I think, I, I do think that the sort of.

• 46:22Speaker 00

  You know, transition has not actually, like, I don't feel it. I, I feel like some, somehow like I found my native land. I, I, I think there's this sort of very specific kind of founder personality and like all the saying of like. Chips on your shoulder or like all these saying about like, you know, being very, uh, both very spontaneous and can be very like. You know, nerdy, methodological. I, I find myself to be like everything, uh, in this, in this portfolio. So I just, I really love my job. Uh, yeah, I, I, I think there's like, I thought there will be like some sort of like shock or transition. No, I feel like a fish in the water. Uh, it's, it's really great. Um, I think also this, working with this team of people coming from.

• 47:06Speaker 00

  I don't think there's another sort of team with AI programming languages and mathematics, the three pillars together. Which is very interesting if you think about like programming languages, more system side of. And we have like many, many people in the intersection of programming language and AI, intersection of AI and, and math and intersection of. Actually, all these sort of applied domains like chips or code verification with these. So we have like. By luck or something, the people we hire for the three pillars also have track record in their past in each of these application areas. So it felt like the right team and working alongside with them is, I think, a lifetime honor. Uh, and kind of seeing how they think about things from all sorts of perspectives, like.

• 47:48Speaker 00

  Mathematicians who might not know machine learning give us a great deal of inspirations. Um, the compilers, you know, uh, literature have interesting techniques that can be, that can be applied here. Um, if you group the AI for math OGs like Francois Charton and Alberto um in doing mathematical discovery. If you kind of like have them talk to the formal pruing people, um, their interesting ideas about what self-improvement means. And these sort of discussions happening every second, you know, inside the Axiom office. Um, and and me being part of that, I just think we're humbled by that. And I feel like it's even more academia in a sense, as in it kind of expands and stretches my intellectual boundaries more.

• 48:29Lukas Biewald?

  Love it. That's super exciting. I think it's a good place to end.

• 48:34Speaker 00

  I don't, I don't know. I, I think like if you like force me to trace like why I enjoy being a founder. I would say that like the five year old like hardcore rock and roll, like there's some correlation to that.

• 48:45Lukas Biewald?

  Can you give us one song? I feel like we should fit the song in the podcast.

• 48:49Speaker 00

  Oh, Jesus Christ, there's so many songs and they are, um, I, I can send you something after this. Yeah, it takes me a long time.

• 48:56Lukas Biewald?

  And it's a playlist. Do you have like a Spotify playlist or something?

• 48:58Speaker 00

  I, I have, I have, uh, I can probably have a YouTube playlist. Those songs are so, all the bands are broke now. Like they are all disbanded and um they are like, you know, like, and actually you find that the songs they write when they are poor. Uh, in the, like the ones that make it, for example, the ones, the songs they write when they are like, when they had no money so much significantly better than the later ones. And it's, I don't think it's the pressure of commercialization. I just think that there's something about like burning um desire to, to make it. And, and the hunger um associated with that, uh, which is something that we try really hard to preserve here at Axiom is that. You know, we want to be constantly uncomfortable. Um, we are like acutely aware that there are large incumbents and we are.

• 49:43Speaker 00

  Um, like a little bit late to the game and we want to have that underdog mindset regardless of what milestones that we are also, you know. Kind of seeing um us achieve. I think preserving that sort of. Small and mighty, hopefully. Like, I think, I think that's something that we, at least myself, I hope that is, you know, always preserving the culture. It's like curiosity like a child, not taking ourselves seriously, which I think that's, that's why it's a perfect time for us to build right now. We're at a day there and we're exactly that face. So hopefully, you know, that, that face can, it's, it's a bit like the grad students, for example, sometimes produce mathematicians when they're grad students, sometimes produce like their best work.

• 50:26Lukas Biewald?

  Totally.

• 50:27Speaker 00

  Yeah.

• 50:28Lukas Biewald?

  Well, great to, great to meet you. This is really fun. Thank you.

• 50:30Speaker 00

  To meet you. Awesome. Thank you so much.

• 50:33Lukas Biewald?

  Thanks so much for listening to this episode of Grading Descent. Please stay tuned for future episodes.