Axiom Math raises $200M to build mathematical superintelligence using formal verification — scored a perfect Putnam

We'll get you guys some Quinn stuff. Uh

do it.

That sounds amazing. Thank you.

Bye. Let me tell you about apploving. Profitable advertising made easy with Axon.ai. Get act get access to over 1 billion daily active users and grow your business today. And without further ado, we have Karina Hong from Axiom in the TV.

What's going on?

Karina, welcome to the show. How are you doing?

Hi, great to meet you.

Great to meet you.

Uh, since it's your first time in the show, please introduce yourself and the company.

Hi, I'm Karina Holm, founder and CEO of Axium Maths. We are building mathematical super intelligence that will be a critical path to verified super intelligence.

Amazing. Uh what's your background? How did you start this company?

Yeah, so I did my um undergrad at MIT math and physics kind of did math Olympia since I was a kid and uh we are

overnight success

seven months seven months of company. So we're at downtown Palo.

Very cool. Uh, and I mean it feels like so many of the math benchmarks have been saturated. I don't know what is the goal. How do you know that you're making progress when the just the frontier models seem really really good at math?

Yeah. So, we combine the very interesting techniques in post- training reasoning with formal verification. We use this language codling which is program for proofs. And at the Pundam competition last December which is the hardest undergraduate math test we competed in real time and we got a perfect score 120 out of 120 where the best scoring LLM is 103. Uh so by deepse so there's a lot to be done you know if you combine informal and formal approach and that you will have a really strong superhuman mathematician. Okay. Talk about uh why why you think math is the pathway to general super intelligence.

Yeah. So we think that math is the sandbox for reality. You will be very quickly seeing verifiable rewards because in math there's like absolute right or wrong and especially when you have lean you can check the proof the solution step by step. You'll be able to um you know apply reinforcement learning in a much more sort of efficient way. And we have currently scaled from winning pun perfect score to solving a batch of research problems that professional mathematicians find really challenging. Wow.

And we also see this transfer to code verification.

Okay. Uh on the last uh IMO I believe everyone struggled with question six. I believe OpenAI and Google both were unable to answer question six. It was this sort of like tessillation of triangles question. I don't understand it. Uh I didn't get it right. said, uh, do you feel like you're making progress?

It came close.

I didn't even I didn't even try.

It came close.

But, uh, but but do you feel like you're the read on that particular IMO question was that it required a lot of outside the box thinking and that's why both uh many of the students who took the IMO struggled with it and that's why also the model struggled with it. Do you feel like you're the progress that you're making will transfer to that type of uh that type of math question?

Yeah. So there's this going joke that no AI could solve it because they were not at the Australian airport because what actual solution is the the tiling of the floor. So no AI was able to look down to the floor. They can't solve problem six. And uh we have seen that consistently since 2024. There were two comes problem. No AI was able to solve that stays the same in 2025. You know still haven't seen an IMO perfect score. But in this year's Putnham, we have seen some really difficult questions um by the mass Olympia hardness scale by Aan Chen. There is a question much harder than any of the five questions on the IMO that Axium solved perfectly. Okay. Um and we don't believe any other AI has done so.

How are you thinking about the impact of uh advanced AI that can solve math? I is there is there direct benefit for for just advancing the basic research that is done at a high level in the mathematics profession? Is it just once you're good at math, you can also go and you know write software that generates economic value? Like what are you most excited about?

Yeah. So um let's just like kind of take the time machine back to 2024. I think everyone was kind of aware that Enthropic was working on coding

and people didn't really think much of it and thought of that as just one vertical in the enterprise AI applications. Turns out coding is a much more horizontal bet and we believe the same thing with math too. We believe in formal math give us a pathway to verified AI to be able to revolutionize how verification has been historically done in say hardware and software. We think the temp is all AI code and we think that in a way we are looking at the roofer right the first refusal to verify or not all the AI code that will ever be produced and so this is a bet that's really relevant even if you assume AGI

I think to a lot of people verification is about sort of correcting mistakes right like sort of erasing hallucination to us we see the upside we think of verification as a way to have AI agents work with each other. Human AI work with each other to compound and scale the brilliant, right? The the int the super intelligence in a way just like Rammenujan after he learned proof writing from Hardy and Littlewood came out to be a much more powerful mathematician turn his intuition into into theorems and theorems have proofs. We think that we are seeing a similar thing happening here and math reasoning will transfer to other parts similar to code and logic. talk about the impact of verifiability on mechanistic interpretability. Just the idea of like, you know, a lot of people have fear around AI. They think it's a black box. They don't understand it. Is this going to make it more of a black box because it's doing math at such a high level that no mathematician can understand it. or does it make it more interpretable because you can verify what's happening once the AI generates its output?

Yeah, I think instead of being sort of like you know going to the machine interpretability which I know some other great companies are doing and we also work with them. Um that's about like the blackbox what's going on inside. Verified AI is about being able to trust the output once it is generated. And so um mathematicians will be able to function at a much higher abstraction than they ever ever have been. So I mean if you ask me what is the purpose of like you know proof checkers like the formal language lean in the mathematical community if they already have a pretty rigorous like peer review process right like all the mathematicians will just peer review each other's work I would say that it's because you know the lean and all the tactics within such as grind is able to cover all the low-level deduction and for mathematicians to focus on the high level navigation and then do math at a much more um compressed timeline. So I think I'm we're quite excited about the future where mathematicians because of this sort of increased supply of reasoning can like produce way more breakthroughs than before and that you know can then flow to other applied scientific domains. That should be quite interesting.

You raised a lot of money $200 million. Congratulations. Are you is is there a large compute budget within your organization because of that? Yeah, we are going to spend the um new capital in compute and hiring. We are also very excited to continue the amazing team building progress we have been I think I feel fortunate every day to work with this worldclass team and we want to you know have people who are interested in program verification to also join us.

Amazing. Well, congratulations. Thank you so much. We got to hit the gong for the $200 million

for Axiom.

Wow, that was a that was a big hit. Thank you.

That's a that's

it's a big round and it's a big idea and this has been a great interview. Thank you so much for taking the time to come chat with us. I'm sure we'll be back and we'll talk to you soon.

Have a good rest of your day. Goodbye.

Let me tell you about Gusto, the unified