跨越非正式 AI 的规模化——Carina Hong、Axiom Math

Karina Hong

But I think, for the first time now, verified AI is opening up collaboration. It's either human-AI collaboration or, before AI blueprinting, human-human collaboration. Lean was the grounding, the verification formal language. And then there's human-AI collaboration, like we're seeing now, and future AI-agent-to-agent collaboration.

I think verified AI is for openness. It's not for meeting the requirements of closed industries. And I think verification should not be about, “Oh, I remember there was an article about chatbots making things up. There are hallucinations in math solutions.” Verification, to me, is not about lossiness; it's about scaling brilliance, compounding brilliance.

Going back to the collaboration point, it's about Ramanujan becoming a much stronger mathematician. He was already a really strong one, but verification helps him extend his brilliance. It helps scale up and scale out.

Brandon Anderson

I'm Brandon Anderson. I build RNA therapeutics at Atomic AI, and I'm joined by RJ Honicky, the CTO of Mira Ox, working on spatial transcriptomics. It's a pleasure to have Karina Hong, CEO and founder of Axiom Math. Axiom has made a splash in several different areas.

First, they got a perfect score in the Putnam last December, I think. They also claim to be the first AI to prove research conjectures using formal verification, and I'm very excited that they just yesterday announced a sizable Series A.

Karina Hong

Thank you for having me.

Brandon Anderson

You just raised $200 million, which, as one of your colleagues said, is basically the entire U.S. math budget for math research each year.

Karina Hong

Is that true, actually?

Brandon Anderson

According to his LinkedIn post, yeah.

Karina Hong

Okay, wow.

Brandon Anderson

$250 million is apparently our annual math budget. We should spend more on math research.

Karina Hong

Yeah, it's kind of sad, but—

Brandon Anderson

Yeah, I know. But anyway, as a nerd who loves math, it's really cool. That kind of blew my mind. I was like, “What?”

Karina Hong

Yeah, we're super excited to be here. Also, I think this is a Series A, so it's a very interesting, timely podcast. We're a 7–8-month-old company, so it definitely means a lot to us. It's a very cool milestone.

We're currently about 30 people, right? I think this amount of funding will give us the fuel that we need to accelerate the strong execution momentum that we've had so far. People think of us in many different ways. People think of us as a math startup—a math startup, a Lean startup.

The other obvious thing that we do is formal verification. We think verification is a really good first market for math. I think this fundraise is going to let us explore some of the applied domains. As my colleague, CTO Shumo, said in the little launch video, this Series A lets us broaden our dreams.

Brandon Anderson

But still, $200 million and, I guess, a $1.6 billion valuation—how is there a market for that? Obviously, you're not doing this just for the fun of proving things, although I'm sure there's a lot of that.

Karina Hong

Let's bring us back to 2024. When the o1 models recently came out, what was Anthropic secretly working on back then? It was coding. Everyone knew they were working on coding. OpenAI, Meta, Axiom—everyone had full knowledge that Anthropic was working on coding. They just overlooked it.

They thought, “Oh, they're a B2B play. They just want one vertical.” People think of coding as one vertical. Now look at where we are today: coding has strong transfer learning to reasoning, to basically a monopoly in the future of reasoning. I think that's really, really shocking.

The people who were working on coding back then believed in something that we similarly believe with math and Lean now: if you have more structured and formal data, it's going to be a lot more horizontal than the specific vertical we're tackling.

If today we were doing math in a formal way like standard chain-of-thought data and training a math model based on human preference, then I would say perhaps we're just a math startup. But while we're pursuing math, we're also doing things that do have transfer learning to other domains.

I think the broader picture is that the DNA of the company remains math. All of us are math nerds, and this is a very strong cultural statement. Everyone has a great mission of having AI become a superhuman mathematician, like what we're seeing on the Putnam, the IMO, and research conjectures. In fact, we have another batch coming.

We're also thinking that this is going to be fundamental to verified reasoning. We've talked a little bit about verified AI, and I want to talk a little bit about verified AI next.

Brandon Anderson

Yeah, yeah, yeah. I have several things I want to ask. I want to hear about verified AI, and I do want to dig in a little bit. Do we know that Anthropic, OpenAI, and everyone else aren't doing formal verification and using it for their rollouts and whatever?

Karina Hong

I have a lot of rumor mill that probably shouldn't go on the record. Researchers talk; they play card games. But there are really interesting reasons for whether they are or aren't doing it. I think that's the takeaway I have: if you're at a frontier lab, the direction can change a lot for reasons beyond your control.

I want to bring us back to the AlphaProof moment. AlphaProof was such an amazing achievement. The 28-out-of-42 performance in 2024 was the IMO moment for me. It was not the gold in 2025, because across 2024 and 2025, AI models could solve all the problems that were not combinatorics.

The only difference is that if you get all the problems that aren't combinatorics, you get 28 in 2024 and 35 in 2025, because there was only 1 combinatorics question in 2025. After AlphaProof, we didn't see a lot of formal math results or progress from Google DeepMind, and that's actually because of reasons that are not necessarily technical.

But if you're at a startup and you have a singular focus on formal math and verified AI, you get to work on really cool problems for a long time. You have a much higher likelihood of getting to where you want to be in terms of progress and breakthroughs.

Brandon Anderson

So, just define that for us.

Karina Hong

A lot of people think about formal verification as an ancient subject. It existed way before deep learning, back in the time of rule-based computer science. There's been a really strong push for formal verification since the 1980s.

There are interesting historical anecdotes, such as how I think the Paris trade union demanded that the automatic switching of the subway system be formally verified for safety purposes. That's quite an interesting trade union for technology.

Around the time of the Challenger disaster, both before and after, the European Space Agency was using formal verification for the Ariane spacecraft. Boeing and Airbus use formal verification, too.

In more recent years, I think there's been a lot of push for automated reasoning at AWS, because they have a lot of enterprise customers that really require things to be 100% verified, with no edge cases missed. General testing doesn't satisfy that need.

A lot of people think about verification as something annoying because it's a tax-and-compliance thing. It's making sure that we're good to go, but that's really not the point. Our competitor, when they launched, talked about formal verification for reasoning. They talked about it in the context of hallucination, and maybe for them formal verification is about lossiness and hallucination.

For us, no. For us, verified AI is about brilliance. It's about scaling and compounding superintelligence. This is a deep point, and sometimes it takes a little bit of explanation.

If you think about brilliance, for example, Ramanujan was a brilliant mathematician. He was able to find a lot of interesting formulas just by intuition, before he knew how to write proofs. He went to Cambridge, worked with Hardy and Littlewood, and in the famous movie The Man Who Knew Infinity, there's a storyline about how hard it was for Hardy to force him to stop relying on intuition and do proofs.

After he learned proof-writing, he became a much more powerful mathematician. His intuitions turned into theorems, and future generations of mathematicians built on those theorems. It's a way to scale and compound the intelligence that we already have.

Another example is that mathematicians have been writing code in English, or in their respective countries' natural languages, for thousands of years.

And why do I call it writing code? Because there's this sort of community standard of rigorous logical deduction. Everything has to be step-by-step correct; otherwise, you will get outcasted by your math community.

Shawn Wang

More rules in the community.

Karina Hong

So it's interesting, right? That is kind of human-mathematician-enforced, right? And so it's a peer-review process. Peer review to get a paper currently takes 2 years.

Proof assistants and formal proof checkers like Lean still found their place. Why? If I'm a mathematician and my work can be peer-reviewed by other humans, why do mathematicians even play with Lean? Why do we even talk about Lean-based assisted theorem proving? It's because it handles a low level.

For example, we're not even talking about AI. We're talking about a grind tactic in Lean. It can currently handle a lot of math proofs at a very low level. This is pretty shocking because I have seen another company working in the same space. I look at some of their demos, and it can actually be completely handled by grind, which is a tactic in Lean.

Shawn Wang

Can you explain what Lean is to non-experts?

Karina Hong

Yeah, I think our order is a little wrong. Lean is a computer program for math proofs. It is a formal language, just like its cousins Isabelle, Coq, or Rocq, and some other further cousins like Daphne and Agda. There's also Hoare logic.

Shawn Wang

What does it do?

Alex Meinke

It basically—if you have a proof written in Lean, and assuming there's nothing weird happening, such as an unintended use of `sorry`, which is a tactic that lets you take things for granted, and assuming everything is safe, then you're happy. There are tools like proof checkers and safety verifiers, and Axiom recently rolled out a verified proof that's like 100 times faster than comparator.

Once you execute that program, once it compiles and tells you that it's correct, then the proof is actually correct.

Shawn Wang

So it's like a type checker.

Alex Meinke

Yeah, that's based on this result called the Curry–Howard correspondence, which turns proofs into programs. I want to talk about the magic of Lean. Why I think it's a really good programming language is because, on the one hand, if you don't care about the formal part at all, if you don't care about the logic part, and you just want to use Lean to write code, you can.

We have had candidates—currently, the person is working at the Lean FRO—who wrote AutoGrad in Lean during our interview process.

Shawn Wang

Is it a Turing-complete language?

Alex Meinke

That's right. You can do a lot of things with Lean. It's a functional programming language, right? You can use it to write code, and you can use it to do math. Two in one.

Shawn Wang

Okay.

Alex Meinke

Going back to what I was getting at, if mathematicians are already enforcing that most proofs—say, maybe not all mathematicians, but the ivory tower and people in academia—all proofs are correct, why do we even need Lean, the proof checker? It's because Lean has tactics that help them handle the low-level calculation or proof or deduction—not calculation—so that they're able to navigate in the high-level intuition space.

This is my point: It is not about formal verification or verified AI. To us, it's not just about handling or kicking out the lousiness, the hallucinations, and the mistakes. It's about scaling brilliance. It's about superintelligence.

Shawn Wang

Terence Tao has a great video about using Lean as a way to collaborate.

Alex Meinke

That's another point I want to talk about, right? A lot of people think about, what is our market? It has to be some really niche industrial or societal area that is mission-critical, safety-critical. No, that's not the TAM. The TAM is all code. The TAM is a right of first refusal on all AI-generated code. By “right of first refusal,” I mean you get to choose whether you want to verify it.

This is the important part I want to get across: People talk about formal verification as almost painful because it has all these stringent requirements.

Shawn Wang

Up until now, it has been.

Alex Meinke

Well, yes. And to us, verified generation means performance gain. It means higher sample efficiency. It means a startup like us—with, you know, we still raise some money, but a lesser compute budget and lesser data budget than frontier labs—will be able to match and even exceed performance on superhuman tasks.

For the Putnam Exam, competed in December 2025, which we did in real time, MASS Arena, which is this organization that evaluates a lot of LLMs, found that the best LLM, DeepSeek, got 103 points out of a 120-point exam. The best human, obviously, we now know is a student from either MIT or Chicago. We don't know which one because they don't announce the top 5 winners' scores. They got 110, and we got 120.

It's the first time, actually. I remember when we were starting this, people were like, “Is it even possible that a formal math system with so many orders of magnitude less data can match or beat an informal LLM?” Putnam is the first time it beat one.

We're not thinking about it just in terms of the painfulness or the challenges it poses. We're thinking about the performance gain from verified generation, the improvement, and the fact that you can expect RLVR for Lean to improve because of evidence of RL encoding. This is the second point I want to make about how to think about verification and verified AI.

Shawn Wang

So maybe we can talk a little bit about why. Can you describe what is different about what you do versus what the frontier labs are doing, at least when they're building their standard RL-enhanced LLMs? What's different about what you do?

Alex Meinke

Yeah. We heavily rely on data called Lean data. We talked about Lean as all the data that we have in Lean proofs; you know it's correct. So you know whether it's correct or not. That's quite important. We have a system of models. These models are post-trained using RL or FFT.

Shawn Wang

So you find some sort of foundation model that you get off the shelf, and you post-train it or continue training it?

Alex Meinke

Yeah, and there's obviously an inclination toward open-source base models.

Shawn Wang

Does it speak English?

Alex Meinke

Yeah.

Shawn Wang

It probably knows how to code.

Alex Meinke

Yeah.

Shawn Wang

But you also fine-tune it or continue training it?

Alex Meinke

Yeah, and the base model may be similar to what everyone else is using as well, right, if they're not pre-training their model.

Then we basically do RLVR for formal math. There's, I think, a standard pipeline, or tricks of the trade, that people use. We try to innovate a ton, as much as we can. I think that we found scaling inference to have almost no ceiling: recursively decomposing a proof goal into many subgoals and learning to backtrack as well.

Shawn Wang

Is there a risk that you start out with what you know in a certain domain of datasets and so on, and then you start rolling out recursively in a space, but now all of your training data is localized in some domain that is only logarithmically growing in some large space from your initial training data? So you could get trapped, essentially, in that you could be really good at this, but you just created a big jagged frontier where some other domains are just far from that.

Alex Meinke

That's the distribution shift we're talking about. So, yeah, it is an open question whether a system that can do really well in number theory can do well in another field of math.

Shawn Wang

Yeah, exactly.

Alex Meinke

Well, actually, I think the way we think about it is, it depends. It depends on whether topology has a lot of existing definitions that serve as the math infrastructure. What people have found in the past is, when people were building out mathlib for the algebra groundwork, they can just—

Shawn Wang

So mathlib is the Lean undergraduate library.

Alex Meinke

That's right.

Shawn Wang

So it's like all the proofs that you learn in undergraduate math, and they're all sort of in Lean.

Alex Meinke

Yeah. For example, some of my friends who are currently at Axiom—it's a crazy full-circle moment—Kenny and I have been friends for 5 or 6 years, and he was the first one to tell me about Lean. He was working with Kevin Buzzard to build out mathlib.

It's a lot easier to codify algebra in mathlib than analysis. That's interesting, because for analysis, a lot of the definitions around convergence, limits, and so on become tricky. I don't think there's a lot of topology in mathlib today in terms of differential topology and differential geometry, that kind of stuff. Our system likely will not do very well on those domains because it doesn't even have definitions to build on top of.

For the places where the definitions are in, we're actually doing quite okay in terms of distribution diversity. We have good performance; we've solved open research questions in number theory, commutative algebra, algebraic geometry, and some discrete math, including combinatorics and probability.

Shawn Wang

Earlier, you said that with the Putnam exam—the 2024 version—all of the questions that AlphaProof did not get right—

Alex Meinke

The IMO, the International Math Olympiad.

Shawn Wang

For the IMO, all of the ones they got wrong were in combinatorics. Is there a weakness there in that specific domain?

Alex Meinke

I would say so. For Olympiad math, people see combinatorics as a little bit trickier because the steps are quite creative. I'm a human, and when I have friends who are really good at combinatorics—which I never consider myself to be at the top of—I’m kind of better in number theory.

But I know some people who are IMO gold medalists with perfect scores, Putnam fellows with perfect scores, all the way through. When they do tricks in combinatorics, I'm like, “I don't know how you thought of that.” But after you give me that construction, it actually becomes a lot more tractable.

I think a Lean-based system will struggle in those very creative places, which is why we at Axiom also invest in something called Mathematical Discovery. It does not use Lean, and we have some major news in the coming weeks. Basically, we're open-sourcing the entire codebases of Mathematical Discovery.

Shawn Wang

You want to tell us a little bit?

Alex Meinke

Yeah, sure. We currently have 2 codebases being open-sourced. The goal is that if you're a mathematician or a theoretical physicist and you have a problem that you would like to solve—for example, you want to find a construction that is a very complicated graph construction—then we will suggest that you follow a very detailed manual intended for mathematicians to run the code that we write.

It's a tool for mathematicians to make mathematical discoveries. Mathematical discovery is the idea that proof is not enough for math. In fact, before you start proving something, you don't know where you want to start, so you try to construct some interesting examples.

These can usually be sequences, right? If you want to understand a property of a sequence, you write out a few of the first terms. This can also be graphs. If you want to figure out what the graph that you're looking for should have to satisfy a certain property, then you start by doing some simpler version of the graph.

Now, constructions cannot be done by Lean. So we believe in having AI for math discovery. We have one of the OGs in that field, François Charton, a member of the team at Axiom. He previously did PatternBoost and Int2Int, and set out to disprove a 30-year-old conjecture by finding a counterexample.

Shawn Wang

He found a solution to a 130-year-old problem, the global Lyapunov function, which is a kind of mathematical object showing the stability of the three-body problem. We are thinking that mathematical discovery tools should be open to the math community, so we are open-sourcing entire codebases for that.

Shibo Wang

So, discovery meaning it makes new conjectures, or it—

That's a pre-conjecturing step, actually.

Shawn Wang

Okay. Oh, I see.

Shibo Wang

Yeah, you start to form intuitions. If you're a mathematician and your goal is to solve a really hard conjecture, Axiom Prover can't just solve it for you. You might want to try to formulate some sort of lemmas or conjectures that you then want to give to Axiom Prover.

Shawn Wang

(Snorts.)

Shibo Wang

If you're a human mathematician, you will start by wanting to formulate that conjecture. You don't know where to go. You want to find constructions. The codebases that we're going to open-source are going to help you, hopefully significantly.

Shawn Wang

One thing that a lot of computer scientists listening will immediately think of, especially when you're talking about formal verification, is Rice's theorem, decidability, the incompleteness theorem, and perhaps some arguments about computational complexity in LLMs. I'm curious to hear how you're navigating this space.

Rice's theorem says you cannot prove nontrivial things about programs for all programs, right? So how are you navigating this space? Obviously, formal verification is able to do some things.

Shibo Wang

Yeah. I think it's very clear that there's a theoretical result telling you that you cannot formally verify all programs, right? But I think it's good to formally verify a majority of the useful programs.

I remember this MIT little documentary—or not a documentary, an advertisement for admitted students—and there's this famous line by Tim the Beaver, the mascot of MIT, saying, “What does theory give you?” Which is kind of like, it doesn't stop us from—

Shawn Wang

Mhm.

Shibo Wang

The goal that we have for the future is: suppose you're doing the coding and you want to write code for a really complex task. Currently, it's front-end websites, but in the future we might want to write code for much more complicated things, even whole distributed systems.

Then we want to be able to decompose it. There's maybe a high-level sketch plan. We can make this; other people can make this. Say you have Claude give you a breakdown into 10 things. At one point, it will decide to call Axiom, and Axiom will give you a computer program that you know is formally verified. Or it will say, “This is still too hard for us.”

Shawn Wang

So you write the program, give it to Axiom, and it makes changes to it, maybe?

Shibo Wang

We're talking about 2 sort of phases. It's possible that we are the verification partner: you already have a computer program and you want us to verify it. In fact, GPT found a proof to an unsolved Erdős problem, and our competitor, Harmonic's Aristotle, verified it.

But we want to do verified generation, right? We might want to say, “Hey, this little component—everything that we generate and provide for you—is formally verified.”

Shawn Wang

I see. So the idea would be that you generate, or co-generate, both. I can imagine this fitting into the idea of a promise, or—sorry, sorry—and then a sorry.

(Laughter.)

Which is a Lean sorry. A Lean sorry meaning it's a lemma that is unproven, but you're just taking it as given until you have the time to prove it, right? Is that a good way to think about a sorry?

Shibo Wang

That is a good way to think about a sorry, but not necessarily in the coding context.

Shawn Wang

So I can imagine you can say, assuming that this module is verified, then this module is correct. And that you can decompose a problem small enough that you can verify. Is this what you're saying?

Shibo Wang

Let's say we want to do web code control flows.

Shawn Wang

Yeah.

Shibo Wang

Right, that's quite hard. You will likely break that down into multiple steps. Then it will continue to break down these steps into more fine-grained steps.

Shawn Wang

Yeah.

Shibo Wang

At one point, you want something that is absolutely correct.

Shawn Wang

Yeah.

Shibo Wang

This is also something that is likely within reach. Then we want to generate both: a piece of computer program, and underlying it, a guarantee that there's also a proof that has been generated. That proof tells you that the thing you specified—this program—is something I can solve for you.

Shawn Wang

Yeah.

Shibo Wang

So the vision we have is that anything that can be—which, anything is, and it's a little bit marketing because, as you said, there's a theoretical bound—but mostly, well, I'm not sure, really, hopefully, anything that can be defined can be executed; anything that can be specified can be proven.

The way I think about it is, if you have a program times a statement or a problem, it maps to verification conditions times a proof. The program verification community has given you, say, the verification conditions—and we're trying to recruit a really strong team to help us do that—and Axiom Prover is going to give you the proof.

Shawn Wang

So just help me map from the program to the proof. I could say, “This 2-line Lean program verifies whatever I claim it solves.” How do I know that it actually verifies the thing that I think it verifies?

Shibo Wang

For example, there's this benchmark called Code Verifier. It's a code verification benchmark that's supposed to be Lean-friendly. Every problem is a coding problem, and the goal is to generate a code part and a proof part—2 different computer programs.

The goal is to generate code with proof: the code that supposedly solves this problem, and then the proof that this program indeed does solve the problem.

Shawn Wang

I see.

Shibo Wang

Now, how do people do on this benchmark? I want to talk about this a little bit because it's interesting. It was written, I think, by Berkeley and Meta researchers in 2025, and they found that whatever version of GPT they evaluated had a pass@1 score of 3.6%, and iterative was something like 22%.

How do the formal math system models do? Cobra, which is a system—because in a system you iterate and refine, pass@1 doesn't quite work—but still, they evaluated pass@1 of the system at about 11% to 12%.

And then also DeepSeek-Prover and Gödel-Prover, very strong prover models, are at 11% or 12%. I think our competitor released something last year and got 96% on the Lean proof part, and we recently, with no modification to the Ponym system, saw 99%: out of the 189 problems, we solved 187. We missed only 2 Code with Proof problems.

If you want to train something to do code with proof and you want to do reinforcement learning, it’s actually quite annoying. If you want the proof to be informal math, that’s just a mixed objective function: your code is something like Python, and your proof is, say, a natural-language math proof. You will not have very strong RL performance, right? But if you have proof as Lean and you have code, you can choose Rust, which is a strongly typed language. It’s smarter; it’s more convergent. So you’re going to have much better performance.

Shawn Wang

I can’t wrap my head around how you tie it together. I can say that this proof solves Fermat’s Last Theorem, right? But I don’t know that—it’s 2 lines of Lean. Obviously, it doesn’t. So how do I know that the program I wrote matches the proof that I generated?

Shibo Wang

You will basically look at the coding problem and look at the program, and then try to see if it satisfies the verification conditions.

Shawn Wang

But how do I know? If I read it—

Shibo Wang

Right.

Shawn Wang

I can eyeball it and say—and traditionally, this is how mathematicians have done it—they take the paper and read it and say, “I agree that this proof solves the problem.” Then another person says, “No way it doesn’t—for example, look at this.” People disagree, and eventually there’s consensus that this proof solves this problem. So how are you crossing—

Shibo Wang

You check it step by step, right?

Shawn Wang

Yeah, right, right.

Shibo Wang

Yeah, yeah. So you basically look at the verification conditions and see if it actually satisfies them.

Shawn Wang

So suppose we’re looking at a piece of computer program, right? Whether it actually solves the coding problem—you’ll have a judgment about that, right?

Shibo Wang

Yeah. So you will not solely rely on testing, even though that is one way.

Shawn Wang

So someone looks at the proof and says, “Yeah, that actually solves the problem that we think it’s supposed to solve.”

Shibo Wang

But then now you’re basically producing a formal verification program that satisfies the verification conditions about this program and this statement. So again, the function is taking you from the program and the statement to verification conditions and proof.

Shawn Wang

Okay, so I can see how this works on a benchmark. If I have, let’s say, a flight control system that is very—

Then the problem becomes very annoying: the specification. Even if we say something is successful, we have a specification problem. Here comes a bank saying, “Please prove a really safe financial audit for me,” right?

Shibo Wang

Yeah.

Shawn Wang

What does that mean? We can’t specify. Humans are bad at specifying everything that we want, right? There’s always some sort of thing that we haven’t specified, and if it’s not specified, it’s not proven.

Shibo Wang

Yeah, so we’re not there yet.

Shawn Wang

Okay.

Shibo Wang

Currently, again, the vision is that anything that can be specified can be proven. Now, obviously, people have been really good at that; that’s maybe where informal reasoning comes in. Informal reasoning can—and this is where I want to call out the literature on testing—testing is great because testing is like, “Hey, have you thought about that?”

I want to highlight the work on mutation-based LLM unit-test generation by ex-Meta CTO Shubo, who was a director at Facebook AI Research. The way you think about it is that the AI will be like, “Have you thought about this, this, this case?” This is a little bit like conjecture. Conjecture is going to help with the specification.

Shawn Wang

I see.

Tudor Achim

And then the prover does the proof.

Shawn Wang

So this is an interactive process with the person, so that we’re actually getting good—

I think this is the future of coding.

Tudor Achim

Yeah.

Yes, I think this is the future of coding. Even if we suppose, given the assumption that everything can be formally verified, studying automatic test generation is still interesting because it is basically giving you a specification proposal. And then another thing is autoformalization, right? That’s the ability to convert something that is more informal into something that is more formal: autoformalization.

Suppose I have a coding problem written for ICPC, and this problem is written in English—Alice and Bob, blah blah blah. Now I want to convert that into a formal statement, like a formal spec. How do I do the autoformalization step, right? This is going to be difficult because I have not solved the problem yet, so I don’t have any signal. I don’t have any grounding. The test-case input-output pairs are going to ground my formal spec.

Shawn Wang

I know I have to know: I’m going to give this input, I’m going to give this output, and it has to have these characteristics. So I write test cases and I write a— is there an equivalent in Lean of this, where the specification is where you just know the outcomes that you’re expecting? So you have the statement of the result, but the proof is completely unproven.

Tudor Achim

That’s actually quite annoying, because a lot of the time it’s proof, so you don’t actually have the numerical answers to ground it.

Shawn Wang

Okay.

Tudor Achim

So autoformalization is quite a hard thing to do because it’s hard to ground the autoformalization of a statement. You can obviously ground the autoformalization of a proof, because you can then just run it. But you need a human to eyeball it.

Shawn Wang

How big is a Lean proof of a formalized program of significant size? Do they grow with the size of the program, or do they grow superlinearly?

Tudor Achim

Currently, for each line of code written, there could be 20 lines of proof.

Shawn Wang

Okay.

Tudor Achim

It’s not looking that great.

Shawn Wang

But is that a linear relationship, or as the complexity of the program gets greater, does it also grow so that it’s like 40:1?

Tudor Achim

I don’t have a good answer to the scaling law of that.

Shawn Wang

Okay.

Yeah, because I know that’s a problem in formal verification, right? You have these huge programs, and you have to have these very, very long proofs for even simple programs. So do you run into limitations in the capabilities of LLMs when you start to get too large?

Tudor Achim

What we believe fundamentally is that we’re building a reasoning engine.

Shawn Wang

Mhm.

Tudor Achim

We’ve seen Axiom Prover deal with really huge proof trees. We’ve seen it scale from 40 nodes to 4,000 nodes.

Shawn Wang

Wait, sorry—Aristotle is the LLM?

Tudor Achim

Axiom Prover is an ensemble system of multiple models that we do post-training on. It also includes, obviously, the tools that we have open-released.

Shawn Wang

Sorry.

Tudor Achim

Yeah, in other words, we’ve seen it being able to deal with more and more complex tasks.

Shawn Wang

I see.

Tudor Achim

We don’t think it’s probably bounded. You could ask, is it bounded at one point only by the pretrained base model?

Shawn Wang

Yeah.

Tudor Achim

I think that’s a good question. Mid-training could be very interesting, because a lot of the capability gain does come from that part, right? You could argue that even if you try to reinforcement-learn some person who is not very talented, that person might perform a lot less well than an un-post-trained Ramanujan. You can argue that way, but whether that’s the reality of things is another question. At one point, we might consider doing that.

But we think there’s so much room to push.

Shawn Wang

So you just feel like there’s so much overhead right now, or so much—

Tudor Achim

Space to grow.

Shawn Wang

Space to grow—that you’re not running into theoretical constraints at this point. I just wonder because there have been recent results in the computational complexity of the problems that LLMs can solve fundamentally, and I don’t think they’re really a concern when I’m writing code with Claude Code. But I can imagine problems becoming big enough in a system like this where you have a gazillion lines of Lean. You can’t get them into the context window, so you have to be smart about that, and then you have to summarize, and then you’re summarizing and summarizing, and pretty soon you’re kind of losing track of what’s going on.

It just seems like with a very large system like that, you might run into a—

Tudor Achim

Yeah, I think this is interesting. It’s always a problem of abundance. Really, the mathematical code-discovery renaissance has come; an agentic prover does try to prove everything. You end up with tens of thousands of lines of Lean proofs.

First of all, auto-informalization is a lot easier than auto-formalization, minus the problem of no grounding, right? Every model has seen a lot of text and a lot of Lean, so you can always convert that Lean back into informal language. Then there’s the problem of how you know whether you’re correct or not.

You can rely on cyclic consistency. You formalize again and then prove program equivalence, something like that.

Shawn Wang

Oh, so you informalize and then formalize?

Tudor Achim

Yeah, you can use it to ground and make sure that it still works. Auto-informalization is obviously a less hard problem, so you can always do that. For a lot of the Lean code that we output, we can have an informal summarizer for big chunks of Lean. It’s actually doing okay.

There’s another question that I think is very interesting. I think there was a panel at ICML and COLM last year, at the AI for Math Workshop. Leo de Moura, Jeremy Avigad, and Shubho, the CTO, were there. They were talking about whether humans or mathematicians would, at some point, stop trying to understand what’s going on there.

Suppose you’re a very ambitious mathematician and you want to prove the Riemann hypothesis. Bang, here’s a Lean proof. It’s actually correct, and it’s just a problem that’s 1 million lines long.

Shawn Wang

Yeah, isn’t that a big negative for the community? Usually, when someone comes up with a big proof of something, oftentimes—

Tudor Achim

Yeah, I was about to get there. Will that negative outcome happen? That was the question the panel was discussing. It’s completely hypothetical. No one’s model system can prove the Riemann hypothesis, right? So, disclaimer: please don’t cut that part.

Shawn Wang

I just did that.

Tudor Achim

Will people still try to understand what’s going on? I think the answer is usually yes. Curiosity and the desire to understand what is going on, mathematically or in other domains as well, is a basic human need.

I think that’s a dose of optimism in an era of verified superintelligence, suppose we get there. Even if all the outputs are going to be produced at a much faster pace and in much greater volume than humans could possibly consume, people are still going to try to consume them—at least the ones they deem important.

Basically, attention is the bottleneck. If attention is the bottleneck, then intuition and taste—what statement is probably worth human consumption, and perhaps what is worth spending finite computer resources on—that’s where human mathematicians’ taste will always guide us. I think that’s incredibly beautiful.

Shawn Wang

Is it worth internally taking results you can prove one way and then trying to send your system down many different routes to get orthogonal, conceptually orthogonal proofs? That way, you get a diverse set of different ways of reasoning about the same thing.

If you’re given a problem, it could be valuable to say, “Here’s the brute-force, natural way that maybe some humans would do it,” and then there’s a much shorter, elegant way of doing it. Have you thought about training your models to be elegant in some way?

Tudor Achim

Yeah, at one point we’re going to get there because I think the conjecture will probably depend on what we mean by taste and elegance.

Shawn Wang

It feels like an alignment problem to me. Who gets to say what is elegant? Humans get to say what is elegant, right?

Tudor Achim

That’s what I mean. There’s something about hard work, right? What you work hard on is what you’re going to be good at.

We’re going to have a problem about that, I think, in a lot of domains as well, not just math. How do you become that senior programmer with really good high-level understanding—full-stack understanding, high-level and low-level—if you haven’t spent a year of training?

Shawn Wang

I mean, I would argue that you don’t. This is very philosophical, but I don’t need to be good at assembly-language programming, right? Not many people are good at that. A few people are, because it’s important for their job.

Tudor Achim

It’s not just experience, but your curiosity.

Shawn Wang

Yeah. But it feels a little different to me. Not being good at proving things, for example, seems like a fundamental gap. Maybe my mind doesn’t develop in the same way if I’m not doing that. Whereas if I’m just not good at assembly-language programming but I’m good at higher-level programming, maybe that doesn’t matter.

Tudor Achim

I think that’s probably because of how the education system—the pipeline—works. If you don’t show early signs of brilliance, you sometimes don’t go through the process of pretraining in math.

Shawn Wang

Yeah, yeah.

Tudor Achim

Right, so maybe you can argue that you don’t need to learn everything to develop a sense of taste. But there’s a threshold you need to meet.

Shawn Wang

Yeah.

Tudor Achim

For example, you probably need to be able to code, even if you don’t need to understand assembly language. That thing might transfer into my intuition. My intuition might transfer from Olympiad math problems into some other research areas I tried to pursue. The transfer to combinatorics is more direct—it’s very similar—and number theory could be farther, but still okay.

When it gets to something that’s a lot more different from Olympiad math, the transfer isn’t that strong. But, as you said, you need to be diligent. You need to go through some amount of training.

Shawn Wang

Yeah.

Alex Davies

And if you only rely on strong AI, that doesn’t happen.

Shawn Wang

I want to switch gears.

Alex Davies

Yeah.

Shawn Wang

You mentioned software verification. What are the domains? How are you going to make enough money to justify the valuation? And congratulations, by the way.

Alex Davies

Thank you.

Shawn Wang

So, give us the high-level summary. What’s the vision that you put in front of investors about why this actually makes a lot of money?

Alex Davies

First of all, this one is kind of preemptive, so I think a lot of investors have pretty high interest in Axiom. In terms of what we believe in, we believe the future of coding is going to be somewhat constrained by verification capability. We believe solving formal math is a very natural starting point. Then, by extension, you can increase verification capability across hardware and software.

For hardware, for example, that’s quite revolutionary. As far as we know, there’s no partial credit for a mostly verified GPU.

Shawn Wang

No. And so what is—

Alex Davies

It’s all or nothing. It is all or nothing, and you do need a perfect prover. I want to stress this point: suppose I’m someone who loves solving math. I think there are a lot of Twitter users who enjoy Pokémon-like hunting for those problems.

I just try to use a nondeterministic GPT to get the full proof for that. I can do that many, many times. I might succeed and I might not, and I might not have a problem with whether I actually succeed or not.

This absolutely does not work for hardware verification. For those kinds of domains, which I call hardcore-verification-needed domains, it is a pain point. It is a current pain point. There are hundreds of humans and thousands of licenses dedicated to solving a single logic-verification problem.

Shawn Wang

Just as an aside, my understanding is that the industry standard for the design-to-verification ratio in an ASIC project is like one to three, one to—

Alex Davies

One to three and one to four, correct—both in size and in duration.

Shawn Wang

Yeah. Right, so let’s call it that.

Alex Davies

Yeah, exactly. And then I think it’s a must-cover.

For software verification, it is interesting, right? As we probably all realize, my nephew wrote code for a Lovable website. There’s absolutely no need to formally verify that piece of code. Why would you?

I heard a story from Cade Metz, the New York Times reporter. He told me the story, which is—

Shawn Wang

Yeah.

Alex Davies

However, if you think about the time of agents, my OpenClaw can probably do all sorts of things and probably do some bad things.

Shawn Wang

OpenClaw can decide to text something bad to my professor, right?

Alex Davies

Yeah.

Shawn Wang

And you can say that perhaps that's a problem of formal verification. Probably still not, right? You can change something about the action space and make it more limited, so you don't need to rely on formal verification. So, you can have a lot of cases, but you can think about maybe an enterprise that is dealing with a lot of regulatory stuff using agents. They might want to do something like it. It's their choice.

Alex Davies

But I will argue that the improvement of verification capability, both in latency and in accuracy—all this stuff, the performance holistically—is going to determine whether people rely on formal verification or not.

Shawn Wang

Sure.

Alex Davies

So, in a way, we want to make it so good that basically we can make that a choice.

Shawn Wang

So, why did the investors think that you could do this? People have been working on verification for so long, and I think everyone agrees it's an important problem. If I can just have a verification proof for every program that I write—“Hey, Claude, give me the proof also”—and then it produces it and it looks good to me, I would absolutely do that. So, what was it that the investors saw, in your opinion, that persuaded them that this is the moment to put in $200 million or whatever?

Alex Davies

I think when it comes to faith, you either have it or you don't. So, you either dream the dream with us or you don't, and that's okay. Because when we realize the dream, the company is going to be worth $10 billion. I think that's the feeling that I have: We believe verification is the critical part to superintelligence. Our version of superintelligence is absolutely verified. We don't think there's any other possible future. We do not believe—and I'm going to say it on the record—that an informal math system is going to be the math AGI solution.

Shawn Wang

Why not?

Alex Davies

We just don't believe that.

Shawn Wang

I mean, the counterargument is, “We just do a lot of good RLVR, and we've seen GPT solving some of those problems,” and whatever. So, why do you think that runs out of gas?

Alex Davies

Yeah, so you can say that if you're already doing frontier math and you're a frontier lab with infinite resources, why would that run out of gas? It's, by definition, not running out of gas, right? Do you think “infinite” means there's no running out of gas? I don't think it's going to scale to superintelligence.

Shawn Wang

So, you think that you run out—you run out of money, basically; you run out of power?

Alex Davies

We, as a startup, first of all, cannot do that. But we generally think that formal math, by converting math proofs to programs, to code, gives us much better performance.

Shawn Wang

So, it's just your sample-efficiency argument and so forth: You just can't bend the curve enough if you don't use formal verification?

Alex Davies

The thing is, the informal stuff is also available to us in a way. If you really want, you can have both an informal and formal system, and that is going to be—

Shawn Wang

I see.

Alex Davies

—a very strong system. The thing that I think—my suspicion about whether we can scale to math AGI just by the informal approaches—is that you're going to keep having LLMs judge solutions, or you'll have human experts who grade. Human experts just don't scale that well.

If you really argue infinity, then sure, you also have infinite money and you can pay infinite people. But is there really an infinite number of people who can understand and prove, say, a nontrivial result in the Langlands program? I think, good luck finding those people. In fact, I think how FrontierMath came together is because they couldn't assemble a benchmark with their expert pool, so they had to collaborate with Epoch to do it, right?

That's what I worry about with having the human part. They have LLM judges, and then now stochastic judging. The problem is that whether something is impossible to achieve versus something being incredibly expensive—really incredibly expensive—to achieve gets kind of mixed in the end.

Shawn Wang

And then, of course, investors always want to know why you. I've read a little bit about your background, and I think we'd do a disservice to the audience if we didn't hear a little bit about your personal story.

Alex Davies

I see.

Shawn Wang

Do you want to talk just a little bit about yourself? You've done some really interesting stuff, so I'd love to hear about you and then your team. What makes Axiom special?

Alex Davies

Yeah. I think Axiom is very special because we are really expert mathematicians. Basically, we're users of the system we're developing, and that iteration loop is very fast. It is extremely fast.

We have some of the strongest mathematicians in both research and Olympiad contests, and we also have people who are mathlib contributors, maintainers, and developers—Lean gurus, really. We combine them with people who come from applied ML, from really strong organizations like Meta FAIR, Google, and Nature Fair, as well as people who have code-generation expertise and work with compilers like KernelGen. Having these backgrounds together, I think that sort of interdisciplinary way of thinking about things is quite helpful.

We think AI for math has traditionally been quite interdisciplinary. People are borrowing techniques from AI for science, from the code-generation literature, and, obviously, from the broader frontier applied-ML field to try to apply them to the niche problem of AI for math. We also think having this very special team is a differentiation.

We also think that, as you say, there's no permanent moat. The proprietary data that we generate, and a little bit of a flywheel we're seeing, is a time moat.

Personally, I love math. I've been doing math since I was very young, and math sometimes gets really hard when the problems you're solving are just a little bit out of reach. It gets a bit depressing. At times, I wonder if I can just have an AI help me. And, yeah, I figure, why not build such a thing?

Shawn Wang

You did a master's at Oxford in neuroscience.

Alex Davies

Yeah.

Shawn Wang

Does that inform your thinking here?

Alex Davies

That's a great question. I think my experience with neuroscience is that you learn very well about what's hard—

Shawn Wang

Yeah.

Alex Davies

—and what's impossible. It's very interesting. I think that year of neuroscience gave me some feelings about what's hard and almost no feeling about what might work.

I was under the pretense of neuroscience, hanging out at the UCL Gatsby Unit, and was fortunate to do AI research with some really cool faculty. So, I think that was a very productive year of AI study, and not neural study.

Shawn Wang

So, it was mostly you studying AI?

Alex Davies

That's right. I think in the UK, back in the 20th century, if you called something AI, you would not get the donation, but if you called something brain science, you might have a chance.

The UCL Gatsby is a premier AI hub where a lot of people actually go from there to DeepMind, including Demis himself. It's a very wonderful research environment. I remember those tea-time talks were very amazing, and people were basically just doing AI. It's called the Gatsby Computational Neuroscience Unit.

How that happened was that I was in the master's of neuroscience program and then quickly realized that you need to kill rats, and I kind of didn't want to do that. Computational neuroscience sounded more appealing. When you look at the project and you see a transformer, you're like, “You absolutely want to do that.”

swyx

Yeah. We're all excited about that. So, after the Gatsby, you started a math PhD program at Stanford.

Alex Wei

I actually started one full-time year at the law school.

swyx

Oh.

Alex Wei

The JD-PhD program is structured in a way where you have to spend 1 full residency year. That was also a very fun year of learning things that are just quite fascinating, like criminal law and looking at homicide cases. Exciting.

swyx

Do you ever feel like the legal system is under- or overspecified in some way that maybe you could actually improve?

That's a great question. I think for a lot of things, it's definitely underspecified. For some other things, I was actually quite excited about transferring learning from mathematical reasoning to those specific fields.

I think appellate litigation—the legal gymnastics you see from really good appellate scholars and lawyers—has some people who just come from math training. Not many, but Lawrence Tribe, for one, the Harvard law professor, is one of the strongest appellate-litigation and SCOTUS-brief legal brains on the left, in the Democratic Party.

I think there are a lot of other domains, such as antitrust, that are incredibly flowcharty.

Contract law is sometimes also flowcharty. Bankruptcy and tax are more on the corporate side. I just love the litigation side.

swyx

So, actually, just because we're talking about litigation, it's not the same thing, but there was an Erdős problem that Axiom saw. I don't remember if it was AxiomProver or whatever. Is that right? There was a controversy about it because it had represented that it had solved the problem, when in fact it had discovered a proof and then just formalized it.

So, actually, what happened was our competitor, Harmonic, decided to publicize that they had solved unsolved Erdős problems, numbered 124 and 481. We trusted their literature review, believing that these problems were truly unsolved, and we were a really young company at the time. We wanted to test whether our system could attempt the problems that our competitor could. We fully did not expect to actually solve them, but it turns out that we were both wrong: in fact, the problems had been solved before.

swyx

I see. So, then—

It's not the only time that we relied on others for literature searches. We really should have done our part. The other time was this paper called “Dead Ends in Square-Free Walks.” Professor Miller had this problem that actually turned out to have been solved, but we really should have done our part. That is, you know—

swyx

The point I'm trying to elicit is not that you guys did something wrong, but rather—

You know, there's this Japanese advertisement of a whole company, with hundreds or thousands of people apologizing. It's like, “Sorry, we raised our price by 5 cents.” That's the advertisement. I was thinking that maybe I should just do that. It's so embarrassing.

swyx

No, no, but I think the question is about the provenance of information and how you connect the answer to the question. It goes back to the question I was asking before: How do I connect the answer to the question?

Yeah, this is a good question. I think after the Erdős thing, we were extremely careful. We didn't really look at the other Erdős problems. I believe that Harmonic still continued to claim that they had solved Erdős problems. That might or might not be true; I don't know. Terence Tao and a lot of other people have a database about all the Erdős problems and their status.

I think it's a really easy mistake to make because there are so many Erdős problems that have actually been solved. Search and retrieval is a hard problem. You don't know if that argument, or an equivalent version of that argument, has in fact been solved. I think the most interesting part about that entire database is that there are a lot of problems that are not directly solved, but can be solved by a very easy extension—almost a trivial extension—of another result that has been solved, or sometimes not even a result.

Sometimes I think, in this “Dead Ends in Square-Free Walks” case, which has nothing to do with Harmonic, what we actually didn't realize—and what Professor Kannan Soundararajan pointed out to us and to Professor Miller—was that it was actually from a MathOverflow post. A user had pointed out that there was a result. It's fascinating, and I think it's hard to find out. Search is a hard problem.

swyx

I guess that means that the conjecture engine, or whatever it is, uses search as part of its process. Is that something that you do as humans and then feed into it?

I think a knowledge graph or knowledge base is a very important component of any company.

swyx

Yeah.

Alex Wei

I don't think it's talked about enough.

swyx

And so, you guys have a knowledge graph. It sounds like you don't want to give us too many details, but I read somewhere that you have a really massive database of Lean proofs that you've generated, or synthetic data in some sense. The end result—and this may be a competitive advantage for you—is this massive database?

I think everyone is trying to accumulate data, which is not a moat. It's just time and time more.

swyx

Yeah.

Alex Wei

It's all about whether you can execute fast enough to make sure that you have a certain buffer because of, say, your data-set accumulation. But that is only just a buffer.

swyx

Have you ever thought about doing something like AlphaZero for math, where you start from nothing and let it just make up axioms and see what happens?

This is a wonderful question. I think that's a very interesting approach, actually. We believe in something: suppose AxiomProver can be a really strong mathematician. Then, really, the thing that it is proving every day should hopefully help it improve. This sort of self-improvement is extremely valuable.

swyx

Mhm.

Alex Wei

There are other people in the AI-for-math community whose work is very interesting. I think Professor Gabriel Pereira's work is very interesting. There are some more conjecturing-type explorations. There are specific things you can do in certain ways to try to see if your system can learn to conjecture and build theories.

swyx

I think the topic is really interesting and important because you're claiming that, to get to superintelligence, there's sort of this—it's just not going to be possible. Maybe if you had infinite resources, you could just use RL and it would work, but the reality is that you just can't be sample-efficient enough to do that. So, you need some sort of verifier in the loop with the inference process, rather than only during training, because you do have verifiers during the training process and you just don't have them during the inference process. Is that right?

Yeah, I think a lot of them are secretly trying to use this to ground their reasoning.

swyx

Yes. I would. I was surprised that, when o1 was coming and everyone knew o1 was coming but it hadn't come out, I was sure they were going to announce that they were using Lean to do formal verification of proofs and actually generate proofs and then verify them, so that they were grounding their reasoning. That was my—

When Lean was there, there was GPT-f. That was a great piece of work. There's also MiniF2F. These are all formal-math works from OpenAI.

swyx

Okay. So, presumably those guys are doing something.

No, no, they all left.

swyx

Oh, they all left. I see.

So, that's my point. If you're an intern, I guess you can't be an intern forever. Let's say you're a junior member of technical staff and you want to work on something for as long as it takes to solve it. Weirdly, people think about startups as this sort of thing where your runway can just run out and everything can just fall apart. You might have a better chance of staying focused on the same problem for as long as it takes at a startup like Axiom or one of the other new labs.

swyx

Yeah. If you're aligned to the mission of the—

Big tech.

swyx

—company, rather than somebody deciding that what you're doing is no longer—

Yeah, yeah. It can be that your VP lost some political fight. So—

swyx

Yeah.

Alex Wei

Yeah, absolutely. So—

No, obviously, if we succeed, then they're all going to start doing that again.

swyx

Yes. And then, as a talent, I guess there are more potential places to choose from as well.

Yeah. So, then your job is to go fast so that they're struggling.

swyx

Actually, we haven't talked about it, but you also just released an API for doing Lean verification.

Yeah.

swyx

I actually tried it with Claude Code because it's easier than setting up your own Lean toolchain.

Alex Wei

Yeah.

swyx

It was like trying to get Lean to prove some things. The infrastructure is maybe nontrivial, especially at scale. Do you want to talk a little bit about that?

Alex Wei

Yeah. We just released Axel, spelled A-X-L-E, which stands for Axiom Lean Engine. It's really a set of proof-validation and manipulation tools built for Lean, in the language of Lean. It's a bunch of metaprogramming tools.

Metaprogramming talent is extremely hard to find, and we're so grateful to have a really cracked team working on that. We want to release it to the community to use for free because we think there are probably other people also doing large-scale Lean operations, and these tools are going to make their work a lot more robust and faster, and allow them to do so at scale.

Axel currently has, I think, 14 such tools, starting from verified proof, which is the sort of thing that makes sure there's nothing weird going on, like no cheating by Lean code. You don't axiom something out, and you don't assume weird things. If you axiomatize M + N = N, you can prove 2 + 2 = 2, which is definitely not the right answer.

There are also a lot of other generation tools. For example, you can try different repair attempts: broken Lean in and good Lean out. There are currently other repair methods by LLMs, so hopefully what we provide can be a lot cheaper and more straightforward. I think strong and better engineering can get you to a place that's quite far.

A lot of people from the Lean community have been using Axel. It's only been a week, and they've been using it to do all sorts of different, interesting things. We've seen people from the blockchain community use it to do interesting things in Anchor. We've also heard from a lot of people that Claude plus Axel is their go-to setup for now.

We think these are really interesting tools. Famously, I think today there's a mathematician who said he formalized Donald Knuth using Claude to prove, I think, a Ramsey result, and then formalized the Lean proof, which was also using the Axel tool. So we've already gotten to see people using it.

swyx

I mean, I feel like this is a great opportunity for the collaborations that Terence Tao was talking about as well, where once people have access to the common tools, it becomes easy to do. If you have an intuition—even if you're not a strong mathematician like myself—you might be able to participate in an effort to prove a larger theorem or something like that.

Guest

Yeah, I think that's very interesting. Mathematics has not been as collaborative as software engineering. You don't have hundreds and thousands of people working on something together. I think Polymath was an instance when that happened, and that was fantastic.

If you have a really good setup and commoditized access, then people can all participate. In fact, that's how I think some of the large formalization projects have been done. Things are divided into subtasks, but really, the blueprint-writing process—say, Terence Tao and Alex Kontorovich assigning the tasks to different people and figuring out how things fit together—that blueprint-writing part is extremely important.

There has been, I think, a result about sphere packing by one of the other companies out there, and the blueprint part for the 8 dimensions is still pretty much built on what the sphere-packing community and the Lean community—the humans—blueprinted. It's similar with some of their other results as well. The blueprint part has still been human-generated, and I think auto-generated blueprints are going to be a technical bottleneck that many people are trying to solve around the same time.

swyx

So, is there value in me as a Claude Code user trying to attempt part of a small lemma or whatever, where I don't have a great understanding of the math? Maybe I have a high-level understanding.

It depends on what you're trying to formalize, or are you trying to prove?

To prove those things.

swyx

Yeah. So maybe formalization—you would obviously probably start with formalization, right? You know the proof and you just can't get it.

Yeah.

swyx

Nobody has been able to get the formalization correct.

Guest

I do actually have some people use Lean for formalization, and they try to do it by hand, not using any AI, as a way to learn mathematics. Now, it's all the formalization. You don't have that process.

It's interesting because I think a lot of my friends who started working on Lean and mathlib were in PhD programs, and the problems are really hard. We get stuck all the time, and we want to review some of the undergrad classes from a time when we still understood what the math was about. We do so by doing Lean, and I think that's very beautiful.

Yeah, but if you have, for example, access to Axiom provers that can also formalize all the formalized things, then you lose that part of the learning process.

swyx

Yeah.

Guest

Yeah, but I do think that for you and me, we can set up Axel and try to see what results we might be able to prove. I think that's quite interesting. Thanks to Axel making the speed a lot faster, you don't have to wait very long.

I remember the Putnam exam day. We were all in the war room. It was a Saturday. We were all really excited, and we had just gotten the exam paper from the official organization, the proctor of the Putnam exam. We were looking at how much work Axiom was getting through. Without it, we couldn't have solved the 8 problems within the time limit. That definitely would not have been within the time limit.

I think the one thing about these tools is that, potentially, you can have an interesting reward for RL as well.

swyx

What do you mean by that?

For example, a verified proof can be a reward for a proof being completely correct and validated.

swyx

I see.

I think formal verification tooling can be an interesting direction for scaling with RL.

swyx

Yeah, so you mean, for example, you formalize or autoformalize the informal proof and then verify it, and then use that as a reward? Or do you mean—

No, as in, you pass Lean programs into these formal tools, right? And you will have some sort of score.

swyx

Okay, yeah. I think if I were to build one or something, I would have, in my mind, used what I just described. But you're saying just to learn how to do Lean?

So, the value proposition that's interesting about frontier labs is that suppose you are a B2C business, then sure, you can just not do what we're doing. We've seen, for example, DeepSeek originally having a formal team and then later dissolving that team because of a strategic direction change. That's all completely reasonable.

Now suppose you're focused on coding, right? And you have talent who want to work on what we're doing. It makes a lot more sense for you to do code generation, furthering your strength and moat.

swyx

Yeah.

Guest

You can partner with Axiom, just like how, for example, frontier labs partner with startups that work on search, such as Exa and Parallel, right? Just call the Exa API for searching. Potentially, if you're a frontier lab, I think you should call the Axiom API for verification.

swyx

Yes.

Guest

It doesn't make sense. Potentially, I think, given the talent, the finickiness of Lean, and the sort of data and code, there's no reason to.

swyx

Yeah, I mean, it took me 5 minutes to set up.

swyx

Why did you decide to start Axiom? Like, you were a grad student at Stanford and in math. So, what made you decide to—

Yeah.

Guest

I wasn't in math for very long. I think almost as soon as I started the PhD, I just started fundraising. So it wasn't like—

swyx

Oh, really? Okay.

Yeah.

swyx

Was that the plan, or did you start there and almost immediately realize that this was—

Guest

Right. So, the year of law school was very, very interesting to me on an intellectual level. But it was also the first year where I had no science, technology, or math whatsoever in my life. It was a weird year. I was reading a lot. I was practicing—well, I was learning how to write and learning how to read.

I just wanted to be obsessed about something in technology. That was also what was going on that year. So, yeah, the year of law school was very interesting to me because I thought, “Okay, I just need to be obsessed with a technical thing, because otherwise I get bored.”

I don't think I'm bored because I really love everything about law. I really loved it. It was something incredibly interesting to study. But I've basically been very excited about the progress of reasoning. I was looking at a lot of the post-training papers, and I was learning all of this just by myself.

At one point, it got to the point where I thought, “I think this is for sure happening.” Talking to Shubha at Verve every weekend also didn't help soothe these thoughts, so I got more and more obsessed. At a point, I thought, “Okay, if I'm doing this literally every minute and I can't think about something else, I need to do something about it.”

I fell madly in love with the idea that AI was going to do math. And I thought, “Okay, now do I do math?” It was really crazy at the time. I remember I just couldn't get out of it.

Then I went to a Knight-Hennessy event. Knight-Hennessy Scholars Dining House hosts all sorts of free-lunch events, and those are great because you get free food and interesting intellectual exposure to things.

I remember Julie Zhuo, who was, I think, Facebook's first PM, came to speak. After that, I basically walked up to her and said, “What do you do if you want to do a startup and you really want to do academia because you kind of love math?”

She said, “Well, what's your time spent on these 2 different things?” I said, “100%, 0%.” Then she said, “Well, you kind of have to follow your energy.”

swyx

Yeah, I mean, if you're completely obsessed with it.

Yeah, I was completely obsessed with it. I thought, “This is going to be big.” I thought it just had to be a for-profit startup because it’s so much broader than making mathematical breakthroughs. If you think about recursive self-improvement and the more high-level concept that you really want to have just AI scientists, math reasoning is going to be a pretty big part of it.

I think the belief by Cursor and Claude and other folks is that math transfers to code, and coding transfers to math as well. I think that’s true. It’s just that, why not push it directly? I don’t get it. You need to push that directly.

Then there’s this other thought, maybe going back to the collaboration point. Verification has traditionally been thought of as something for industries where there are a lot of guardrails. If you’re working in defense or military use, you need to satisfy a lot of barriers to entry and meet stringent requirements. So verification has been thought of as being for industries that are closed.

But for the first time, I think verified AI is about opening up collaboration. Either it’s human-AI collaboration, or, before AI, that was human-human collaboration, with Lean as the grounding—the formal verification language. And then there’s human-AI collaboration, as we’re seeing now, and future AI-agent collaboration.

I think verified AI is for openness. It’s not for meeting the requirements of closed industries. I remember there was an article about chatbots making things up and whether math is a solution to hallucination. Verification, to me, is not about lossiness. Verification, to me, is about scaling brilliance and compounding brilliance.

Just 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 his brilliance, both scaling up and scaling out. Verification is more rigorous, but verification, to me, is not about erasing mistakes or lossiness. It’s about scaling brilliance.

The third point is that verification, to me, is not just about rigor. It’s actually about performance gains. It’s not just about the stringent requirements and the hurdles that you need to overcome. It’s about actual verified generation making things so much better.

A lot of people think you work on verification because of your distrust of technology. That sells really well to the general public, including my parents: “Why are we doing verification? Because technology makes mistakes.” No, we don’t think verification is based on distrust of technology. It’s because the expected rapid exponential scale-up, deployment, creation of technology, and technological progress compel and demand it.

swyx

It’s a very mathematical perspective, right? You’re saying proofs drive math. A lot of math is based on proofs, and math drives a lot of science and innovation in the world. Innovations in math drive innovation in the world.

But it doesn’t even need to go through that. In terms of “solve math, solve everything,” that obviously stands. My point is that transfer learning doesn’t—transfer learning is about closing the gap in math reasoning.

So there are, I guess, a couple of narratives here. For some people, you solve math, and then math is the fundamental layer of the sciences. So that’s the “AI for math, then take the theoretical layer of AI for science” narrative. We actually believe in general transfer learning. I think Axiom is on the infrastructure stack.

swyx

And you think this is just a first step to basically unlocking capabilities in many domains in science and law, for example?

Yes. So, again, there are multiple beliefs. One belief is that there is math, and there is the power of formal verification. Suppose we actually solve math and have a really strong informal math-reasoning engine. We do not expect that to be as large as solving math through the formal way.

swyx

Why?

I mean, code is a language, but it is indeed on the more structured end.

swyx

Yes.

Guest

It bridges informal and formal.

swyx

Yes.

Guest

What we’re doing is not informal versus formal, and we’re not taking the completely formal-proof approach. It’s bridging between informal and formal. It’s bridging between high-level and low-level. It’s a direct improvement through reasoning and transfer learning, and it’s also indirect in that math is going to unlock a lot of science.

swyx

So you think that it enables transfer learning?

Yeah.

swyx

I see.

Guest

I think that is pretty much a consensus. I think it’s a consensus, and this is the bet that has been pretty much overlooked by others because math sounds pure and it doesn’t sound like there’s any commercial value.

swyx

Mhm.

Guest

I obviously understand the opportunity cost if you’re a frontier lab solving this problem. But I definitely think it’s a problem that, if you’re a well-resourced startup, you should be doing.

swyx

That’s an interesting perspective. Did you get everything out that you wanted to say?

I think the question is whether Axiom is math versus Axiom is verification. The DNA of the company is math, so we think verification is the best first market. We think that solving math, and especially formal math, is going to help us tackle the really ambitious quest of verified AI.

When we’re done with that, we might have another, a second market, including AI for science, which we just talked about. On the theoretical layer, I think real-world testing is important, and potentially we can stay in the digital world and do software stuff. For other things, you need to get rewards, like physical rewards or signals.

swyx

But do you think that the capability of doing really powerful reasoning—

Same.

swyx

Once you have that powerful verified reasoning engine, is that the moment when we’ve unlocked software verification, hardware, or whatever? But now, what about biology? What about chemistry?

Guest

That would be one. The other one is really, how far are you from recursive self-improvement?

swyx

Okay, so just AGI.

Yeah. I think there’s this question, and different people, because of their different backgrounds, have different answers. It’s really where your energy and your passion lead you.

For some people, I’ve heard this from my friends, they want to work on AGI because they believe solving AGI solves death. There are other people who come from more of a medicine background. They really believe they can solve death, and they don’t solve AGI and then solve death; they just solve AI for science.

swyx

Yeah.

Guest

Now, which way is correct? I don’t know.

swyx

The recursive self-improvement angle sounds to me like you’re saying that the combination of verification plus language, which is informal, enables really good recursive self-improvement.

Recursive self-improvement is going to happen anyway. We’re trying to have formal verification earn its place. Whether formal verification can be welcomed, deployed, and become a consensus depends on how well we execute.

When you boil that problem down into an execution problem, you should just go for it.

swyx

Looking forward, what’s the biggest bottleneck that you see in the field, both for Axiom and maybe for the field broadly?

Fragmentation. I think we’re in a market where, instead of 1,000 people joining forces, people start 1,000 things. I think that’s the biggest bubble indicator.

There are category bubbles, and there are other categories where there are moonshots. It’s not a bubble; it just looks a little bubbly. In a field, if people with really legitimate backgrounds decide to join forces and work as a team for the mission rather than for ego or status as a new founder, I think that category is something I’m really bullish on. Other than that, and vice versa.

I think the bottleneck is potentially that we’re in a—if you believe we’re in an age of research, if you believe deep tech is the interesting direction to pursue—the current market conditions are good and bad. They’re good because they enable these long-term, long-horizon bets to be funded, and bad because there’s too much noise in the market and there are some irrational players.

We try to work with really incredible venture firms. They are the partners, they are our intellectual partners, and there's a lot of alignment. We bounce very cool ideas, technical and non-technical, off each other for long hours, and we spend a lot of time outside of work and on weekends together to really intensely build the company.

But there are also other people who just want to park capital somewhere. While we don't work with them, these are market conditions that encourage fragmentation. When things get fragmented, no one gets there. I think every category, regardless of how right the idea is, is pretty much in a sort of “earning the right to exist” stage.

If that is the case, then, for example, take a great deep tech company like SpaceX: people do actually join forces to work on that dream. Potentially, in that case, you also have a very charismatic founder. I think a really concerning thing for me personally is that, for some other categories that I'm personally quite bullish about, just looking at things generally, fragmentation is a problem. We see startups pulling professors from universities to work on something, and it really is a really interesting kind of situation.

swyx

Maybe this is a naive question, but right now, when you were talking about players in, let's say, AI for math, where you have Harmonic—

Yeah.

swyx

—and then the big labs, right? Am I missing someone? Is that actually fragmented?

Guest

I guess fragmentation, I think, is a bottleneck for the entire AI landscape.

swyx

Okay. Yeah.

Guest

I think AI for math is a category that is actually not a bubble because it is not fragmented. People who are really amazing talents do like to join forces. For example, the fact that we got Kevin O'Nolan and François Charton on the team, this is fantastic. You have someone who's a core contributor from Lean Mathlib and some really great benchmarks, and François, who's on AI for Math discovery and proving. They work together.

Then you are suddenly a player with both proving capability and construction capability, and that's fantastic. I believe, as you said, Harmonic probably also has some really great talents joining forces together. I think AI for math is a good category because of the absence of fragmentation.

But even from our perspective, for example, RL, right? I don't think that's a category per se, but RL talent currently is quite hard to attract and retain, literally for everyone. There are a lot of companies being started and then sold 3 months later. Each month where you could have worked on a technical problem and you're instead working on deals is a month that is wasted.

I say that also with some amount of pain and suffering, as I've gone through 2 fundraisers.

swyx

Yes. [laughter] Yes, yes.

Yeah.

swyx

So what's the biggest bottleneck in AI for math?

Guest

For Axiom, or for AI for math?

swyx

Not Axiom, but just the community.

But the community of AI for math.

swyx

Where is it going? What is the thing that everyone just really wants to break?

I expect fragmentation to start to happen as Axiom and Harmonic establish category leadership.

swyx

Mhm.

Guest

I expect people to kind of— that's one thing. But I also think that another bottleneck could be the pressure of short-term versus long-term. We are doing things in a very fast-paced manner, but that does not mean it is always correct to do things in the most fast-paced manner.

We do things in a fast-paced manner because we were founded on the day of the International Mathematical Olympiad, so we couldn't have competed in that anyway. The next math Olympiad is Putnam, and we're quite excited because it's an undergraduate exam. This year's 2025 IMO was easy on the Mohs scale, and Putnam could be hard. In fact, it was harder than the IMO on the Mohs scale if you look at how many scores the AI has attained on average and at the maximum difficulty of the problem. Putnam is harder on both axes.

We want to try, and there's only a gap of 4 months, but it doesn't mean I'm always going to set 4-month goals. If I build a company only setting 4-month goals, I might build a really short-sighted company. I see longer-horizon problems.

For example, market forces could force other players into proof verification. It is possible that formal verification is a holy grail. It's possible that if you solve that, then you also naturally solve proof verification, with some amount of epsilon caveat around distribution shift. I strongly believe that a bottleneck could be that pressure.

I think Axiom is fortunate that we're early enough that we are a team of incredibly high-agency people, and our execution generally surpasses expectations. But I think what could be a bottleneck for the entire AI for math field is that potentially trying to prove commercial value is going to distract significantly from core capability improvement.

Shawn Wang

Yeah. That makes sense. Cool. Thank you for driving up and coming to see us.

Guest

Thank you so much. Yeah.

Shawn Wang

I know the traffic was horrible.

Guest

Yeah. Thank you.

Shawn Wang

It's been a real pleasure speaking with you, and we look forward to seeing how things develop.

Guest

Yeah. Thank you so much.

Shawn Wang

Thank you. Awesome. Thank you. Yeah. Okay.