她筹集6400万美元，打造AI数学神童｜Axiom CEO Carina Hong

Axiom’s mission is to build a reasoning engine that is self-improving and combines generation and verification.

For Putnam, for people who aren’t math nerds, it’s like a contest among math undergraduates that’s incredibly hard. The median score is like a zero.

We recently, at Axiom, got 8 out of 12. We use formal languages like Lean to ground the natural-language counterpart, and because we’re doing that, we witness the power of deterministic tooling and probabilistic systems working together.

You were on an academic path, and now you’re running this company. What made you decide to shift gears like this?

When I was 5, I would listen to underground rock-and-roll music. It was obviously very politically rebellious, and I liked the contrarian appeal. I do think that this startup is really fun, in that it’s such a brand-new adventure, and you’re a bit living like the rock-and-roll days every day.

What do you really predict for mathematics going forward?

Mathematicians will learn to work on a different abstraction than they’re used to before. If you’re a great mathematician, just let your intuition take you wherever you want, and have the AI mathematician be the diligent graduate student trying to prove the intuitions you have.

1. Introduction

You’re listening to Gradient Descent, a show about making machine learning work in the real world, and I’m your host, Lukas Biewald. Carina Hong is the CEO and founder of Axiom Math, which is a company that calls itself a self-reasoning system and is currently on the cutting edge of building an AI mathematician. They’ve had astonishingly strong results on math olympiad problems and recently got the highest score on the Putnam test, which we talk about. Carina is super interesting. She was a star academic mathematician now turned into a founder. Axiom Math came out of stealth having raised $64 million. She talks in detail about how Axiom works, how she thinks it applies to more than math over time, and also how rock and roll or hardcore rock and roll music in China influenced her thinking around management and staying hungry. I hope you enjoy this interview.

2. Understanding Axiom's Reasoning Engine

Carina, why don’t we start with the most basic question: What is Axiom, and how does it work at a high level?

Axiom’s mission is to build a reasoning engine that is self-improving and combines generation and verification, which we think is an overlooked component in the current AI landscape. We want to start with an AI mathematician because math is a really good testing ground for this sort of self-improving loop. We use formal languages like Lean to ground the natural-language counterpart, and because we’re doing that, there are a lot of interesting capabilities we can unlock with much higher sample efficiency.

The general vision of Axiom is that there is a prover—a system that can prove theorems—and also a conjecturer, a system that can propose interesting conjectures. They talk to each other. You have this third component called the knowledge base.

If I’m a prover, I’d like to know what’s already been proven and what I can use. If I’m a conjecturer, I’d also like to stress-test whether a conjecture is reasonable. Perhaps a counterexample will help me by ensuring that I don’t suggest that conjecture at all. The knowledge base is a very important component supporting these two, and then autoformalization—the system that can automatically formalize natural-language material into formal-language material—is kind of weaving all 3 together. That’s the basic setup of Axiom.

Can we break it down in the context of something simple that everyone could understand? If we were going to try to prove the Pythagorean theorem, for example, assuming it’s not in your knowledge base, how would that work practically?

If it’s the Pythagorean theorem, which is already proven—hopefully, I think—

Millions of times.

Let’s just do it. But if we do a de novo math problem, we recently got a really strong, winning score on the 2026 Putnam exam. Because it’s in December, they name it by the next year.

So you beat them?

Within the exam time limit, we got 8 out of 12. We’re going to announce our actual final score, but we also announced 9 out of 12 because I think the ninth problem came 2 hours after my tweet, which is a little awkward. So you’re like, “Oh, wait a second, everyone. Don’t repost that tweet; repost this one.”

That’s nice. Breaking news here on this podcast.

Yeah. Nine out of 12 was Nayoto’s score—the number-one score last year among all 4,000 human participants. It’s a Putnam Fellow, which is a top honor—top 5 every year, almost every year consistently, beyond some years where the problem somehow got really easy.

We’re going to announce the final proof release, and we’ll say exactly how many we solved. I think that’s very exciting. We witness the power of deterministic tooling and probabilistic systems working together, and I love the capabilities that result from that.

For Putnam, for people who aren’t math nerds, it’s a contest among math undergraduates that’s incredibly hard. I think the median score is like a zero, and the best math undergraduates are doing it. Getting any of the problems right is a real accomplishment, and beating everyone is kind of amazing. All the best mathematicians did super well in this, so tell me if that’s a good description.

Yeah, that’s right. I personally got a much worse score than our prover system, so it’s a very interesting thing, I think.

What did you get? Let’s brag a little bit. What did you get?

3. Human vs AI in Mathematical Problem Solving

I got 4 out of 12, which isn’t that great. I only got a top-250 honorable mention, but Axiom’s final score will potentially triple me. I think we should have a “Beat Carina” kind of party, which is always fun.

I’ve noticed that using LLMs—say, GPT or Gemini—directly, without your technology, they seem surprisingly good at math-olympiad questions. Maybe not the hardest ones, but the scores are like, “Wow, this is pretty impressive.”

I have a mutual friend, Robert Nishihara, who’s given me a bunch of different brainteaser questions. One of them was a pretty simple, fun question. I put it into GPT and Gemini, and they actually couldn’t solve it.

Oh, interesting.

To me, math olympiad is so much harder than the kinds of questions you might get in a Google interview, but it seems like maybe, for LLMs, they don’t have the same hierarchy of difficulty. Do you have an intuition for what’s easy and what’s hard for them? Is your system similar? Would you find that maybe some things that might feel more trivial to a junior mathematician are hard for your system?

I think it’s fascinating to think about LLMs doing things like math and, sometimes, in safety-critical domains, code. In some cases, like high-stakes scenarios, writing code statistically just doesn’t work in the way you want. You want to make sure that you have provable guarantees on edge cases. This is similar to saying in math that a proof is a proof: It must be sound and not have any critical flaw.

That’s why informal scaling of informal models to math AI just isn’t something we believe in. As to different math questions, it’s easy to make a case for those that require very fine-grained checking. Those things, I think, Lean will be very good at. For things that rely on high-level intuitions and probably don’t have the sort of detailed parts, I think the reasoner—the informal model—will probably make a pretty good contribution.

When it comes to computations, certain tools are probably helpful, like mathematical software and plugins. It’s very interesting to see, for example, a simple positivity argument in analysis.

We’re actually planning to do a Putnam proof release and commentary, so that we’re looking at each problem, how the AI solved it, and whether that’s expected given how a human might think about it. In the analysis problems, you can see the AI doing a lot of work for something that a human student or researcher would just write off. It will do chunks of code to rigorously ensure that things around convergence and limits are very carefully handled.

That’s actually why, in the initial days of Mathlib, funny enough, undergraduate algebra texts were all formalized rather straightforwardly and quickly, and it took them a long time to do the analysis. Analysis and algebra are usually the 2 subjects at the undergraduate level. I actually found the graph that I would like to show.

Okay. Basically, what I'm talking about is that this is not a Putnam problem. This is an Erdős problem 481. A Twitter user—I think an undergraduate math student—solved this problem by himself, got very excited about it, and posted about it. We were trying to see whether our system could solve it as well, just as a sort of Twitter daily-engagement thing.

This is what the system does: It breaks the problem down into different subgoals, results, or lemmas. It starts with this one not being green and continues until everything is green at the very end. When every other node is green, this node will turn green.

Can you turn that into something interpretable by a human?

Yes, I think you can. In fact, for each node, you can click into it and see the Lean code. Auto-informalization, which is converting Lean back into natural language, is significantly easier than the other way around. I think that's because models have seen a lot of English, but not a lot of Lean; in translation, one direction is significantly easier when translating from English into another very niche language.

So, yes, you can poke into it. I think that would be very exciting for someone to interact with the system while it's doing the proving work.

Cool. I wanted to ask: One of the things I noticed with code generation is that LLMs today are better at generating code that works than at generating code that feels easily interpretable by a human. That totally makes sense with the reinforcement learning that they're surely using, and I would think you might have a similar issue, where generating Lean that proves something to be true is probably easier to check than whether a human could understand it.

4. Future of Mathematics with AI

I would think your models would probably generate things in different ways than humans, and I feel like some of the more technical math proofs are already really hard to process. Do you think we're entering a world where models might prove the Riemann hypothesis, but no one understands? Everyone might agree with every step, but no one can actually get an intuition for what happened?

Right, right. I think it's a fascinating question because if, say, a human proved the Riemann hypothesis, in certain cases—I remember when Yitang Zhang, a professor, announced that he had proved a math result. I think they very quickly assembled an expert panel. I was at Oxford at the time, so some of the professors I was interfacing with were telling us how they got together to try to examine the proof. Because certain mathematicians write in a way that is very obscure, the experts couldn't immediately understand what was going on either.

I would start with that. I do think that Lean proofs, which have this sort of verifiability feature, are really good news. If you imagine that GPT one day produces a 10,000-line Lean proof claiming that it has solved an open conjecture, especially because it's trained on chain-of-thought data, among other things, we really can't be sure.

I think that scenario happened in December 2024, around the 2025 Putnam. I remember Dan Hendrycks posted on Twitter, saying, “Hey, I fed these problems into—I think it was o1 Pro or o3 Pro, I forget. I forget. And then o3 Preview.” People were giving those model outputs widely different grades, and no one in the Twitter commentary area was able to say for sure whether they were correct solutions.

The consensus was something like, “No, they're not correct,” because for all these problems there was a significant hole that the model tried to hand-wave. The power of formal systems is that you cannot hand-wave. In fact, it's doing a little bit too much of the opposite: It's almost annoying that it's rigorously checking every fine-grained detail, like convergence and limits. I'm like, you really don't need to spend that much space proving the simple positivity lemma, but it does, and it's actually one of the heaviest nodes in the proof graph that we produce.

So you have at least some peace of mind when it comes to correctness. As for elegance and intuition, I do think that, first of all, for a lot of the problems, it is very hard for humans, given our intellectual ceiling, to produce 2 proofs. If someone tells me, “Hey, I have 2 proofs for the Riemann hypothesis,” that's a much more unlikely statement than, say, “I have 1 proof of the Riemann hypothesis.” There are certain problems where you just feel like there is bound to be 1 proof.

That would probably mean that what the AI finds—minus the part where it might be doing redundant things, like repeating the same thing again and again—could converge to what a human would possibly find. You can call the redundant parts ugly, but if you take those out and streamline the proof, there's a good case to be made that it might converge to what a human would find. I think that's extremely exciting.

You can treat AI not as some sort of second-class citizen, but as just another mathematician collaborator—maybe one you have not heard of. It's similar to the Ramanujan case, where Hardy and Littlewood at Cambridge discovered this self-taught genius from India. I do think that's a very interesting mindset for thinking about an AI mathematician.

Speaking of this, I also found another proof tree. I'm sharing the host screen again. This is how the system is proving problem A1, and there are problems—this is a really complicated one, obviously, and it's proving it this fast. We kind of have time acceleration. If I don't refresh it, it kind of—yeah. This is what it's doing.

I don't know how to show this more easily. Could we look at one of the questions, just so people can see what that looks like?

Yeah, I think I can. A3 is a problem that people can definitely understand. It's a game problem where Alice and Bob—the standard Alice-and-Bob setup—play a game on a string of n numbers, each of which can only be 0, 1, or 2. In the beginning, everything is 0; that's the start state. At each move, a player can either add or subtract 1 from one digit to create a new string that has not appeared before. If you cannot do that—if you've run out of all the possible strings—then the other player wins, and Alice always goes first. Which player has a winning strategy?

That's a standard sort of game-theory problem in competition math. A lot of students, when they look at it, will probably have 2 or 3 widely used results in competition math to attack it. For example, in a game with no ties, you're guaranteed, I think, a winning strategy. Then it's just asking which player has it.

Students will try to write down the string and imagine they are Alice or Bob, to see how they would attack the game and whether they can find a pattern. This is really the part about intuition discovery: If I'm Alice or Bob, what would I do? People solving the problem will try to figure out whether certain states are a lot worse than others. If I'm faced with a string and I have a 0 in one position, I can't subtract; I can only add. If I have a 2, I can't add, so potentially a 1 in a position will give me a lot more flexibility. Then I try to generalize these really bad or really good states to determine the sequence of moves, or what the rational move for the opponent is when I put them in that situation.

I think these are very interesting—it's a very fun problem. There are obviously more tedious problems: If you look at A2 and B2, there's a lot of calculus involved. Putnam is the hardest undergraduate-level exam, unlike the IMO, which is at the high-school level, and calculus is tested. For people who are very proficient with integration, I don't think A2 or B2 would pose any significant challenge. For the AI prover, I don't think it's challenging at all, but it does take a lot of lines of Lean code to solve some of the issues that we take as given. In some cases, we have the AI proving something very different—a very different sort of solution—from what our human mathematician experts expect, which is the most fun to watch.

Well, let's talk about A3, because that's a great one, right? It's so easy to understand. Where my brain goes is, okay, let me try one. It looks like all you can do is add 1, so Alice adds 1. Now you get 1. Obviously, Bob can't subtract 1, so Bob adds 1. Okay, so player 2 wins, I guess, right? Is that—so is that accurate?

Actually, first of all, sorry.

So you say the first player can add 1 to get 1, and then Bob goes and adds 1 and gets 2. I think that's right. So actually, Bob always wins.

Yeah. There's a very clean winning strategy for Bob that can be described succinctly. Once you see it, Bob doesn't need to respond with much care to Alice's moves at all, which is what makes this problem slightly easier than, I would say, a last Putnam problem level. So it's only A3.

There are 6 problems for each session. Usually, we'll expect 4, 5, and 6 to be harder than 1, 2, and 3, I would say. Basically, Bob can just execute that strategy without thinking much. That makes it much more tractable for Lean as well. There's very little state to track, and there's no complicated branching to reason about.

But I guess—it's always dangerous to introspect your own brain here—but I think the human approach is to think about cases, to look for a strategy that makes sense, not a formal mathematical proof. Do you think that Axiom is actually taking a different approach than a human approach?

You mean for this problem—for the specific A3 problem?

Yeah.

For this specific A3 problem, I would say that how the AI thinks about this problem and how humans think about it are kind of aligned. There are other scenarios where we can see the AI taking a different path from humans, because it knows that it can brute-force its way through things, whereas a human, if you're an actual task-taker and you want to avoid brute force, might not do that.

For example, if I'm doing a Euclidean geometry problem and have no idea how to solve it, but I know that brute force—say, the complex-coordinate method—can definitely get me there, I'm probably willing to sink 1 hour into brute-forcing it, but not necessarily for some of the non-geometry cases. I think a human will find a clever, sort of 1-diagram proof.

5. Applications and Future Milestones

So it's a good segue. I want to ask you about the applications of this: What are the milestones along the way? My former CRO is on your board and is one of your investors. I'm curious how you pitched this math LLM.

Yeah. I think people saw it themselves as well. This is something that I find really amazing: when I'm talking to investors, there are real intellectual alignments with certain funds. I think funds even have internal memos just marking that this category is not even a category where it's good to battle. It's something that they consider inevitable for the future.

If you think about the lack of verification in hardware and software, design teams are 1/3 or 1/4 the size of verification teams. Verification could take, as I said, 3 years in the hardware scenario. In software, for example, before we had a lot of programmers who are AI-native programmers using various sorts of coding models like Cursor, there's a lot of need for code review and in safety-critical cases.

I do think that enterprise customers are facing this really unfortunate choice between, “Hey, I just want this not to be wrong, so I might just have a human eyeball it or manually do it,” instead of relying on AI to do it. But that's also very painful for the reasons we described: the time, the resources, and the inaccessibility of certain experts.

I think the difference between a high-expertise formal verification expert in chips and a medium-expertise one is significant. If you can somehow make it the case that the AI can handle the very notorious cases, and so lower the bar for hiring, I think that would also be incredibly valuable. For example, I see that AWS, which has one of the best automated reasoning teams, took 5 years to formalize the memory-isolation component of the hypervisor by hand. That's a shocking number. It's not the entire hypervisor; it's 1 part.

6. Code Migration and Database Consistency

I think also, with more vibe coding and more agents generating code, verifying that the edge cases are covered is going to be very important. Another use case is code migration. If you have legacy code and you want to make sure that, hey, this new code—I want to upgrade it—is completely equivalent to my legacy code, it's not doing better and it's not doing worse, because that legacy code is serving important business functions.

That's another very interesting use case. In the database scenario, if there are bad actors, then proving that it is actually consistent is another one. Currently, databases are sharded from each other, and they are inconsistent in that sense because they have this problem where there might be a bad actor. All of these can be areas where formal verification can provide a very interesting solution, too.

Yeah, I mean, I guess the domains I'm more familiar with in software have test cases that are not quite as black-and-white as with formal proof, and it might be kind of overconstrained. I think the real challenge would be formalizing what it means to be wrong clearly enough that you could actually—

Yeah, I do think it's very interesting. In the database case specifically, I think having some sort of abstraction that's easy to interface with will be a big unlock. Basically, what I think is going on is that there are certain use cases where this is a dire need—we really need to verify everything, maybe because regulation mandates it, maybe because I just can't put that into deployment. Currently, we're having humans do it to make sure that, to the best extent possible, everything is sound.

Then there are good-to-have cases that it's really good to have, say, in the database case. I think if we don't have it, maybe we can live without it, but obviously having it is a weighing of how painful it is to use versus how much capability it will unlock when I use it. I think all of these are interesting trade-offs.

Then there's this final group of maybe vibe coding, like a Lovable website, that wouldn't necessarily need formal verification. I don't think the AI mathematician we're building can write poetry. I think there's this sort of 3-tier thing, and our goal is obviously to start from the first tier and eventually take on the second.

By the time we take on the second group, it will be a big moment in the broader landscape of AI, much beyond math. If you think about, for example, in the first case, an example is a proof of the consistency of the Paxos protocol, written by, say, Leslie Lamport. Then you can automatically formalize that proof in Lean, and, as part of this formalization, the system can generate code in a strongly typed language like Rust to execute this protocol.

This sort of unifying of generation—as in, what is the implementation—and verification in one is going to be a powerful idea. One question you might ask is how much can I migrate that—not migrate necessarily, but extend that—from Rust to some weakly typed languages, and slowly close the gap, knowing that it's not possible to formally verify all code in Python, but you can do a majority of it. Which programming language will be people's choice is also by itself an uncertain question.

7. Auto Formalization and Its Challenges

Then, talking about the 3 verification use cases, I think that in the 1980s, for example, a lot of tech companies tried to do formal verification with humans who were very good at writing in proof languages, in a much more ancient counterpart of Lean. Back then, it didn't quite scale because humans are a bottleneck factor. Perhaps AI formal verification can have a huge comeback here at Axiom, starting with an AI mathematician.

Yeah, it's funny. It feels very old-fashioned in a way, right? I remember that in the 1990s there was a lot of enthusiasm around formal proving and AI, and you don't hear about it much in the last few decades. It's kind of interesting.

I imagine pulling things from the 1980s and 1990s in terms of searching over theorems and trying to build proofs. I think there is a lot more modern research as well, specifically on reasoning models, code-generation ability having greatly improved, applying RL in a verifiable domain, and Lean becoming a widely celebrated language, with more developers than ever excited about it and mathematicians willing to embrace it.

I think all these 3 things coming together make this a really good time. In the software and hardware verification landscape, in software, for example, there’s CSLib, which is under development. Stanford’s Automated Reasoning Group, led by Professor Clark Barrett, is doing it with support from industry partners such as DeepMind and AWS. They’re trying to formalize all the undergraduate computer science literature in Lean. There are also people trying to formalize machine learning in Lean. It’s a very interesting moment that we’re living through.

Going back to databases, I’m curious about your thoughts. For example, I think all databases have to solve the Byzantine Generals Problem. The consistency of those solutions needs to be formally proven. I don’t know if something like that is of interest, but I’m actually quite curious about that myself.

Well, I always wonder—I feel like I’m also not a database expert, but it does make me think. There was a time when the big application of databases was more in financial services, and people really focused on making sure that things were completely consistent and that you could have real invariants. Then I think what I’ve seen in my life is this explosion of interest in NoSQL, and databases sort of relaxed these consistency constraints because they wanted to operate more efficiently, save all user data, and be able to query it.

There are these other competing priorities that I think are different from formal consistency. It seems like the majority of applications for databases maybe didn’t need that level of formal consistency. I feel there will always be applications where you want to be incredibly careful, but there do seem to always be trade-offs. In certain applications, you need to be very careful about consistency.

I agree. I agree. I agree. I think the interesting response to that is that you almost don’t have to give up efficiency because of the strong reasoning component in the system, so it will be very different, I think.

Again, the reasoning-improver framework—for example, the older AlphaProof system, which, by the way, won the IMO—that, to me, was the IMO moment, to be honest, with a score of 28, a silver medal, and 29 being the gold cutoff. But they got every single question but the combinatorics one, which is the same as the 2025 IMO, where a lot of the contestants got 35, missing the one combinatorics problem. The difference between the 2 years is that in 2024 there were 2 combinatorics questions, and in 2025 there was 1. In the AlphaProof system, it’s a formal system, so we see that trade-off: if you have only an informal system, it cannot formally prove things. I think combining these 2 is going to be game-changing, even from the customer’s perspective, because of the natural-language part. You don’t actually need to painstakingly, as a customer, spell out exactly what you want.

I think part of the goal of autoformalization is figuring out what the system does when it faces ambiguity. It would not be very fun if, like Deep Research—I use that a lot—or even some agents like Manus, it asked me for my preference on this or that every time. That’s good when it’s interactive feedback, but once that list gets to 500 items, I’ll obviously lose patience. What to do when facing ambiguity is a very important part of autoformalization.

Most people think about autoformalization as a data-generation method, but for us it’s a core technology. We think of autoformalization as potentially harder than proving—a similar problem to proving. It’s a core technology, and they can’t really be separated. For us, the difficulty of autoformalization is always the statement. If you want to autoformalize a proof, you have the Lean checker as a signal, and that’s fine. But formalizing the statement correctly is going to be challenging because, by definition, you don’t have the solution to prove yet.

It’s very good in the code-verification setting to try to autoformalize because you have test cases of input-output pairs as a proxy to ground your formal specification. I think this sort of spec-based programming, and a similar product like Kani from AWS, is just very valuable and visionary thinking.

I’m a little bit out of my depth here, but isn’t there a halting problem that sort of limits where this can possibly go? Just because you have cases doesn’t mean you’ll know.

You cannot verify all code in Python. That’s not possible. But you can do it for the majority of it. You can do things that make people’s lives easier with the capability you have. I think I said that important qualification about 10 minutes ago: you cannot do all code, but you can do quite a lot.

8. Commercialization and Intellectual Alignment

Cool. Are you already working on commercialization of your technology, or are you still in the research phase?

We’re actually a 6-month-old company now. We thought the R&D stage would take a long time, and I still think today that we’re only at day 0. There’s so much to do, but that doesn’t mean we aren’t in active conversations with some trusted partners about what this technology could solve for them.

Through these conversations, first of all, it’s intellectually expanding, and it’s really great to feel, similar to my seed-round fundraising process, that there’s real intellectual alignment with the people you’re talking to. Everyone feels a bit like a secret keeper. It’s like we see something that the world doesn’t see yet. That feeling, when you’re talking to the right people, is exhilarating. We’re obviously having some early conversations on that front.

What do you really predict for mathematics going forward? Of course, it’s nice to say that this is a helpful friend and collaborator, but this is going to get better and better. I imagine that, in some amount of time, all new proofs will be generated in this manner. Do you think academic mathematics continues?

I think mathematics will continue. I think mathematicians will learn to work at a different level of abstraction than they were used to before. I think the change of abstraction is going to have less resistance than people think it will.

Let’s take an example. Back then, before LaTeX, you had a typewriter. You’d have a secretary typeset your math paper. After LaTeX came out, mathematicians welcomed it and used it as a really good tool. Having computers help with some part of mathematical research is not new, either. Computer algebra systems have been aiding a lot of the more computational work.

We find that this will probably free mathematicians who have already developed very good intuitions from the manual labor needed to painstakingly check every technical lemma. If you’re someone like Terence Tao, a really great mathematician, just let your intuition take you wherever you want, and have the AI mathematician be the diligent graduate student or postdoc trying to prove the intuitions you have.

I think one very important part is that a lot of the AI-for-math efforts overlook the construction part. Proving and construction, to me, are very important parts of mathematical research. Constructing interesting examples is a pre-conjecturing step. As we said, write down a few sequences and see whether they give you ideas about the right lemma to formulate next. Or construct counterexamples to say, “Hey, just don’t go in that direction. It’s insane; the sanity check doesn’t pass.”

I think that will rely not on the formal proving we talked about, but on mathematical discovery—on being able to generate interesting patterns. We haven’t quite touched on that part, and I think it will be a really interesting loop. There’s, say, a conjecture led by the intuition of a mathematician, and then you have the AI prover prove it. Then you generate more conjectures, one way or another. Through formal conjecturing, or even through an end-to-end approach in mathematical discovery, you discover more conjectures and prove them, and then you start having this sort of loop. Mathematicians can be good guardians of the intuitions guiding every step of the loop.

Sure. But I guess it doesn’t take much imagination to also imagine that the system you’re building could have better intuitions than mathematicians about what to try and even what’s interesting to humans, which is kind of funny.

Different intuitions. I think the interesting thing is that it will probably be more a case where the “we are doomed” narrative comes from thinking that what’s difficult and easy for machines is the same as what’s difficult and easy for humans.

That's not the case, right? We think that the reasoner is learning a lot from humans as well. But I do think that there is a sort of top 0.00001% of mathematicians who are intellectual powerhouses. I think for an AI to catch up to that takes a long time.

Interesting, because you think there's a bigger gap between Terence Tao and an average academic mathematician than between someone with a math undergrad degree and the average academic mathematician?

I would think so. But I also think that even when we talk about the Terence Taos, there are many styles of mathematicians. There are mathematicians who are theory builders. They are not the best problem solvers, but they are able to open up completely new fields by connecting the dots between things that are deep in the theory literature.

There are people who are problem-solver-type mathematicians. I do think that the problem-solver type of mathematicians in domains that do not require a lot of deep theory—which, by the way, very much narrows the fields we're talking about, because even in combinatorics, there are a lot of corners that are currently connected to very deep analysis, making it not a shallow subject at all—I do think there are certain types of mathematicians who will see AI's equivalent function more than the other types.

Interesting. Have you tried putting P versus NP or the Riemann hypothesis into your system?

I don't think we're there yet. We'll see what comes out. I do think that there are interesting results we're going to put out soon about surprising capabilities that we didn't expect. Certainly, to be very frank with you, we did not expect Putnam to be that good either.

Constantly seeing that the capabilities of the technology have compressed the timeline predictions of even the people building it is a very good sign, I think, for a startup like us at this early stage.

9. Rock and Roll Influence

Totally. I guess one more thing I was curious about: you were on an academic path, and now you're running this company. Could you talk a little bit about the transition? What made you decide to shift gears like this?

I grew up listening to hardcore rock-and-roll music. I'm talking about when I was 5, I would listen to underground rock-and-roll music with a lot of curse words in it. I don't know why my mom didn't have parental controls on. There are some really secret rock-and-roll bands in China. They're obviously very politically rebellious, and they also write about all topics. The lyrics are quite interesting for a 5-year-old to listen to.

There's a part of me that really appreciates a diverse range of things happening in my life, and also the contrarian appeal. I don't actually think of myself as the most academic academic when I was in academia, and I'm definitely also not the most founder founder. I'm somewhat in between.

I do think that this startup is really fun. It's such a broad, brand-new adventure, and you're living the rock-and-roll days every day. It's very high entropy, and things are wildly exhilarating. You're empowering others to do the research of their dreams, to build their legacy and achieve their scientific ambitions.

I also think that making sure things run and serving the world-class researchers we have is another part that I greatly enjoy. I don't feel the transition. Somehow, I feel like I found my native land.

I think there's this very specific kind of founder personality, and all the sayings about having chips on your shoulder, or being both very spontaneous and very nerdy and methodological. I find myself to be everything in that portfolio, so I really love my job. I thought there would be some sort of shock or transition, but no—I feel like a fish in the water. It's really great.

I think working with this team of people coming from AI, programming languages, and mathematics—the 3 pillars together—is very interesting. Programming languages are more on the systems side, and we have many people at the intersection of programming languages and AI, at the intersection of AI and math, and at the intersection of all these applied domains, like chips or code verification.

By luck, or something, the people we hire for the 3 pillars also have track records in each of these application areas. It felt like the right team, and working alongside them is a lifetime honor. Seeing how they think about things from all sorts of perspectives—the mathematicians who might not know machine learning give us a great deal of inspiration, and the compiler literature has interesting techniques that can be applied here.

If you group the AI-for-math OGs, like François Charton and Alberto, who are doing mathematical discovery, and have them talk to the formal-proving people, there are interesting ideas about what self-improvement means. These discussions are happening every second inside the Axiom office, and me being a part of that—I just think I'm very humbled by it.

I feel like it's even more like academia, in a sense. It expands and stretches my intellectual boundaries more.

Love it. That's super exciting. I think that's a great place to end.

I don't know. If you forced me to trace why I enjoy being a founder, I would say that the 5-year-old who listened to hardcore rock and roll has some correlation to that.

Can you give us one song? I feel like we should put the song in the podcast.

Oh, Jesus Christ. There are so many songs. I can send you something after this.

Send us a playlist. Do you have a Spotify playlist or something?

I have a YouTube playlist, probably. Those bands are all broke now. They're all disbanded, and you find that the songs they write when they're poor—the ones they write when they have no money—are significantly better than the later ones.

10. Final Thoughts

I don't think it's the pressure of commercialization. I just think there's something about the burning desire to make it, and the hunger associated with that. It's something that we try really hard to preserve here at Axiom. We want to be constantly uncomfortable.

We're acutely aware that there are large incumbents, and we're a little bit late to the game. We want to have that underdog mindset regardless of what milestones we're also seeing ourselves achieve.

I think preserving that small-and-mighty attitude is something that I hope we always preserve in the culture: curiosity like a child and not taking ourselves seriously. That's why it's the perfect time for us to build. Right now, we're exactly at that phase.

Hopefully, we can preserve that phase. It's a bit like graduate students, for example: mathematicians sometimes produce their best work when they're graduate students.

Totally.

Yeah.

Well, great to meet you. This was really fun. Thank you.

Great to meet you.

Awesome. Thank you so much.

Thanks so much for listening to this episode of Gradient Descent. Please stay tuned for future episodes.