AI That Can Prove It’s Right: Verification as the Missing Layer in AI — Carina Hong

24:52Carina Hong:Seven months old. Seven months old. Yeah. Amazing. Before we go further, you mentioned your background a couple of times in passing. And as I was prepping for this, it's just so fascinating. I want to spend a few minutes talking about it. You covered it in some other podcasts, but I think the story is just amazing. So taking it from the top. So you grew up in China and you were a competitive math kid. Yeah. Just tell us that story. Competitive math kid is such a great term. Because you can break in different ways. Competitive math kid. Competitive math kid. So which one was it? Both. Well, I think I like to win.

25:35So walk us through what is that experience and how formative was this?

25:41Carina Hong:It was extremely informative. I think years of math Olympiad training, you have one goal that is to score as high as possible on whatever that is next, math competition. You have people that are in the same sort of community circle that are also doing the same thing. You are friends with them. You are competitors with them. There are a lot of sort of like, you know, background reading, learning exercise you need to do to over prepare for every competition. I remember I did 75 exam papers to prepare for a competition that I didn't know if I will be selected for. And I didn't end up being selected for it.

26:18How old were you? I think it was like 14, 15.

26:21Carina Hong:I think I learned a few things. One is resilience. it's just like I think you get addicted to pain and suffering so that like the word resilient is like almost a paradox because it's like you like it it's I feel it's like a given I think um throughout that time I mean just the exam get keeps getting harder and the number of people competing keeps shrinking like elementary school I have like 1000 friends competing for you know the spots for the middle school then middle school is like 90 okay and then like high school 25 that means vast vast majority of your friends lost the opportunity to compete and that's a very interesting thing i think it does to a child but then i also like learned some like you know other side you know not just the math olympia when i was i think 14 15 i got into the ross math program which is one of i think the best like high school uh math camp in the states uh ohio state university um i think my first trip to the united states um was that summer it was like you know summer of like eternal joy like every day i will be learning cool research math like they taught us undergrad math and they asked us to like deduce everything from the grounds up like we were asked to prove zero times everything's zero um by like a limited number of axioms and that was very defining it felt very different from math competition it's not like how many people will win that award it's like there is a vast amount of math that you just have no idea about and you get to build it yourself, almost like one brick by another, right?

27:56Carina Hong:From the limited number of theorems you are provided, you prove new things. So we're given like about 25, 30 problem sets. And each of the problems that have problems that like are probably just bookwork theorems, and you would just learn it in college. But instead of presenting it as something that is like a given fact, it asks us to prove it. So our world of mathematical knowledge is constrained to how much we can prove. And that's actually what's going on right now with Action Prover. Like Action Prover has access, obviously, to a lot of the world's information. But because the lean data is so scarce, it's like a lot less than, say, the amount of code data out there.

28:35Carina Hong:It's only two-digit million number of tokens out there in the open world. Action Prover learns to prove things. And it kind of self-improved in a way where all the things that it proved got fed back into it. into a kind of a skill library can be like, apply for the next challenge. There's also this sort of like self-challenging conjecturing component that keeps giving it harder problems, just like my camp counselor gave me the problem set. And this is a very beautiful process. I think like without this sort of right order, sequential order of introduction, I wouldn't like kind of go this far in math or love math as much as I do.

29:14Carina Hong:I think the sort of curiosity and discovery is a basic human need and that definitely exists in like back then the tenured child and that being used to motivate and inspire mathematical learning I think that was a very beautiful process. Amazing and then on some other incredible things that you've done so you did MIT in three years I believe Then you went to the UK on a Rhodes scholarship to study neuroscience. Why neuroscience? Was it all part of a grand plan towards AI or was it just your interest to naturally carry you? Yeah, I think the Rhodes program like did a really good job and probably too good a job to encourage us to just like shift direction.

30:02Carina Hong:Like it has this sort of, I mean, broad sort of belief that you need a lot of disciplines and studies to help you become a global leader. That's what the Rhodes Scholarship is trying to sort of nurture. People who have a background in STEM, they will encourage you to go into liberal arts. I wasn't fully encouraged to go into liberal arts. So I picked something that's kind of in the middle, like neuroscience. Obviously, I think at Oxford, I have a lot of math friends. And so kind of still math was part of the equation. I was also trying to apply math in my neuroscience study, specifically maybe because I just am afraid of animal experiments.

30:42Carina Hong:Like I'm not gonna, I'm probably just gonna stay in, you know, data analysis, computational neuroscience. I was quite interested in topological data analysis and persistent homology. But later I realized, I think it was like two, three months after the school year started, I realized there was something called UCL Gatsby. UCL Gatsby is this like premium, like, you know, AI hub in London and Oxford to London is a short train. And there's so many world-class faculties there, like doing really cool research in say like theoretical machine learning, like, you know, analyzing the neurodynamics of stuff.

31:21Carina Hong:They're also doing like various other like applied AI research and some from like a cognitive science motivation, but really the core is AI. Then you topped all of this with a joint PhD in math and JD in law at Stanford. All of this has been fascinating, not just in terms of achievement, but in terms of range. And I'm just curious how you were able to do all of this and whether there's any lesson for anybody else. I mean, clearly there's an element of the chart IQ, but there must be something else. I think there's a lot of things, actually. My junior year, I mean, my last year at MIT, I'm like, I kind of grew up with a very sole focus and goal to do Mass Olympiad and then do mass research.

32:12Carina Hong:And the very next step is to probably go to grad school directly and probably not even do the Rhodes Scholarship. I'm not sure because a lot of the Rhodes Scholars are like, you know, politicians or aspiring lawyers, judges. I'm like, I just want to have some fun intellectually. At the end of the neuroscience, I was like, OK, I want to go to Stanford to start my math PhD. But also there's this incredible opportunity of Stanford Law School, one of the two first ranking law schools in the country. And they have really good IP professors who marry like AI and copyright law. They have really good Professor Mitchell Polinsky in law and economics, where you basically are doing differential equations, but you are like analyzing like deference and like retribution, the ratio of each sort of criminal law measure.

32:58Carina Hong:And there are a lot of like other things, cool methods to apply textualism to constitutional law that's very similar to looking up definitions in math textbooks. And so I was like, OK, that's very cool. So I did my I mean, the J.D. PhD is that you have to spend one full resident year in the law school. So that was my first year. I spent like one year being a diligent law student. I was even trying to apply for clerkships. It was a fascinating year and I learned so much. And then the second year, which is kind of a very interesting year where I was browsing all the AI for math research paper and realized that, wait a second, there's so many ideas.

33:33Carina Hong:I mean, from DraftSketch Proof to, I think, STP, Southlake's Air Improving. There's so many exciting papers. And I wish I just have the resources in industry to execute. And that was when, I think, very, very soon after, I just basically decided to do Axiom, fully focused on the company. Fascinating. Thank you for that. So let's actually go into the product now. So we alluded to some of this. Let's unpack how it actually works. So you mentioned there were three components. What is the architecture? What do those components do? So I think like our kind of very broad vision is that we are going to have a conjecture.

34:11Carina Hong:We're going to have a prover. And then there is knowledge base. In a way, your knowledge base is like, let me take a metaphor. Because this is like quite, I think, like in the niche area of like very like subfield of AI. But suppose you are like selling on an ocean, right? And like, where do you know where to go? and sort of your ship that basically decides where to navigate. That's your conjecture. And then you like, you know, sail and tour one direction and then you land at this island. Okay, well, like, do you know if you have been on this island before? You don't necessarily know. Basically, you need to look up your knowledge base.

34:46Carina Hong:You want to make sure that this is indeed uncharted territory. And then once you realize that it is uncharted territory, like, how do you know if it's like, say, India or West Indy, right? So is it, I don't know, is it going to have some rare metal? That's kind of where your prover starts coming in to basically prove this new conjecture that is not in the knowledge phase, that is mathematically correct and has merit. And so that's kind of the, and then there's all the formalization, which is the ability to reason across informal and formal space, kind of weaving all these. Great. And so the conjecture part, is it LLM-based or are you in a completely non-LLM world?

35:28Carina Hong:So we do post-training on, say, like, you know, open source, like, LLM. Okay, so there is an LLM. So how does that work then? What creates the conjecture? Is that front-based? Like, what goes into it? Yeah, I think I would say here, like, the conjecturing part is still the underdevelopment part. We have been, in the last, I think, seven months, very focused on Prover and also made a lot of progress on the knowledge base. So in the Pundam exam, you don't need to conjecture. You have 12 problems. They're incredibly hard. And they are basically tests for your Prover. So Action Prover tried on Pundam exam, got perfect score.

36:06Carina Hong:The underlying system is a system of ensemble of models. And there's also a set of deterministic tools. And also there's like a proprietary data set that's very large. So kind of a combination of these three things that led to that success specifically. I think that for the deterministic tooling, it's quite interesting because these are actually written for Lean in the language of Lean. So a bit like metaprogramming. And that's very interesting. We are actually going to release them on a public API on all these dozens of tools. very, very soon, beginning of March. Great. It's a big announcement today on the podcast.

36:51Carina Hong:I mean, it's releasing the infrastructure for mathematical reasoning. It's called Axiom Lean Engine Excel. It's interesting because there are a lot of sort of grassroots effort from the open source community to try to provide infrastructure tooling for Lean theorem proving. Because Lean is a really sort of, you know, it's a relatively new language and there are a lot of reasons why it could be a bit slow sometimes. There could also be, you know, things where if you assume like an axiom that's mathematically incorrect, like if you assume n plus n equals n, then you will be able to prove 2 plus 2 equals 2.

37:29Carina Hong:You don't want that, right? 2 plus 2 equals 4. So a lot of the sort of like verify, verify proof is actually, you know, one of our prover tools that's about to be released. And that's actually 100 times faster than the other counterparts that are the open source effort called Comparator. So a lot of them are hopefully going to make everyone prove more theorems than Lean. And in this architecture that you just described, compared again to what seems to be becoming the norm in other parts of AI, fundamentally this pre-training LLM plus post-training system, Is there a trade-off to your system in terms of, is it more or less compute intensive?

38:11Is it more or less fast or slow?

38:15Carina Hong:We had a little bit of a sort of cold start problem, right? I think the data is quite scarce. So while there are more than one trillion tokens of code, it's probably a lot less for Lean. So we had to basically take our bold database to generate a lot of Lean proprietary data. So that's one difficulty. And let's double click on that again. So how did you do that? So you created synthetic lean data? That's right. So it's interesting because, you know, when people talk about synthetic data generation in the unverified domain, you really don't know the quality, right? How do you know the synthetically generated financial advisor data is actually good?

38:56Carina Hong:Then they have human experts to try to label it and grade it. Here you have lean. So you know that your thing is correct, at least. And if you do good quality control on the statements, then you will have things that are off mathematical merit. And when we kind of take data bets, we use things like auto-formalization to convert existing math from informal language to formal language. We also do things kind of that are more formal system-inspired, such as repair, fuzzing, exactly, to make there a lot more synthetic variants of the existing formal data that we currently have. So the other difficulty, I think, is like Lean runs on CPU and then the sort of LM part runs on GPU.

39:38Carina Hong:So you have a little bit of CPU, GPU means engineering. Just like a very interesting effort where ideas are out there. You need a very strong industry strength engineering team to execute the many good ideas. Maybe some academia researchers have produced. Some of our researchers have produced this sector. in terms of kind of how compute it's not like horribly compute intensive like definitely not compared to pre-training I think that like data is a large part of it I think that like good sort of infra engineering is another part of it so as I was researching this there were some numbers on a Putnam question basis where there were millions of tokens give us a sense for like the order of value really really varies I think there are like you know there have been cases where a hard problem and penance takes like 1 million tokens and stuff but there are also like a lot of other things we could do we in-house have something that can shorten proof so for example you can shorten the proof significantly 20 times shorter it's like different levels of how you would like to count like how kind of bulky a proof is and then uh still bearing in mind that you're a very company what is the current state of the product are you mostly focused on mvp kind of product that can solve this amazing problem but that's not industrialized yet what what part is research versus what part is engineering and product so far we focus a lot more on i say so there's this sort of like you know team of really strong machine learning researchers and engineers and they're all like both researcher and engineer in one they're like really amazing um we have a lot of really good people from meta from google brain from anthropic etc and we just um we keep hiring you know more and more uh sort of frontier lab researchers um this part i think is like you know focused on developing the core capability of the system so we want to basically push the the goal post like forward right so from putting them perfect score that was four months in then two months later was the four research conjectures and then you know during this middle we also have tested something that is transfer learning from math to code verification so another evaluation only a community recognized benchmark we want to kind of try where we can get because we have really great mathematicians telling us how we should think about certain research problem targets And we currently have really hard research math problems in-house that we are tackling.

42:16Carina Hong:It's showing some problems. It's also obviously getting stuck. So there's this part. And this part is like, you know, the current focus of the company. Once we know where the frontier is, then we can try to say, okay, let's make it robust. Let's make it sort of production grade. So when 1 ,000, 1 million people hit it, you know, it doesn't break. But this part is kind of sort of an effort that's surrounding that. And sometimes people like jump between different tasks as well. Now we learn something about the applied use cases. We also have a lot of subject matter experts and we are hiring, we are hiring subject matter experts to join us to work on trip verification, to work on code verification.

42:58To just double click on something you just said. So is there a long list of just pure math challenges ahead, you know, for the uninitiated? Is there an Everest in math?

43:10Carina Hong:There is. There is. So what is it? Roughly by, I mean, journal submissions, a lot of other factors, obviously. But, I mean, you can think about currently the batch of papers Axiom Prover has autonomously proven and mathematicians have written. You can probably get into Journal of Number Theory, Journal of Algebra, like that level. Well, that's a very different question from Endless of Mathematics or JMS, invention needs. That's one big jump. I think, you know, to get to that sort of result requires a lot of pushing. And we are not pushing it to just chase the amazing feeling, which is quite amazing, of proving something that is like grand and open for a long time.

43:55Carina Hong:But also at the same time, we are basically teaching the model things that it could not do before, such as a more complex reasoning tree. So on the easy end of the Pundum problem, we have 40 nodes. On the hard end of research questions in-house, we currently have a research problem with thousands of nodes. So it's a much wider and much deeper tree. And we want to see, are we going to hit a limit or not? We currently are not seeing one. So we really want to basically scale the complexity of the reasoning of the problem. We want to make the AI be able to do library learning. That is, we have seen it actually quite promisingly, auto-formalized definitions, which is really, really hard.

44:38Carina Hong:So in math, you have theorems, proofs, lemmas, propositions. Basically, you have definitions and that's very hard to ground. So you want to be able to auto-formalize definitions. You want to be able to have the model system explore definition to still be relevant for the proof. To progress through this series of problems. So if this is not super GPU intensive and this is not super... Fairly. Yeah. And if you've built a way to create synthetic data that works, what is the fundamental bottleneck? Is that doing more of the same thing across more domains or is there an architecture evolution? They're scaled up and they're scaled out.

45:21Carina Hong:So we're currently scaling up in difficulty. We believe that is a defensible move. I believe we are currently doing certain things, interestingly, and are ahead of a curve in terms of how we get rid of running out of context, this kind of problems, how we scale learning from experiences, how we scale inference. I think we are doing that. And we are also scaling out in a way of both there are some math problems. They are not solved, not because they are like or they're not auto formalized. Actually, there are interesting things you can do. You can choose an existing math result and try to auto-formalize it, or you can choose an unsolved math problem and try to prove it.

46:02Carina Hong:Both are incredibly valuable. I think people talk about unsolved problems all the time, and there's a lot of value in actually picking good targets to try to auto-formalize it. A lot of these are unsolved or, you know, not completed because they are very complicated in terms of the sheer volume of that result. So that's kind of scaling out within the domain of mathematics. and then there's also scaling out from math to other domains such as code verification and hardware verification. Do you think that AI can win a Fields Medal? There is this friend who taught me a lot of things about math and he said that you don't celebrate when you win the Fields Medal, you celebrate when you get into the shortlist of Fields Medal.

46:48Carina Hong:So obviously there is only a finite number of awards And I think that we really want Accent Prover to be able to solve one longstanding problem in mathematics that you can objectively say, even though if it's an AI, you know, or double blind, whatever, that will be in the shortlist. And just to unpack that, why shortlist? Why is the... Because then there are reasons, you know, whether... Oh, because then it gets political? Well, not quite political. I mean, sometimes fairness, for example, if a certain domain just got, you know, it's, yeah. Yeah, but to the short list, that is sort of the objective standard.

47:25And to the broader creation that I guess we alluded to a little bit earlier in the conversation of just training brand new sort of groundbreaking science. Like you think AI is well on its way. I mean, obviously it's doing some, but like in terms of humanity altering kind of groundbreaking discovery.

47:47Carina Hong:The first couple, well, not the first couple of months, a couple of months before we actually start executing. It was incredibly exciting for me on an intellectual level. Like every day I have this sort of excitement. Like it's like I drink like six cups of coffee kind of excitement for months. And the main source of that excitement, which I would tell you actually about, you know, my colleague Shubo, a good friend, he's excitement of this in a bit. But my excitement is like, just like we're now realizing that we are at the threshold of mathematical renaissance, we could also be at the threshold of theoretical discoveries in science.

48:27Carina Hong:Massive, massive scientific discovery at the theory level. And I think what I mean by that is we have been in a very math poor world. The supply of outlier mathematical reasoning skill is so lacking that people are like in the scarcity mindset. Like you will like hear discussions of, oh, like this problem is so interesting. Unfortunately, I'm solving that problem. They should all be solved. everything that human mind can conjecture find interesting find tasteful to be solved by hopefully majority of them by action prover and then you have the question of high physicists when they talk to mathematicians generally they will have interesting opportunities for collaboration like i actually have this paper with professor kenono and and others xin tong jiang and Michael Mertens, which addresses like the elliptic expansion moonshine conjecture.

49:29Carina Hong:And that kind of stands from like, you know, three, I think three theoretical physicists. They conjecture this based on their observed or like physics like phenomenon that I know, frankly, not very much about. But I can solve the math part. They come to the conclusion that what they believe are a beautiful phenomenon that they find it worthy to formulate as a conjecture and publishes a paper have a proof because they know some mathematics. That doesn't seem right. Like, I think that the really, the beautiful vision is for all the theoretical problems, all the curiosity, all the lack of understanding to be resolved in a satisfactory way across all scientific subjects.

50:12Carina Hong:And beyond this, right, there are things that we still cannot solve that we will get a close form sort of, not a close form solution, We'll get a very like, you know, approximation as precise as possible. I mean, there's a lot of value, for example, to know, say, what is after the 1000 or 10 ,000 digit compared to what is after the third digit. The word is actually a lot of the times not diminishing return. The last mile carry a huge amount of value. Like in search, for example, if you cover some edge case, you likely win. You will be a market winner in, for example, writing, right? If you write just that extra bit or any sort of creative art, getting that extra mile correct or done has a lot of value, like optimization, you know, precision.

50:54Carina Hong:We can try a lot of these things as well. And then as math kind of helps with both first principle understanding and try and error, it just kind of this cycle. Like you have some first principle understanding, you try testing it, you try some try and error, and you maybe give some sort of, you know, risk bond, uncertainty, principle, robustness estimation. And then you go back to your first principles and then you go to your trial and error again. You have this sort of circle of discovery. And this is really not the end of it. So that's why I'm already very excited. I think this is going to be amazing.

51:28Carina Hong:Ideas can diffuse between different fields. A bit like you have like Abacus and now you have like trade and commerce. You have calculus integration. You have like thermodynamics, mechanics, industrial revolution. You have the Babbage engine, which is to calculate log tables faster. And, okay, well, you have the prototype of computer science. The rest is history. You have number theory. You have RSA. Like, you have all these kind of mathematical tools, you know, kind of open up new discoveries and new use cases and in turn demanding more mathematical tools. Beyond this cycle and this cycle marrying science, here comes code.

52:03Carina Hong:We haven't even talked about that. And that's why actually Shubo is very excited. so Shubhou, CTO of Axiom before that was like you know long term like meta veteran he was an IC director he believes in code is math okay so through all my good friends telling me about Lean telling me about Howard Correspondence I believe math is code he believes code is math what does that mean? okay so it means that you can try to fulfill the dream of Donald News literary programming have computer scientist programmers enjoy the luxury of mathematicians where they can reason in natural language and this is kind of starting to happen right web coding like front end right like you know we can have very cool like lovable websites but like how do i have web code nuclear reactor how do i web code control flow how do i web code complex systems that require like quite honestly superhuman hierarchical reasoning skill it's interesting because you're not in code alone You have code and you have math.

53:05Carina Hong:So you have, in addition to the flywheel we already seeing in the coding companies, an additional layer of flywheel of verified code. And sort of math starts to come in. And this kind of flywheel of data keeps compounding. You have actually two, even counting the science parts, three orders of flywheel. How far do you think we are from that world where we have armies of it? We have to execute like, you know, something every couple of months. Like we have to move extremely fast. Like there's so much to do. I think Axiom is a very, very young company and we are at like, you know, the very, very beginning tip.

53:42Carina Hong:And we are already, I personally feel some sort of shock and emotional response. And I know some of my mathematician friends, Scott Commoners is a Harvard microeconomics professor, also Morgan Price winner. We're good friends. We all have this sort of emotional response when Axiom Prover proved Vals conjecture, proves that almost all primes are partially regular, partial Vandiver conjecture, which is one part of the original Vandiver conjecture that has been open for 90 years. The parity of differentials for services of genius zero and one by algebraic geometry paper. We are really just leaping across a point.

54:20Carina Hong:I mean, Pundit marked, I think, the end of AI trying on Math Olympia. We are very glad that we got a perfect score. It's a really good period point. Pundum 2025 is by a lot of sort of experts grading harder than IMO 2025. So it's the hardest reward math Olympia test. And now we are leaping. We are leaping to research. And I think I'm going to have another similar emotional response if it really does solve one of those breakthrough mathematics problems. Interestingly, I think there are a lot of experts in domains that are currently overlooked. by AI development. So if you're a software engineer, you feel like, oh, web coding really changed and improved your quality of life in a meaningful way.

55:02Carina Hong:There are people who are in industries where because of lack of provable guarantees, they couldn't use AI. And there are, for example, AeroAstro, for example, like I think Defense. For example, there is no partial credit for a mostly verified GPU. It's all or nothing. Or mostly flying plane. Yeah, yeah, yeah. a mostly verified, formalized hypervisor. I think for these experts, they are currently kind of hand-holding a lot of the traditional goals. Their life has not been changed. And I want to see the AI for math movement that Axiom is hopefully leading and to transfer to these domains and to try to solve some of those problems as well.

55:47Speaking of emotional response, Is the entire math field super excited about math AI or do they feel like the rest of us possibly disinhibited and replaced by AI?

56:01Carina Hong:So I think a lot of the like adverse reaction about from the math community about AI is actually coming from the fact that they cannot verify an informal solution. So suppose like GPT generate a math proof a million lines. No one's going to check that. Like I'm not going to check that. Like, you know, like I know there are a lot of really great sort of data labeling, you know, services. They couldn't have that sort of level of expert to verify a proof of that link. It's just hard to do. On the other hand, if you have a formal certificate, like a stamp certifying that this is a correct link proof, I think people are a lot more receptive to it.

56:39Carina Hong:That's why actually a lot of mathematicians, especially almost all of the new school of mathematicians are accepting lean. what they want to do is to have human to formalize lean. Now, it's really fun for humans to do lean. We have a lot of the initial Maslip people here at Axiom, and it's a very fun team to see them formalize some statements. But when it comes to, say, like hundreds of thousands of lines of lean code, which is already not a hypothesis, like automated reasoning team at some big tech currently have 260 ,000 lines of theorem proving code, not lean to verify one component of a hypervisor for CPU utilization.

57:19Carina Hong:So that cannot, I mean, they actually did write it by human, but it's just not quite sustainable. So maybe just to close, just one sort of final chapter in this conversation. So while I was listening, I was thinking about how someone with such a deep background in math becomes a CEO and what that transition was like and whether there's any lesson for anyone considering making that jump or any founder out there. I remember that reading the anecdote of Hamilton that he writes down all his flaws and shortcomings every night and forcing himself to correct them. I know what my habits and flaws and shortcomings are.

58:05Carina Hong:I'm a very spontaneous person. I don't have the best ideas when it's planned, which I think sometimes that's like you know in the course of research you have like math research you have these kind of very interesting eureka moments I think so I try to overcome that in my day-to-day I try to do scheduling very intensely I try to surround myself with people who inspire me to execute faster and that's basically the entire team and I think it's a great honor to be working with them every single day I think like I go into the office and I look around and I hear the discussions and I'm like wow I'm like so I'm so lucky to be here uh and I think that's something that in this kind of talent market I think people like to work with people who value their intellectual judgment respect their voice and opinion and I think Axiom has this sort of very flat like non-hierarchical everyone's a member of technical staff or a mathematician, right?

59:06Carina Hong:If you're earlier founding plus that. This culture is really great for sort of, I think, the sort of open communication of ideas and debate of ideas. And that helps with the pace. It helps with the pace of iteration, helps with being more correct. A lot of things I'm learning very rapidly. I mean, it's been very interesting roller coaster, like seven months. When I was in math, I mean, there is this sort of idea where you have like taste and And sometimes these tastes can be interpreted as arrogance. And I learned that ego is a really, really bad thing. And we should just basically get rid of it.

59:42Do you hire people for taste? And if so, how do you evaluate it?

59:46Carina Hong:Yeah, we hire people for taste, but not for ego. And I think that's a very interesting kind of... How do you select people? How do you evaluate someone's taste? Is that their prior work? Right. So one is, basically, that means I have to learn every day because I need to have a certain ground, you know, a basic amount of taste and also the other people who are senior at the company need to have, research scientists need to have that sort of amount of taste and what makes us excited. And when we are excited, we just go after that person. We have had a lot of, I think, extraordinary hires from amazing and interesting backgrounds.

1:00:26Carina Hong:And we like, we really like this team. And I think that we raise the bar for hiring actually continuously. So we recently have an uptick in the number of people who would like to join us and our candidates that we're excited about. We take recruiting very, very seriously. And how did you secure that founding team initially? Because that's kind of ridiculous in terms of like caliber of just world-class mathematicians, world-class. How did that all come about? One of them was your mentor. So now technically you mentioned that you're very flat, but like technically working for you as CEO. How did that come about?

1:01:07Carina Hong:So quite interestingly, I think at the start of this, I realized that there is a movement. And this movement of AI for math is very much by and large in academia. Or actually people are hiding in labs, like secretly doing AI for math, where their day job is something else. So when I talked to each of these people, like it was a very, I think, mutually exciting feeling from both parties. And basically it's like two whales and just kind of realized that only they can communicate in that like frequency range. And that happened like multiple times. I got very inspired by this. Like, I think there were a lot of times at the beginning where fundraising was quite hard.

1:01:45Carina Hong:I think, I mean, I'm a nobody. No one should trust me with their large amount of money. And I think that was very difficult and challenging, but it was those conversations that basically made me realize I have to do this. I just have to. And like, you know, and I have to be the best deal for this team because my team deserves the best of the world. And those kind of like, you know, intellectual alignment were like a main theme. And the other thing I realized was that they found, say, maybe the other AI for math opportunities is not particularly attractive for one reason or another. Maybe they don't want to move geographically to London or to China or maybe, you know, it's just a different kind of vision.

1:02:20Carina Hong:So kind of gathering them was a relatively natural process. And then after that, I think when you have a bunch of really smart and nice people, you just attract other smart and nice people. And especially people who are adventurous, like rebellious. People who come from co-gen want to disrupt co-gen. People who come from math want to disrupt math. Disrupt and I guess like elevate as well. Because they do have a lot of affection still with that feud. So I think it's a very interesting, it's almost like a tribe. Axiom is like a tribe. And we have more and more people joining us. And sometimes I feel like both in those initial conversations and still now, and even after all these sort of like, you know, talking to the world about what we are doing, we still feel like secret keeper.

1:03:09We still feel like we cannot fully elaborate and emphasize

1:03:13Carina Hong:the thing that we are seeing that is the next frontier of AI. That is a generation and verification loop. that is the discovery of verified knowledge. Feels like a wonderful place to live in. This is all incredibly fun, compelling and inspiring. Thank you so much for spending time with us. Yeah, thanks so much. Yeah. Hi, it's Matt Turk again. Thanks for listening to this episode of the Matt Podcast. If you enjoyed it, we'd be very grateful if you would consider subscribing if you haven't already or leaving a positive review or comment on whichever platform you're watching this or listening to this episode from.

1:03:46This really helps us build a podcast and get great guests. Thanks and see you on the next episode.