Axiom’s Carina Hong: Solving Math’s Hardest Problems With AI, And AI's Problems With Math

0:00Carina Hong:Curiosity is like, I want truth. I mean, I don't want a spike of truth. I don't want the perception or the Schrodinger superintelligence. Like, I would actually argue, for example, in a lot of the handling of large language models solving mass open problems, it's Schrodinger's superintelligence. Welcome to the Upstarts podcast, our weekly show where we talk to emerging startup founders about their upstart moment. Upstarts are challengers who punch above their weight to take on the status quo and improve the world, all while building a big business, too. I'm your host, Alex Conrad, founder and editor of Upstarts Media.

0:35I'm delighted to be joined today by the founder and CEO of Axiom Math, Karina Hong. Karina, thanks so much for joining us.

0:42Carina Hong:Thank you for having me. Great to see you. This podcast is brought to you by Mercury, banking redesigned from the ground up. You just raised$200 million at a$1.6 billion valuation for a startup in the math world. And you're less than a year old, I think even younger than Upstarts. Is that right? Yeah, yeah. We are. We started July last year. Wow, that's crazy. So a trajectory from Inception all the way to Unicorn in just eight months. Yeah, seven, eight months. Yeah, we're a young company. What exactly does Axiom do? I mean, you've had this crazy academic career. You know, reading the highlights made me feel really stupid.

1:17because you went to MIT where you won math prizes for the top undergraduate in math in the country. Then you did a Rhodes Scholarship at Oxford. Then you did a law degree and PhD and dropped out at Stanford. Ridiculous. Were you intending to be a mathematician or what was the goal with all of this?

1:36Carina Hong:I was definitely intending to be a mathematician. I think this startup thing is kind of a complete accident. I did a little bit of a calculation of how much I compute I would need if I want to do an AI mathematician. And it very quickly became clear that I have to do it in a for-profit setting. That's so interesting. And Axiom Math is an AI company in a way. It's a math company as well. What's the way you explain it to normal people like me? Yeah. So we built an AI that can do math at a super intelligent level. That means, you know, it should be able to crash all math Olympiades. It should be able to crack a few unsolved research problems.

2:15Carina Hong:We should be able to know kind of exactly what are the blockers to cracking a really, really hard millennium prize problem. And then from there, we want the outputs to be verified. So everything that we produce is actually the output you can trust it to be correct. So that's really the promise of the sort of verified AI or, you know, perfect prover. What does the math verification unlock in a business context? If you think about like machine critical areas in various parts of the industrial society, then there are certain cases where you cannot deploy the code unless you know that it is always, always, you know, satisfying certain property you want.

2:53Carina Hong:Now, you know, people do testing, but testing covers like finally a number of cases. And there are potentially, you know, edge cases that are missed by testing will be extremely expensive, sometimes a loss of human lives. Now, I think even more than the mission-critical areas where there are large enterprises, they have certain regulatory and compliance requirements. They will want their code to satisfy certain properties as well. And then I think you can extend from there, which is that if you do knowledge generation in a verified way, you can do knowledge generation better. So that part is actually, I think, quite beautiful in that it's not about erasing hallucination or catching mistakes about how to scale and compound superintelligence.

3:34Carina Hong:So this is like the part that I think a lot of people often miss. Like they think of verification or verified AI as like, oh, well, something's lousy, you go fix it. Well, actually, it's not, right? If you think about, take a math example, Ramanujan became a really powerful mathematician after he went to Cambridge, studied with Hardy and Littlewood to know how to do proofreading. So that kind of, you know, moved from his brilliant intuitions to something that he can land as rigorous results, that he becomes much powerful mathematician after that. So verification actually to me is about the super intelligence part.

4:06And so in the short term, you can use the math to keep AI from screwing up as much basically, right? Yeah. But then that can unlock a lot of other cooler things.

4:16Carina Hong:We believe that if you do the sort of informal-formal hybrid approach, you can, for example, get a perfect score on PUNNAM, which by Math Arena. Explain to our normies what PUNNAM is. So PUNNAM exam is the hardest undergraduate math test. So it's actually, this year is 2025. It's harder than the International Math Olympiad. So no AI was able to get PNAM exam like ever. We know that last year, so 2024, I heard rumors like other industry players like Google DeepMind tried and they didn't go anywhere. PNAM is known to be much harder in terms of getting a perfect score than say the IMO gold medal.

4:51Carina Hong:And we got a perfect score. We were the only AI that we competed in real time. And we were the first and probably the only AI that competed in real time and got that result. Math Arena, which is this nonprofit academia lab, they evaluated various large language models on this year's Putnam many months after. And they found DeepSeek to get the top score. And that's 103 over 120 versus we got a 120 out of 120. But why is it important that these companies, whether they're a big one like Google or a Chinese company like DeepSea, their creators, or a new startup like you guys, I can understand why from an ego standpoint, from an excitement standpoint, it's cool to get really good at this math.

5:34But why is it so important that your software be able to ace these tests? What does that do for you?

5:40Carina Hong:Yeah, so slowly getting to the point that I don't think we will be able to get a perfect score if it's not with the power of a formal system. which is quite different from all the large language models approach. To answer the question, we kind of share the sort of cultural mission statement that I think DeepSeek also has, which is that math is AGI. So saying math is AGI feels like a provocative statement. I feel like maybe some of your peers in the AI world might find that a hot take or maybe not everyone would agree. What exactly do you mean by that? And where would maybe someone say, Karina, you're crazy?

6:14Carina Hong:Yeah, I mean, a few things. My work wheel is we start with math. You go to code, software. Math and code is twins. Math is code and code is math. We're going to get to that in a bit. And then you kind of run the reward experiments starting from your software stack, right? So you go to physical work. You go to physical AI. And then you go to everything else. So this is like the order. And then the two domains that you can get verifiable signals are math and code as a twin. Okay. And physical AI. Like I drop an egg like gravity. Like it gives me a reward. Yeah. But there's no other thing to have that property.

6:50Carina Hong:And software controls the physical one. So then, okay, I'm going to get to math and code, and code is math. So this is a line that is, I think, in Shubo's, one of his keynotes, the last slide. Mathematicians have been writing proofs, almost like coding for thousands of years. They're coding in English. What I mean is all the lines of the proof have meanings, and they are hooked together in a perfect way. There is a rigorous deduction process that's actually going on and there's objective truth and not truth. And in a way, proof is not computation, but it's close. So computation gives you output and proof gives you property.

7:33Carina Hong:And the output is meaningless if it's not associated with the property. So a lot of the, I think, people working in the formal verification, program verification space actually share the belief that, you know, instead of vibe coding, we need very coding, very coding, V-E-R-I and coding. The dream is that you can generate code and verify the formal verifier, like checker running the back the same time. And what that does is that creates a much more advanced, trustworthy system. When you say math is AGI is because that... No code review, okay? No extensive testing, right? There's a theoretical limit to that.

8:20Carina Hong:You cannot verify all code. There's a theoretical bound, but you can do a lot. You can do a majority of the code that matters. I have seen actually a demo of that. After I saw it, I cannot see it. This is what I mean by it's a code. There's also, I think, a question of whether we will still need mathematicians after, say, you know. What's your take? Do your math careers root for you? I'm using that to show a point, which is that curiosity is a fundamental human need. Even if you have action proof, we're basically generating all the math proof. We're not there yet, but if that day comes, mathematicians will still like to understand it, to auto-informalize from lean to natural language or do informal summarizer to understand it.

9:07Carina Hong:And then from that, they will be able to conjecture more. It's a never-ending cycle in flywheel. And because curiosity is a basic human need, I could also actually argue that reliability or the sort of requirement for consistently correct or trustworthy is actually the flip side of curiosity. Because curiosity is like, I want truth. I mean, I don't want a spike of truth. I don't want the perception or the Schrodinger superintelligence. Like, I would actually argue, for example, in a lot of the handling of large language models solving mass open problems, it's Schrodinger's superintelligence. 2024, I think this guy Dan, who's the head of the Center of AI Safety, Dan Hendricks, I think his name, put on Twitter the pandemic sample of 2024 and, like, put, I think, open AIs, either 03 or 01 Pro was the hot model that was being evaluated.

10:04Carina Hong:And, like, the rollouts are on Twitter. People disagree whether it got it right or not. Like just really like superior mathematicians who were put them takers themselves could not agree on how to grade that. And I think the final consensus got zero out of 12. The open-air people claim it's 10 out of 12 or 11 out of 12. I think no one pretty much believed that. Okay, now like this is Schrodinger's, like something cannot be both zero and 10. And curiosity being the fundamental human need and the pursuit of truth in the verified form being something that also speaks to that. I think that's quite beautiful.

10:40Carina Hong:And another final kind of touch on why math is AGI. Math is a sandbox, and especially lean, where you can try all your frontier techniques. We, I think, are ahead of the curve for a few of the things that people are doing in frontier labs because we have this perfect environment to try. So it's a better sandbox. It's a better sandbox. You can have faster iteration cycles. If you want to push for scientific discovery and scaling learning from experiences, your data trails, how to approach a really complicated mass problem can be that perfect environment. And I talk to a lot of people who are in AI for science, actually.

11:17Carina Hong:They have, like, physical lab. They have, like, they're working on, like, material science, biology sector. Lots to talk about because they are also seeing, because they have that real world of real words. They are seeing a little bit of that, but obviously with much larger spending because, I mean, we don't need robots doing experiments. When you were, you know, a student doing the Olympiad, thinking about going to MIT someday. Why was math exciting to you and what was the potential that you saw in math, you know, at a younger age? Math is like very interesting because in a way I think when you're a mathematician doing deductive proof, like, you know, step by step, like this follows from the last step and then kind of finally arriving at the goal you want to prove.

11:57Carina Hong:What you're doing are two things. One is you're doing knowledge generation. So even if that theorem has been proven before, when you are working out a proof, you're actually exploring uncharted territory in your intellectual boundary. And so there's this exercise of if you take a real analysis textbook, like Rudin, a lot of students will just cover the proof, use another piece of paper to cover the proof and re-derive all these very classical, beautiful results. So that's one thing you're doing. And do you think they're beautiful? I think they're beautiful, yeah. What made you... I'm one of the very few mathematicians who think analysis is beautiful.

12:32Was that always the case? I mean, you're obviously a brilliant mathematician, but were you always just really good at it and like, this looks cool, I love this, or what triggered that?

12:41Carina Hong:I always thought I was okay at it, but I'm always then like, the moment I thought I'm like kind of getting it, I got thrown into another more competitive environment. It's actually pretty bad in terms of like, you know, it's very depressing. You look around and everyone is like an international math olympiad medalist, and a lot of them have like three medals, and like I've never been. So that was like a very humbling moment at MIT. Like the first week I remember it was before the actual orientation was an international student orientation. And then the international student orientation are like every single country's like gold medalist.

13:17You ended up winning multiple big prizes at MIT and being awarded a Rhodes Scholarship. How did you reorient your focus and find the new challenges that you kind of kept moving once you achieved that goal?

13:28Carina Hong:Yeah, that's a great question. So when I got to MIT, I think when some other people probably feel like they're not the smartest kid for the first time, I have felt that like three times, like, you know, in the previous Olympia experience. I was actually coping OK. I was kind of like, well, OK, this is what I expected. I mean, I had the choice of whether I wanted to go to Stanford back then and then that would be less mass Olympia people. But I didn't want to do it. I still want to kind of learn from the most brilliant people and collaborate with them. And after I got the Morgan Prize, I do think actually that thing kicks in, which is like, well, if someone is like a nobody for the entire duration of their limited number of years of life, okay, suddenly you got a recognition.

14:12Explain how hard it is to win this prize. Yeah. For people who are not in math, it's a huge deal.

14:16Carina Hong:Yeah. So the Morgan Prize is awarded to one undergraduate student each year, I think around the world or North America, I think it's US, Canada, Mexico. It's just one person. Just one. Yeah. And it was you. Yeah. So after I got Morgan, I'm like, okay, well, I want to try something else. Like immediately that sort of the loss of focus started kicking in. Right. So I'm like, I was in a neuroscience program at Oxford. I was like really random. I was doing computational neuroscience. Really fun. Casual, you know, piece of cake compared to math, I'm sure. Well, no, I know nothing about biology. But you threw yourself into the deep end with this at Oxford anyway.

14:53Carina Hong:Right. And then there's obviously the UCL Gatsby Institute, which is a very vibrant sort of AI hub. I would take the train from Oxford to London, and I took many, many of those trips. So thanks to Professor Andrew Sachs, whose lab reimbursed those train trips. I was really poor as a grad student at Oxford. Like, a calculator is like, we cannot spend more than 23 pounds each day. Like, that's it. Like, that's your entire road step. And it's hard. It's hard to pay for three meals under 23 pounds, if you think about it. As a year-old startup, we experienced a lot of firsts at Upstarts Media. So when it was time to process our first international wire following a London event, I braced myself.

15:30This is going to be a painful lesson. Instead, Mercury made the process easy. Issuing an invoice, sharing routing numbers, and processing the wire with just a couple clicks. No phone calls, no paperwork, no learning curve. We're still figuring plenty of stuff out. When it comes to our banking, Mercury's already got it all figured out for us. Visit mercury.com to learn more and apply online in minutes. Mercury is a fintech company, not an FDIC-insured bank. Banking services provided through Choice Financial Group and Column NA, members FDIC. You're kicking, you know, whatever word we want to use in the academic world.

16:07And you say, OK, I'm going to go to Stanford now. I'm going to do a PhD and a law degree at the same time. Was that just a proof that you could?

16:15Carina Hong:I never had a liberal arts education. Like I was, MIT is a very big engineering school. and I was taking mostly only math classes, frankly. And it felt a little bit like, I mean, I went to Rhodes and then I saw some of my friends who went to Columbia and they start off their freshman year reading the big books. So from like Pluto to like Socrates. And like, I kind of wanted that. I wanted to read and write a little. I kind of felt like illiterate, you know what I mean? Like English is not my first language. My first semester at MIT, I was learning how to write an English email. like by the winter quarter or like the IAP, which is a winter recess period.

16:56Carina Hong:I called my mom. I'm like, mom, I know how to write an email in English. What was the end goal still? Was it, okay, I'm going to then go back and finish the PhD and then I'm going to become a great mathematician? Or what was the vision? The law school year, the end goal has nothing to do with math. Like I think it is in a way I did only one year of road. I didn't do the full two years. Okay. So I go to this coffee shop every weekend. and this is called Verve Coffee Roaster they have the best mantra advertisement for Verve I am a regular there and every weekend I will go and I will carry my big like books that's my like law school textbook because I have readings to do and it's like I cannot keep up with the reading speed that the law school demands because I read slower than my peers and so then I go and I read my intention is to read the books but then once I get there usually I will just open my laptop and check out the like papers there are a lot of like AI papers around the time.

17:51When would this have been?

17:53Carina Hong:This is throughout the law school year. Okay. This is a couple of years ago at this point? So it's 2023, 2024. 2024, okay. Yeah, because I think of the Gatsby kind of training, I was quite interested. There are naturally people I follow, their work, deep learning, theoretical deep learning. And then I think one day I met Shubo, and then he's like, theory of deep learning is useless. like you know get into practice which is what some of other my friends told me that around the same time a conversation i had i think that was quite influential was with greg young who was a um ex-co founder uh morgan price honorable mention 2018 is that how by the way people who win math prizes talk about each other they're like prize winner 2017 third place 2019 i completely co-emailed i mean that that's like i don't have other connection to him to him it might be just one conversation with this like you know random person for me it was very influential he said try to grab as much gpu as you can try to do like actual ai research and that was very interesting because he kind of had his like period of focused locked in on math he had this period of exploration where he went off being a dj and then he kind of came back to math briefly and then jumped into ai I mean like mu-p, like you know hyperparameter.

19:16Yeah, yeah.

19:17Carina Hong:And then obviously XAI. For me I was at a time where I'm like, okay, well I'm doing neuroscience, I'm doing law, you can definitely call that my exploration period. I'm not following the expectation of what someone might reasonably expect a math person to continue the path. And then I think that's why they say AGI, ASI is a cult. It's like once you see it, you cannot unsee it. the feeling that maybe AI can do math kind of starts kind of climbing into my head. And it is just that thought. My first reaction actually is who I can work with at Stanford for AI for math. And if I were able to find such a person, and if that person had a large amount of compute, I'm not sure I would jump that quickly.

20:00Carina Hong:I think I would still jump. And you had already co-published a few papers, right? I think you've published at least 10 at this point. Yeah, a lot of them actually under a supervision profile. Oh, no, it's quite interesting. I felt like I kind of wanted to explore a little bit. I do want to say that I think generally it's good to be a nobody for as long as you can. Why is that? Your learning curve is a lot steeper. So what was the jump moment to put aside the academics, start a company? So what I did was there was like hundreds of paper on the GitHub repo called AI for Math. And it's grouped into, actually I think they've done a really good job maintaining it.

20:41Carina Hong:It's grouped into different parts. There are like AI for mathematical discovery, so finding constructions and interesting examples. There's this one part about like, I think like hammers, like much to hammer, which is this sort of very niche concept within the formal language lean that we need to get into. there is this hammer that can help you handle the low-level computations or or or derivations I read all these papers abstract over like a very short amount of time like intensely so I was basically reading these people because I was like I don't again I don't have the prior for that so then I need to be able to see what the picture is like and I start to be able to like write on paper what I thought is the way to build such a thing.

21:28Carina Hong:And obviously in conversation with a lot of other amazing people. It's a little later on, but kind of gradually start to like talk to François Charton. Some initial conversations with other AI for math researchers were also very defining. Is this a tight-knit community? It is a tight-knit community now. It was not at the time. So at the time, actually, it felt very interesting because I would write an email to someone And it felt like two travelers travel a very far distance to meet each other. It sounds like if you're in this community, this is an obvious confluence of a bunch of people and ideas.