🔬Scaling Past Informal AI - Carina Hong, Axiom Math

**Carina Hong** (0:00)
But it's for the first time now, I think, verified AI is to open up collaboration. Either it's human-AI collaboration. Well, before Blueprint, that's human-human collaboration, and lean was a grounding, was a verification, formal language. And then human-AI collaboration, like we're seeing now, future AI agent-agent-agent collaboration.
I think verified AI is for openness, it's not for meeting the requirements of closed industries. And I think, just like I think, verification should not be about, oh, I remember, like, you know, there's this article, like, chatbots make stuff up, it's a mass solution to hallucination. Verification to me is not about lousiness. Verification to me is about scaling brilliance, compounding brilliance. It's like just kind of going back to the collaboration point. It's about Ramanujan being a much stronger mathematician. He was already a really strong one. But verification helps him extend the brilliance, like both kind of like scale up and scale out.

**Brandon Anderson** (0:49)
Welcome to the Latent Space AR for Science Podcast. I'm Brandon Anderson. I build RNA therapeutics at Atomic AI, and I'm joined by RJ. Hanaki, the CTO of Miraomics, working on spatial transcriptomics. It's a pleasure to have Carina Hong, from CEO and founder of Axiom Math.
Axiom has made a splash in several different areas. First, they got a perfect score on the Putnam last December, I think. They also have the claim of the first AI to prove research conjectures using formal verification. And very exciting, they just yesterday announced quite a large Series A. Welcome to the show.

**Carina Hong** (1:27)
Thank you for having me.

**Brandon Anderson** (1:29)
You just raised $200 million, which as one of your colleagues said, this is basically the entire US math budget for math research each year.

**Carina Hong** (1:37)
Is that true, actually?

**Brandon Anderson** (1:39)
According to his LinkedIn post, yeah.

**Carina Hong** (1:40)
Okay, wow.

**Brandon Anderson** (1:42)
$250 million is our fairly annual math budget.

**Carina Hong** (1:45)
I think we should spend more on math research.

**Brandon Anderson** (1:48)
Yeah, it's kind of sad.

**Carina Hong** (1:49)
Yeah, I know.

**Brandon Anderson** (1:50)
But anyway, as a nerd who loves math, that's really cool. But I mean, I'm just like, that kind of blew my mind. Like, what?
When I heard that, I'm like, okay, so yeah, how is it $200 million, I guess $1.6 billion valuation? Yeah, I don't know.

**Carina Hong** (2:05)
Yeah, well, super excited to be here. Also, I think this is a serious day, so it's a very, very interesting, timely podcast. We're like a 7, 8 months old company, so it definitely means a lot to us. It's a really cool milestone.
We're currently about 30 people now, so kind of going into, I think this amount of funding will give us a fuel that we need to accelerate the strong execution momentum that we have so far.
I think people think of us, there are many ways to think about Axiom, people think of us as a math startup, so math startup, lean startup. The other obviously things that we do, that are formal verification, we think verification is a really good best first market format. So I think this fundraiser is going to let us explore some of the applied domains. As my colleague, CTO Shibo said in the launch video, the series that we had, it lets us broaden our dreams.

**Brandon Anderson** (3:04)
But still, like $200 million and I guess a 1.6 billion valuation, how is there a market for that? I mean, obviously, you're not doing this just for the fun of proving things, although I'm sure there's a lot of that.

**Carina Hong** (3:17)
So let's bring us back to 2024, so when O1, recently models just came out, what was Anthropic secretly working on back then? It was coding.
Everyone knows they're working on coding, like OpenAI, Meta, Axiom. Everyone has full knowledge that Anthropic was working on coding, and they just overlooked it. They thought, oh, they're at B2B place, they just want one vertical. If you think of coding as one vertical, and now look at where we are today. Coding, strong transfer learning from coding to reasoning, to basically a monopoly in the future of reasoning, and I think that's really, really shocking. The people who are working on coding, I think, back then believe in something that we believe similarly with math and lean now, which is that if you have more structured and formal data, it's going to be a lot more horizontal than the specific vertical we are tackling. So, if today we are doing math in an informal way, like the standard channel thought data, train a math model based on human preference, then I would say, well, perhaps we're just a math startup, but while we are pursuing math, we are also doing things that do have transfer learning to other domains. So I think that's kind of like the broader picture, is that while the DNA of the company remains math, and all of us are math nerds, and this is a very strong cultural statement, everyone has a great mission of having AI be a superhuman mathematician, like we are seeing on Putnam, on a batch of research conjectures. In fact, we have another batch coming.