AI That Can Prove It’s Right: Verification as the Missing Layer in AI — Carina Hong

Hi, great to meet you.

Yeah, so I think that the idea where you have an infinite number of mathematical reasoning agents going out to industrial society to solve all the theoretical problems, I think that's incredibly compelling. I think through solving math, we also realize that it can solve a lot of other problems, such as verification, such as optimization. Actually, I think that math is great. And if you solve math, you can have physics, you can have a lot of logic and probability, and you can extend to a lot of things.

The world needs more math.

Yeah, I think people generally start with competitive math because it's kind of that you have, like, a known solution, and then you kind of start hill climbing the infinite, sort of like infinitely high mountain of math. There are actually two axes of difficulty. One is how creative the solution is, and the other one, roughly speaking, is how abstract the mathematical object is. So, say, a qualifying exam can be incredibly abstract, but the sort of creativity required to solve each problem might not be that high, might be very standard.

On the other hand, an IMO problem, well, it's very sort of easy to understand even by high school students, not very abstract, but it's incredibly creative.

Yeah, 100%. So we started out in mid-July, and so Putnam was December, and we were like a four-month startup. We were kind of looking at Putnam as this really hard math competition, and most people actually got zero. So over 50% of humans got zero, and I think over the 100-year history of Putnam, there's only five human perfect scores.

Is that how it works? That's right. You have 12 questions. You have three-hour sessions, morning and afternoon. So yeah, that's the setup. I think it was a Saturday. It was December 6th, and we all kind of gathered at the Axiom office and decided to put Axiom Prover in the real-time test. So it's not a benchmark. We got the exam from the proctor of the Putnam exam, and then we just basically threw it to the prover, and we announced that we got a perfect score.

That's right. Eight within the time limit, and then 12 out of 12.

Yeah, that's right. So I think that because we have a lot of mathematician friends, and they all have a lot of really hard research conjectures. So, for example, Professor LG, and he has like four failed conjectures, and this is the last one still standing. And he's an Israeli professor at Technion University. And there are also Dawei Chen, a Boston College professor who's an algebraic geometer, and he knows Professor Ken Ono, who's our founding mathematician, for years. And they recently met at this Joint Mathematics Meetings conference.

So he also supplied a problem. So people start sending problems to us, and then we just put the system to the test. And recently, I think, like a couple of weeks ago, we just announced that Axiom Prover solved these four research-level open problems. And it's quite interesting because it's probably the first AI to solve a research conjecture completely end to end and self-verify. That means the outputs are fully verified, 100% correct.

Without human intervention. That's right.

Yeah, I think it's kind of two parts. One is there are some really important mathematical breakthroughs that happen once in a decade, or maybe perhaps more than once in a decade for each domain, probably. But those require very interesting sort of eureka moments, deep intuitions, and very sort of almost lucky kind of moments. And there are a lot of other questions that are sort of proficiently, routinely applying the standard bag of tricks. And I think that a lot of the research questions can be solved by a combination of both.

So a little bit of intuition, a little bit of sort of just kind of like one step at a time. I think that we are at a threshold of mathematical renaissance, which is to realize that there are so many unsolved problems that will currently take, say, researchers months to crack, or even technical lemmas in those really longstanding conjectures, that we believe are not sort of out of reach for today's AI technology, but only through, I think, very intricate system design and hybrid kind of use of different methods.

And that's what Axiom is trying to do. These are the first batch. We hope to have a lot more coming. We actually have a few more research conjectures that are being proven every week, just by the supply of mathematicians from the world. And we try to put those problems to use.

It's interesting because there's, I think, a hindsight problem. So it's like, we didn't know how to do it. I definitely have no hope in solving those conjectures. And our founding mathematician, Professor Ono, didn't know how to do it either. Now we saw the Lean code, right? Thousands of lines of Lean code, and sort of read through it, understand it. And maybe we see some of the techniques as sort of standard, but I think the application of them and the combination of them is also not entirely—I think it's somewhat at the level of a junior math professor, say, a postdoc or a junior researcher.

Obviously, a lot of junior researchers do amazing work, and they have their Move 37 moments in some very longstanding open questions. But there are a lot of day-to-day research tasks that feel like they're at that level. There's also this question of, because it's solving the problem in Lean, which is a kind of machine language, not a human natural language, the proofs actually look quite different. So we actually analyzed all 12 problem solutions of the Putnam exam, and we found that a lot of the solutions actually differ from the human solution.

So because it is a Lean-based system, it is really good at routine bookkeeping, and it will actually choose a lot of the more mechanistic arguments over the ones that require a clever, say, one-picture solution. And on the other hand, there are a lot of these sort of caseworks that humans shy away from. It's just very easy for the machine. There might be a slight bit of what's difficult for humans versus AI being different.

So Lean is a programming language for math proofs. I think that's kind of the one-line, high-level explanation. There's this kind of concept called the Curry-Howard correspondence, which basically allows you to code math up as computer programs. And so Lean is similar to Python, but it also can serve as its own self-verifying function. So in the computer science analogy, it's roughly both the C language and the GCC compiler. So, two in one, it's a formal language. There are a lot of other theorem-proving languages before Lean, such as Isabelle, such as Coq, now called Rocq, and such as HOL, et cetera.

So there is this family of formal languages, and Lean is one of them. And it's a very popular language. There are a lot of mathematicians around the world that use Lean, that choose to code their proofs up in Lean, and they can just run it, and then they will see a checkmark, which shows that it's a correct, logically correct proof. And if there is an error message, maybe there is a bug somewhere or there is some sort of syntax or type mismatch, just like any other programming language.

The fun fact is you can actually use Lean as a functional programming language. You can write an autograd in Lean, for example. And that's very interesting because basically it allows you to do both math and code at the same time. So if you think about a security protocol, you can try to implement the code in Lean, but also prove its soundness in Lean. So it's a very flexible, adaptive language.

Yeah, I think the concept of formal theorem proving actually existed—automated theorem proving as a field existed before deep learning. So I think there are a lot of researchers, a lot of them in Europe, in 2018 and even before then, who were doing automated reasoning without the LLM component. And we actually have some of these people on our team; they were the authors of ATPBoost. And it's a very interesting time. In 2019, François Charton and Guillaume Lample, the co-founder of Mistral, had a paper which tried to put transformers on symbolic integration and realized that it can beat computer algebra systems such as MATLAB or Mathematica.

I think Ilya was actually the reviewer of the paper, and he actually tweeted about it. There is this other Fields Medalist, Tim Gowers, who said it was either amusing or game-changing because it was an open review. People didn't know if it's correct or not. And that was not amusing. That was the beginning of AI for math. And François is now also at Axiom. There's a long history of what people are trying to do with it. And I think Google started the AlphaGeometry effort in 2021, and that was a very exciting effort.

They realized that if you convert the figures and lines, triangles, circles, intersection points into symbolic expressions in a vector language, a specific domain-specific language for Euclidean geometry, you can actually try to do those geometric problems a lot easier using machines. And that's very interesting because it just draws back to my childhood, when I was doing Math Olympiad and I could never solve one Euclidean geometry problem. I don't know what's wrong with my brain.

It's usually the easiest problem of every competition. So if you go to a math competition and you don't solve the geometry one, then obviously you can't solve the inequality one. And obviously you cannot solve the number theory or the combinatorics holy grail. It's like that's the one problem you must know how to solve, and I don't know how to solve it. And I remember my teacher, the coach, taught me how to do the complex coordinate one, which is a very tedious way of converting everything that shows up in the figure into a complex coordinate and just basically manipulating those algebraic expressions.

And through that, I can solve it. I will solve it a lot slower than other people, but at least I will solve it. But it's a very interesting philosophical point, which is you can convert geometrical figures into algebraic expressions. And I think that's what they did. I mean, not exactly the human version, but AlphaGeometry. And then that led to AlphaProof. In 2024, I think Google sort of got a silver medal in the IMO, missing the gold medal only by one point.

That was my moment. That was my moment of IMO, at least. And then they couldn't solve the two combinatorics problems. And in 2025, no one solved the one combinatorics problem either. So in 2025, there's only one combinatorics problem. And I think that was kind of the history of things. There are also other players in the field and also a lot of really great academic labs doing it. We kind of take the approach that it's important for the system to be able to reason both informally and formally, and in a way bridge across these different abstractions, from high-level intuitions to low-level, more Lean-like formal checking.

Yeah. So informal is, say, reasoning in natural language, in English. And mathematicians, quite fascinatingly, have been doing reasoning in English for thousands of years. I mean, they write formulas in characters, but mostly they write arguments, proofs in English. And I think, to us, math is code in a way. Mathematicians have been coding in English for centuries and thousands of years. The formal language means Lean, and the output will be Lean machine code. I mean, it wouldn't be super readable to humans.

But I think there are two beautiful things going on here. One is the first time this sort of formal proving comes in to assist mathematicians, which is a traditionally informal reasoning subject. The second thing that's interesting is you can play to the strengths of both informal reasoning and formal reasoning. So you can bridge across these different levels of abstraction. And autoformalization, which is the capability of converting natural-language reasoning to, say, the formal language.

And that's harder than translation because it's different than, say, translating between two programming languages. You're translating something that cannot be verified, natural language, into something that can be. And that direction is obviously very challenging, but also very promising. There's also auto-informalization, which is kind of translating back, I mean, from Lean to English. That's easier than auto-formalization because most of the machines, AI, have seen a lot more English than Lean.

Correct.

Google was doing, I think, formal until, I think, as of the previous year's IMO, 2024, the AlphaProof system was a formal system.

That's how I would describe it. I think, first of all, that we are supportive of scaling. We think scaling works in a lot of the scenarios. There's also this question of sample efficiency, which is kind of how effective scaling is, potentially. And I think the sort of informal way to solve mathematics requires a vast amount of training data. You basically throw everything you can possibly find on the internet to it. Now, my question of that is, what if you also throw this vast amount of math text data to your AI, but you throw the Lean versions of them as well?

I think that we believe in doing things at big scale, and an internet-scale dataset of Lean, I think, in addition to the internet-scale dataset of math, is going to be quite interesting. And I think that we shouldn't do pre-training. We shouldn't try to just only train from scratch. I think we're kind of focusing on post-training reinforcement learning can potentially get us better performance gain.

Yeah, I think the world is realizing that we need verification. Verification means very different things in math. I think in early 2025 or late 2024, it means the numerical answer associated with each problem. Now, the thing is, reward hacking. We have seen from, say, FrontierMath and other benchmarks, which only compel a numerical answer, that it doesn't actually necessarily reflect the model's capability in logical reasoning. So it's able to get to the answer without reasoning through it, which is quite fascinating.

I mean, there's always this—when I did Math Olympiad before, there's always this classmate who's really good at guessing the answer. I don't know, like AIME, which is this exam that all the answers are between 000 to 999. I remember there's one year where my friend told me that he just basically guessed three questions correctly, versus the rest of us needing to reason it through. And, Jesus Christ, he just put, like, a zero in there, and somehow that answer is indeed zero.

It sounds very unfair.

And in a way, in high school, the teacher will ask you to show your work. So for a while, I think verifiable reward means that final numerical output. I think that people are now realizing it doesn't scale to the sort of math AGI, however you define it. Most of the sort of adult mathematics, mathematical research, are proof-based, require sort of step-by-step rigorous deduction based on logical reasoning. And a lot of them don't even have a numerical answer. Like, a lot of the problems are, prove that something exists.

Prove that something cannot exceed a certain value. Very seldomly, I mean, beyond the Math Olympiad kind of high-schooler context, would you have a math question where getting to the answer at the end of it—it's a lot more difficult to get verification reward for the intermediate steps.

And so, if you want to have a reasoning engine that really truly masters logic and mathematical reasoning, then you need to somehow get verifiable reward for the proof steps. Coding is great. I mean, people have seen RL in coding have incredible gains. And can we turn math into code? And Lean, which we just talked about, the Curry-Howard correspondence, exactly turns proofs into computer programs. So that makes RLVR possible in our setup as well.

Make AI perfect. The perfect prover.

I think the one thing, if you talk about perfect AI, I think people's first reaction is, wow, that's really valuable. I think a lot of the different labs are trying to reduce hallucination or increase the accuracy through many, many different ways. If you have a lot of industries where mistakes are extremely costly, that's a block to AI deployment if you don't have that sort of provable guarantee. And now that's the value of, say, catching the edge cases.

And there is this additional value of trusting that your edge case can be covered. So, two additional layers of value to reliable, consistently correct AI. In terms of how general this is, I think we start with math. Our worldview is math reasoning is a true reasoning layer of AGI. And I think a lot of the labs share that view, labs across the US, China, Europe. And from math, you kind of get to code. Math gives you proof of property, and code gives you output.

Output and property affiliated with it are two quite important parts of the digital world. And so from math, you go to code, and from code, you can run a lot of real-world experiments in the software stack. Then you can have a lot of other things. We don't claim to be doing things that are in the physical world at all. We are obviously not doing things that are non-verifiable. Say, just like sometimes mathematicians are stereotypically not the best sort of writers, we are not building an AI that's very good at literature.

But I think in a lot of the fields, such as math and code verification and verification applied to many different domains, it's incredibly valuable.

That's a very interesting question. I think so. As you can see, even within math, sometimes creation of domain-specific languages, like the vector language for Euclidean geometry, has its gains. There could be the case where, in other domains, something that is not exactly the abstraction of Lean is the right sort of medium. But in that case, you can sort of do code translation, and you can kind of build out the sort of stack that's required to use your Lean-based theorem-proving engine.

I think the sort of gap between, say, for example, Lean and another strongly typed language like Rust is a lot closer than the gap between Lean and English. And I think that's a lot of the commercial value. I mean, if you can sort of reason in between informal and formal space, that I think is going to unlock a lot of the things beyond just the power of a formal theorem prover.

I think we want to try to figure out what are things that can be done in software. One is, I think, math and code, they really complement each other very well. I mean, there are a lot of great code generation companies. We can provide provable guarantees and code verification. There are a lot of other domains where just that sort of verified generation capability is incredibly valuable, like hardware. And then I think if you can have a lot of theory and you can have partners who are really good at real-world testing, then that is AI for science.

And I think that's also incredibly promising. I feel like this is a generational effort. It's going to take a long time. We're going to see the DNA of the company remains math, and we're going to see best first market, maybe verification, best second market. I don't know what that is. Could be optimization. A lot of the things, I think, are waiting to be explored, but just the generation-verification loop, I think, itself is going to have a large TAM.

And then I think there are a lot of things that we're also learning together with the potential customers.

Seven months old.

Okay.

"Competitive math kid" is such a great term. You can parse it in different ways: competitive math kid, competitive math kid.

Both. Well, I think I like to win.

It was extremely formative. I think years of Math Olympiad training, you have one goal: that is to score as high as possible on whatever that next math competition is. You have people that are in the same sort of community circle that are also doing the same thing. You're friends with them; you're competitors with them. There are a lot of background reading, learning, exercises you need to do to overprepare for every competition. I remember I did 75 exam papers to prepare for a competition that I didn't know if I would be selected for, and I didn't end up being selected for it.

I think I was like 14, 15. I think I learned a few things. One is resilience. I think you get addicted to pain and suffering, so the word "resilient" is almost a paradox because it's like you like it. Failure is a given, I think, throughout that time. I mean, the exam keeps getting harder and the number of people competing keeps shrinking. In elementary school, I had like 1,000 friends competing for the spots for middle school.

Then middle school is like 90, okay? And then high school, 25. That means the vast majority of your friends lost the opportunity to compete. And that's a very interesting thing, I think, it does to a child. But then I also learned some other side, not just the Math Olympiad. When I was, I think, 14, 15, I got into the Ross Math Program, which is one of, I think, the best high school math camps in the States, at Ohio State University.

I think my first trip to the United States was that summer. It was a summer of eternal joy. Every day I would be learning cool research math. They taught us undergrad math, and they asked us to deduce everything from the ground up. We were asked to prove zero times everything is zero by a limited number of axioms.

And that was very defining. It felt very different from math competitions. It's not like how many people will win that award. It's like there is a vast amount of math that you just have no idea about, and you get to build it yourself, almost like one brick after another, right? From the limited number of theorems you are provided, you prove new things. So we're given about 25, 30 problem sets, and each of the problem sets have problems that are probably just bookwork theorems, and you would just learn it in college.

But instead of presenting it as something that is a given fact, it asks us to prove it. So our world of mathematical knowledge is constrained to how much we can prove. And that's actually what's going on right now with Axiom Prover. Axiom Prover has access, obviously, to a lot of the world's information, but because the Lean data is so scarce, it's a lot less than, say, the amount of code data out there. It's only a two-digit million number of tokens out there in the open world.

Axiom Prover learns to prove things, and it kind of self-improves in a way where all the things that it proved get fed back into it, into a kind of skill library. It can be applied for the next challenge. There's also this sort of self-challenging, conjecturing component that keeps giving it harder problems, just like my camp counselor gave me the problem set. And this is a very beautiful process. I think without this sort of right order, sequential order of introduction, I wouldn't go this far in math or love math as much as I do.

I think the sort of curiosity and discovery is a basic human need. And that definitely exists in, like, the teenage child, and that being used to motivate and inspire mathematical learning, I think that was a very beautiful process.

Yeah, I think the Rhodes Program did a really good job, and probably too good a job, to encourage us to just shift direction. It has this sort of broad belief that you need a lot of disciplines and studies to help you become a global leader. That's what the Rhodes Scholarship is trying to nurture. People who have a background in STEM, they will encourage you to go into liberal arts. I wasn't fully encouraged to go into liberal arts, so I picked something that's kind of in the middle, like neuroscience.

Obviously, I think at Oxford I had a lot of math friends, and so math was still part of the equation. I was also trying to apply math in my neuroscience study, specifically maybe because I'm afraid of animal experiments. Like, I'm probably just gonna stay in data analysis, computational neuroscience. I was quite interested in topological data analysis and persistent homology. But later I realized, I think it was like two or three months after the school year started, I realized there's something called UCL Gatsby.

UCL Gatsby is this premium AI hub in London. Oxford to London is a short train, and there's so many world-class faculty there doing really cool research in, say, theoretical machine learning, analyzing the neural dynamics of stuff. They're also doing various other applied AI research, and some from a cognitive science motivation, but really the core is AI.

I think there's a lot of things, actually. My junior year—I mean, my last year at MIT—I kind of grew up with a very sole focus and goal to do Math Olympiad and then do math research. And the very next step is to probably go to grad school directly and probably not even do the Rhodes Scholarship. I'm not sure, because a lot of the Rhodes Scholars are politicians or aspiring lawyers, judges. I'm like, I just want to have some fun intellectually.

At the end of the neuroscience, I was like, okay, I want to go to Stanford to start my math PhD. But also, there's this incredible opportunity of Stanford Law School. It's really one of the two first-ranked law schools in the country. And they have really good IP professors who marry AI and copyright law. They have Professor Mitchell Polinsky in law and economics, where you basically are doing differential equations, but you're analyzing deterrence and retribution, the ratio of each sort of criminal law measure.

And there are a lot of other things, cool methods to apply textualism to constitutional law that's very similar to looking up definitions in math textbooks. And so I was like, okay, that's very cool. So I did my—I mean, the JD/PhD is like, you have to spend one full resident year in the law school. So that was my first year. I spent one year being a diligent law student. I was even trying to apply for clerkships. It was a fascinating year, and I learned so much.

And then the second year, which is kind of a very interesting year, where I was browsing all the AI-for-math research papers and realized that, wait a second, there's so many ideas. I mean, from Draft, Sketch, and Prove to, I think, STP, Self-Taught Prover. There's so many exciting papers, and I wish I just had the resources in industry to execute it. And that was when I think very, very soon after, I just basically decided to do Axiom, like fully focus on the company.

So our very broad vision is that we are going to have a conjecturer, we're going to have a prover, and then there is a knowledge base. Let me take a metaphor, because this is quite a niche area, a very small subfield of AI. Suppose you are sailing on an ocean, right? And where do you know where to go? Your ship that basically decides where to navigate, that's your conjecturer.

And then you sail in one direction, and then you land at this island. Okay, well, do you know if you have been on this island before? You don't necessarily know. Basically, you need to look up your knowledge base. You want to make sure that this is indeed uncharted territory. And then once you realize that it is uncharted territory, how do you know if it's, say, India or the West Indies, right? Is it going to have some rare metal?

That's where your prover starts coming in to basically prove this new conjecture that is not in the knowledge base, that is mathematically correct and has merit. And then there's auto-formalization, which is the ability to reason across informal and formal space, kind of weaving all these.

So we do post-training on, say, open-source LLMs.

Yeah, I would say here the conjecturing part is still the underdevelopment part. In the last seven months, we've been very focused on the prover and also made a lot of progress on the knowledge base. So in the Putnam exam, right, you don't need to conjecture. You have 12 problems. They're incredibly hard, and they are basically tests for your prover. So Axiom Prover, tried on the Putnam exam, got a perfect score. The underlying system is an ensemble of models, and there's also a set of deterministic tools.

And also there's a proprietary dataset that's very large. So a combination of these three things led to that success specifically. For the deterministic tooling, it's quite interesting because these are actually written for Lean in the language of Lean, a bit like metaprogramming. And that's very interesting. We are actually going to release them on the public API, all these dozen tools, very soon, beginning of March.

Yeah.

I mean, it's releasing the infrastructure for mathematical reasoning. It's called Axiom Lean Engine, ALE. It's interesting because there are a lot of grassroots efforts from the open-source community to try to provide infrastructure tooling for Lean theorem proving, because Lean is a relatively new language, and there are a lot of reasons why it could be a bit slow sometimes. There could also be things where, if you assume an axiom that's mathematically incorrect—like if you assume n + n = n—then you will be able to prove 2 + 2 = 2.

You don't want that, right? Two plus two equals four. So a lot of this sort of verify-proof is actually one of our prover tools that's about to be released. And that's actually 100 times faster than the other counterparts that are the open-source effort called Comparator. So a lot of them are hopefully going to make everyone prove more theorems in Lean.

We had a little bit of a cold-start problem, right? I think the data is quite scarce. So while there are more than 1 trillion tokens of code, it's probably a lot less for Lean. So we had to basically take our bold data bet to generate a lot of Lean proprietary data. So that's one difficulty.

That's right. So it's interesting because when people talk about synthetic data generation in the unverified domain, you really don't know the quality, right? How do you know this synthetically generated financial advisor data is actually good? Then they have human experts to try to label it and grade it. Here you have Lean. So you know that your thing is correct, at least. And if you do good quality control on the statements, then you will have things that are of mathematical merit.

And when we take datasets, we use things like auto-formalization to convert existing math from informal language to formal language. We also do things that are more formal-system-inspired, such as repair. Fuzzing is actually to make a lot more synthetic variants of the existing formal data that we currently have. So the other difficulty, I think, is Lean runs on CPU, and then the sort of LM part runs on GPU. So you have a little bit of CPU-GPU.

I mean, it's engineering, just a very interesting effort where ideas are out there. You need a very strong industry-strength engineering team to execute the many good ideas maybe some academic researchers have produced, some of our researchers have produced, at this scale. In terms of how compute-intensive, it's not horribly compute-intensive, definitely not compared to pre-training. I think that data is a large part of it. I think that good infra engineering is another part of it.

It really varies. I think there have been cases where a hard problem in Putnam takes one million tokens and stuff. But there are also a lot of other things we could do. We in-house have something that can shorten proofs. So, for example, you can shorten a proof significantly, 20 times shorter. It's different levels of how you would like to count how bulky a proof is.

We focus a lot more on—I’d say, so there's this sort of team of really strong machine learning researchers and engineers, and they're all both researcher and engineer in one. They're really amazing. We have a lot of really good people from Meta, from Google Brain, from Anthropic, et cetera. And we just keep hiring more and more sort of frontier lab researchers. This part, I think, is focused on developing the core capability of the system. So we want to basically push the goalposts forward, right?

So, from Putnam perfect score—that was four months in—then two months later was the four research conjectures. And then during this middle, we also tested something that is transfer learning from math to code verification. So, another evaluation on a community-recognized benchmark. We want to kind of try where we can get, because we have really great mathematicians telling us how we should think about certain research problem targets. And we currently have really hard research math problems in-house that we are tackling.

It's showing some promise. It's also obviously getting stuck. So there's this part, and this part is the current focus of the company. And once we know where the frontier is, then we can try to say, okay, let's make it robust. Let's make it sort of production-grade. So when 1,000, 1 million people hit it, it doesn't break. But this part is kind of sort of an effort that's surrounding that. And sometimes people jump between different tasks as well.

Now we learn something about the applied use cases. We also have a lot of subject matter experts, and we are hiring subject matter experts to join us to work on theorem verification, to work on code verification.

There is. There is, yes. So what is it? Roughly by, I mean, journal submissions, a lot of other factors, obviously. But you can think about currently the batch of papers Axiom Prover has autonomously proven and mathematicians have written. You can probably get into Journal of Number Theory, Journal of Algebra, like that level. Well, that's a very different question from Annals of Mathematics or JAMS, Inventiones. That's one big jump. I think to get to that sort of result requires a lot of pushing.

And we are not pushing it to just chase the amazing feeling, which is quite amazing, of proving something that is grand and open for a long time. But also, at the same time, we are basically teaching the model things that it could not do before, such as a more complex reasoning tree. So on the easy end of the problem, we have 40 nodes. On the hard end of research questions in-house, we currently have a research problem with thousands of nodes. So it's a much wider and much deeper tree.

And we want to see: are we going to hit a limit or not? We currently are not seeing one. So we really want to basically scale the complexity of the reasoning of the problem. We want to make the AI be able to do library learning. That is, we have seen it actually quite promisingly auto-formalize definitions, which is really hard. So in math, you have theorems, proofs, lemmas, propositions. Basically, you have definitions, and that's very hard to ground. So you want to be able to auto-formalize definitions.

You want to be able to have the model system explore definitions that will still be relevant for further proof.

There's scale-up and there's scale-out. So we're currently scaling up in difficulty. We believe that is a defensible move. We believe we are currently doing certain things interestingly and are ahead of the curve in terms of how we get rid of running out of context, this kind of problem, how we scale learning from experiences, how we scale inference. I think we are doing that. And we are also scaling out in a way of both. There are some math problems that are not auto-formalized, actually.

There are interesting things you can do. You can choose an existing math result and try to auto-formalize it, or you can choose an unsolved math problem and try to prove it. Both are incredibly valuable. I think people talk about unsolved problems all the time, and there's a lot of value in actually picking good targets to try to auto-formalize. A lot of these are unsolved or not completed because they are very complicated in terms of the sheer volume of that result.

So that's kind of scaling out within the domain of mathematics. And then there's also scaling out from math to other domains, such as code verification and then hardware verification.

There is this friend who taught me a lot of things about math, and he said that, like, you don't celebrate when you win the Fields Medal; you celebrate when you get into the shortlist for the Fields Medal. So obviously there's only a finite number of awards. And I think that we really want Axiom Prover to be able to solve one longstanding problem in mathematics that you can objectively say, even if it's an AI or double-blind, whatever, that will be in the shortlist.

Because then there are reasons whether—

Not quite political. I mean, sometimes fairness, for example, if a certain domain just got—yeah, but to the shortlist, that is sort of the objective standard.

The first couple—well, not the first couple of months, a couple of months before we actually started executing, it was incredibly exciting for me on an intellectual level. Like, every day I had this sort of excitement. Like, it's like I drank, like, six cups of coffee kind of excitement for months. And the main source of that excitement, which I will tell you actually about—my colleague Shubo, a good friend, his excitement of this in a bit—but my excitement is, like, just like we're now realizing that we are at the threshold of a mathematical renaissance, we could also be at the threshold of theoretical discoveries in science.

Massive, massive scientific discovery at the theory level. And I think what I mean by that is we have been in a very math-poor world. The supply of outlier mathematical reasoning skill is so lacking that people are, like, in a scarcity mindset. Like, you will hear discussions of, oh, like, this problem is so interesting. Unfortunately, I'm solving that problem. They should all be solved. Everything that the human mind can conjecture, find interesting, find tasteful, should be solved by AI—hopefully, the majority of them by Axiom Prover.

And then you have the question of high-energy physicists. When they talk to mathematicians, generally they will have interesting opportunities for collaboration. Like, I actually have this paper with Professor Ken Ono and others, Shengtong Jiang and Michael Mertens, which addresses, like, the elliptic umbral moonshine conjecture. And that kind of stems from, like, three, I think three theoretical physicists. They conjectured this based on their observed, or, like, physics-like phenomenon that I know, frankly, not very much about, but I can solve the math part.

They come to the conclusion that what they believe are beautiful phenomena, that they find it worthy to formulate as a conjecture and publish as a paper, have a proof because they know some mathematician. Well, that doesn't seem right. Like, I think that the really beautiful vision is for all the theoretical problems, all the curiosity, all the lack of understanding to be resolved in a satisfactory way across all scientific subjects.

And beyond this, right, there are things that we still cannot solve that we will get a closed-form sort of—not a closed-form solution—we'll get a very precise approximation, as precise as possible. I mean, there's a lot of value, for example, to know, say, what is after the 1,000th or 10,000th digit compared to what is after the third digit. The world is actually, a lot of the time, not diminishing returns. The last mile carries a huge amount of value. Like in search, for example, if you cover some edge case, you likely win.

You will be a market winner. In, for example, writing, right? If you write just that extra bit, or any sort of creative art, getting that extra mile correct or done has a lot of value, like optimization, precision. We can try a lot of these things as well. And then, as math kind of helps with both first-principles understanding and trial and error, it's just kind of this cycle. Like, you have some first-principles understanding, you try testing it, you try some trial and error, and you maybe give some sort of risk-bound uncertainty principle, robustness estimation.

And then you go back to your first principles, and then you go to your trial and error again. You have this sort of circle of discovery. And this is really not the end of it. So that's why I'm already very excited. I think this is going to be amazing. Ideas can diffuse between different fields, a bit like you have abacus and now you have trade and commerce, you have calculus, integration, you have thermodynamics, mechanics, the Industrial Revolution. You have the Babbage engine, which is to calculate log tables faster.

And, okay, well, you have the prototype of computer science. The rest is history. You have number theory, you have RSA, you have all these kinds of mathematical tools kind of open up new discoveries and new use cases, and in turn demand more mathematical tools beyond this cycle. And this cycle marrying science—here comes code. We haven't even talked about that. And that's why actually Shubo is very excited. So Shubo, CTO of Axiom, before that was a long-term Meta veteran. He was an IC director.

He believes in code as math. Okay, so through all my good friends telling me about Lean, telling me about the Curry-Howard correspondence, I believe math is code. He believes code is math. What does that mean? Okay, so it means that you can try to fulfill the dream of Donald Knuth's literate programming, have computer scientists, programmers enjoy the luxury of mathematicians where they can reason in natural language. And this is kind of starting to happen, right? Vibe coding, like front end, right?

Like, we can and have very cool, lovable websites. But, like, how do I vibe code a nuclear reactor? How do I vibe code control flow? How do I vibe code complex systems that require, like, quite honestly, superhuman hierarchical reasoning skill? It's interesting because you're not in code alone. You have code and you have math, so you have, in addition to the flywheel we're already seeing in the coding companies, an additional layer of flywheel of verified code and sort of math starts to come in.

And this kind of flywheel of data keeps compounding. You have actually two, even if you're counting the science part, three orders of flywheel.

That's why we have to execute, like, something every couple months. Like, we have to move extremely fast. Like, there's so much to do. I think Axiom is a very, very young company, and we are at, like, the very, very beginning tip. And we are already—I personally feel some sort of shock and emotional response. And I know some of my mathematician friends, Scott Kominers, who's a Harvard microeconomics professor, also a Morgan Prize winner—we're good friends—and we all have this sort of emotional response when Axiom Prover proved Wiles' conjecture, proved that almost all primes are partially regular, partial Vandiver conjecture.

Which is one part of the original Vandiver conjecture that has been open for 90 years. The parity of differentials for surfaces of genus 0 and 1, by an algebraic geometry paper. We are really just leaping across a point. I mean, Putnam marked, I think, the end of AI trying on Math Olympiad. We are very glad that we got a perfect score. It's a really good period point. Putnam 2025 is, by a lot of experts, graded harder than IMO 2025.

So it's the hardest real-world Math Olympiad test. And now we are leaping, we are leaping to research. And I think I'm going to have another similar emotional response if it really does solve one of those breakthrough mathematics problems. Interestingly, I think there are a lot of experts in domains that are currently overlooked by AI development. So if you're a software engineer, you feel like, oh, web coding really changed and improved your quality of life in a meaningful way. There are people who are in industries where, because of lack of provable guarantees, they couldn't use AI.

And there are, for example, aeroastronautics, for example, like, I think defense, for example. There is no partial credit for a mostly verified GPU. It's all or nothing.

Yeah, yeah, yeah. A mostly verified, formalized hypervisor. I think for these experts, they are currently kind of handholding a lot of the traditional tools. Their life has not been changed. And I want to see the AI for math movement that Axiom is hopefully leading transfer to these domains and try to solve some of those problems as well.

So I think a lot of the adverse reaction from the math community about AI is actually coming from the fact that they cannot verify an informal solution. So suppose GPT generates a math proof, a million lines. No one's going to check that. I'm not going to check that. I know there are a lot of really great data labeling services; they couldn't have that sort of level of expert to verify a proof of that length. It's just hard to do.

On the other hand, if you have a formal certificate, like a stamp certifying that this is a correct Lean proof, I think people are a lot more receptive to it. And that's why actually a lot of mathematicians, especially almost all of the new school of mathematicians, are accepting Lean. What they want to do is have humans formalize in Lean. Now it's really fun for humans to do Lean. We have a lot of the initial Mathlib people here at Axiom, and it's a very fun team to see them formalize some statements.

But when it comes to, say, hundreds of thousands of lines of Lean code, which is already not hypothetical, an automated reasoning team at some big tech currently has 260,000 lines of theorem-proving code—not Lean—to verify one component of a hypervisor or CPU virtualization. So that cannot—I mean, they actually did write it by hand, but it's just not quite sustainable.

I remember reading the anecdote of Hamilton, that he writes down all his flaws and shortcomings every night and forces himself to correct them. I know what my habits, flaws, and shortcomings are. I'm a very spontaneous person. I don't have the best ideas when it's planned, which I think sometimes, in the course of research—you have math research—you have these kind of very interesting eureka moments, I think. So I try to overcome that in my day-to-day.

I try to do scheduling very intensely. I try to surround myself with people who inspire me to execute faster, and that's basically the entire team. And I think it's a great honor to be working with them every single day. I think, like, I go into the office and I look around and I hear the discussions, and I'm like, wow, I'm so lucky to be here. And I think that's something that, in this kind of talent market, people like to work with people who value their intellectual judgment, respect their voice and opinion.

And I think Axiom has this sort of very flat, non-hierarchical—everyone's a member of technical staff or a mathematician, right? If you're earlier founding, plus that, this culture is really great for, I think, the open communication of ideas and debate of ideas.

It helps with the pace of iteration, helps with being more correct. A lot of things I'm learning very rapidly. I mean, it's been a very interesting roller coaster, like seven months. When I was in math, I mean, there is this sort of idea where you have taste, and sometimes this taste can be interpreted as arrogance. And I learned that ego is a really, really bad thing, and we should just basically get rid of it.

Yeah, we hire people for taste, but not for ego.

And I think that's a very interesting kind of—

Right. So one is, basically, that means I have to learn every day because I need to have a certain basic amount of taste. And also the other people who are senior at the company, research scientists, need to have that sort of amount of taste and what makes us excited. And when we are excited, we just go after that person.

We have had a lot of, I think, extraordinary hires from amazing and interesting backgrounds. And we really like this team. And I think that we raise the bar for hiring actually continuously. So we recently have an uptick in the number of people who would like to join us and are candidates that we're excited about. We take recruiting very, very seriously.

So quite interestingly, I think at the start of this, I realized that there is a movement, and this movement of AI for math is very much, by and large, in academia. Or actually, people are hiding in labs, like secretly doing AI for math where their day job is something else. So when I talked to each of these people, it was a very, I think, mutually exciting feeling from both parties. And basically, it's like two whales and just kind of realize that only they can communicate in that frequency range.

And that happened multiple times. I got very inspired by this. I think there were a lot of times at the beginning where fundraising was quite hard, I think. I mean, I'm a nobody. No one should trust me with their large amount of money. And I think that was very difficult and challenging. But it was those conversations that basically made me realize I have to do this. I just have to. And I have to be the best deal for this team because my team deserves the best of the world.

And those kinds of intellectual alignments were, like, a main theme. And the other thing I realized was that they found, say, maybe the other AI-for-math opportunities not particularly attractive or whatever. Maybe they don't want to move geographically to London or to China, or maybe it's just a different kind of vision. So kind of gathering them was a relatively natural process. And then after that, I think when you have a bunch of really smart and nice people, you just attract other smart and nice people, and especially people who are adventurous, rebellious, people who like to disrupt, who come from Cognition and want to disrupt Cognition.

People who come from math want to disrupt math. And disrupt and, I guess, elevate as well, because they do have a lot of affection still with that field. So I think it's a very interesting—it's almost like a tribe. Axiom Math is like a tribe, and we have more and more people joining us. And sometimes I feel like both in those initial conversations and still now, and even after all this sort of talking to the world about what we are doing, we still feel like secret keepers.

We still feel like we cannot fully elaborate and emphasize the thing that we are seeing that is the next frontier of AI. That is a generation and verification loop. That is the discovery of verified knowledge.

Yeah, thank you so much. Yeah.