Entrepreneurial Thought Leaders (ETL)
00:04:32 · Carina Hong
[00:04:32] S2: Yeah. I think, like, Axiom is doing something called formal math reasoning, which is the ability to convert mathematics into machine checkable code. And this is quite valuable because if you think about the amount of materials being produced by AI, it lacks like this sort of verification layer. So something that we announced yesterday, which is I think the reason I'm sick, is because we announced the formalization of the classification of finite simple groups. For those of those of you who don't know the theorem, it is the largest human written mass proof. So there literally isn't another proof that's longer than that. And the problem with it being really long is not a single human have read the whole thing. So it's the collection of twentieth century mathematics over generations since, I think, first time the concept of a simple group started from. And then in the sort of nineteenth century, someone decided that, oh, it's like... These, like, five, I think, sporadic groups might be in the family. And then I think nineteen fifties, in the famous ICM, Brauer decided decided to start the hunt for classifying all the finite simple groups. And that is more than 15,000 pages of mathematics, kind of like scattered across many papers and books. And I think the sort of our mission is to basically turn a lot of these mathematics, but also other stuff into machine checkable code, where when you run the computer program, you can be sure about its correctness. That is a 100% verified. I mean, Gödel kind of tells you that you cannot be truly sure of anything. So what it does is it boils down this really large thing into a small trusted kernel. So it's beyond a reasonable doubt, correct. And I mean, it's basically very, very it's only a theoretical question that it will have like a major problem. And then that resulted in more than 50,000,000 lines of code in this programming language, Lean. And the reason it's very interesting, I think, from a commercial perspective is it's also the largest open source software project. So it's larger than Linux. It's larger than like the other like software open source project you have had. And this is also a programming language, just lean. And it reflects this one theorem, one really big proof.
00:06:43 · Carina Hong, Ravi Belani
A lot of mathematicians described their like reaction yesterday, like there's always this cloud sort of on top of all these mathematicians' lifelong work, their legacy, and now that the kind of cloud has fully dissipated. [00:06:56] S1: And so that's profound from an academic perspective on that proof, on the research. Can you share what the vision is of why the venture capitalists are so excited? [00:07:05] S2: I think it's something that hasn't been done before. I think that's... I think one one is emerging cap... Emerging technology. It's always very interesting because the moment you can kind of have the verification layer, it's not really for, oh, I have this code and then like, please tell me if it's correct or not. If I can generate new code and instant time get that verification feedback. So then that is really like the future of AI assisted coding. [00:07:32] S1: So the shift is even though right now people are using ChatGPT co... Codex or Claude Code, that is for creating code that's human created. The vision with what you're building is to actually have agents creating code. Is that is that what you're saying?
00:07:47 · Carina Hong
[00:07:47] S2: Yeah. Think so. So, like, no one really trusts, like, tasks that much nowadays. I mean, you see on, like, the news about our nation's, like, critical infrastructure. Oh, the railway is down or, you know, the... I think there is this Boeing seven thirty seven that kind of had to, like, re land because of a critical software bug. I mean, all of them have gone through testing. Now code review is actually at, like, all time, like, lowest for, like, you actually do the code review or not. There are a lot of companies, AI native organizations just skip a code review. I know for some part of my company, we don't have code review. We just ship. Now that's going to, I think, create some problem. And then when that problem is big enough, it stops the AI deployment altogether. So I think value there are roughly three layers of value. One is the direct value that this technology create. A large part is verified cogeneration, small part in actual verifying existing code, even though that small part is not small. And then the second layer is the amount of the number of organizations that is willing to deploy AI in really, really large TAM critical sectors. And that AI the enablement of AI deployment is value. And then there is this third part of, I mean, you're into the auto research, I mean, AI for science, it's like long horizon discovery, whereas agents are sort of functioning autonomously. And I mean, it's different it's similar to the verified cogeneration because but with that, it's more interesting because you can then play with data. And then that is going to, I think, drag AI out of the existing like information, knowledge extraction or exchange layer into more physical world, into also like some other parts where it's like material science, new molecules, etcetera are created. I think that's kind of the third layer is that coming out of the software layer into physical world, not just hardware, but like broader science.
00:09:33 · Ravi Belani
[00:09:33] S1: So this is so this is such foundational and impactful across multiple different areas, and so I understand the the gravity of it. I'm still curious if you can unlock the mysteries of how you closed the... There were two financing rounds within six months where you closed $260,000,000 as... And at the time you were 24, a solo founder. Is that right? Yeah. No co founders. And it's also, you know, people... It's also particularly difficult as a female solo founder to close capital, let alone without without... With just academic background. At at that point, you had... You didn't have any professional work experience. You were coming out of academia. Is
00:10:10 · Carina Hong, Ravi Belani
[00:10:10] S2: that During my first round of fundraise, my CTO came in, so definitely, I think, ease a lot of ease a lot of burden. I think the first seed round was really the idea of AI is going to change mathematics. There are other companies doing formal reasoning at the time, but I mean, I think a lot is spent on the right technical approach division. We were pretty sure that we would not use a Monte Carlo Tree Search type of search at training. I mean, search at inference, turns out to be the right bet. It's then adopted by like Cdance and other amazing player, a seed prover, ByteDance. And then I think the second round was more of the ability of transfer learning. We observed that the formal math prover that we have built got a lot of very high impressive scores on other software verification benchmarks, sort of to our surprise. And also with Putnam being perfect score, I think the sort of feeling that it will be destroyed by the bitter lesson, the dawp on that front has, I think, been a lesson. [00:11:14] S1: Mhmm. [00:11:14] S2: Even though I think it's a constant battle to try to stay ahead at the frontier. [00:11:19] S1: So you had these substantive milestone proof points that that were really significant. Right. Others get those substantive milestone proof points and still don't close rounds. Was there a a shift change in your approach on fund... Was fundraising easy or was there an inflection point where you changed your approach and that shifted how you closed the round?
00:11:19 · Ravi Belani, Carina Hong
[00:11:19] S1: So you had these substantive milestone proof points that that were really significant. Right. Others get those substantive milestone proof points and still don't close rounds. Was there a a shift change in your approach on fund... Was fundraising easy or was there an inflection point where you changed your approach and that shifted how you closed the round? [00:11:37] S2: Yeah. So the first round was very difficult. I think that was just very, very difficult. It was an idea. My slide probably looked horrible. And then I think something changed at the second fundraise where I was very focused on building the company. When you focus on building the company, you don't give a lot of attention to the process. That actually ended up turning quite well. So sort of when you are very focused on just fundraising, you might tend to overthink things, will drag on process. Later on when you are just building the company, I think it became a lot easier. [00:12:14] S1: Can you demystify that just so we understand? So the irony here is that when you gave it less attention, it was it was more effective. Can you on... Can you can you can you give us... Can you share the details of the specifics of how that looked in in the process?