🔬Scaling Past Informal AI - Carina Hong, Axiom Math

But it's for the first time now, I think, verified AI is to open up collaboration. Either it's human AI collaboration. Well, before it blueprint, like, that's human human collaboration, and Lean was a grounding, was a verification, formal language.

And then human AI collaboration like we're seeing now, future AI agent agent agent like collaboration. Like, I think verified AI is for openness. It's not for meeting the requirements of closed industries.

And I think just like I think verification should not be about, oh, I remember, like, you know, there's this article, like chatbots mixed up. Oh, there's math solution to hallucination. Verification to me is not about lousiness.

Verification to me is about scaling brilliance, compounding brilliance. It's like just kind of going back to the collaboration point. It's about Ramanujan being a much stronger mathematician.

Well, super, super excited to be here. Also, think like, you know, this is a series A, so it's very, very interesting timely podcast. We're like a seven, eight months old company.

So definitely means lot to us. It's a really cool milestone. We're currently about like 30 people now.

So kind of going into, I think this amount of funding will like give us a feel that it needs to accelerate the strong execution momentum that we have so far. I think like people think of us like there are many kind of ways to think about Acxiom people think about us as a math startup. So math startup, lean startup.

The other obviously things that we do that are formal verification, we think verification is a really good best first market format. And so I think this fundraise is gonna like let us explore some of the applied domains as my colleague CTO Shubo said in the little launch video of the series A we had is it it lets us broaden our dreams. So yeah.

So when, you know, one recent models like just came out. What was Anthropic kind of like secretly working on back then? Was coding.

And everyone knows they're working on coding like OpenAI, Meta, Acxiom. Everyone has full knowledge that Anthropic was working on coding. And they just like overlooked it.

They thought, oh, they are at B2B plays. They just want one vertical. You'll think of coding as one vertical.

And now look at where we are today. Coding kind of like strong transfer learning from coding to reasoning to basically monopoly in the future of reasoning. And I think that's really shocking.

The people who are working on coding, I think back then believed in something that we believe, you know, similarly with math and Lean Now, which is that if you have more structured and formal data, it's going to be a lot more horizontal than the specific vertical we're tackling. So, you know, if today we are doing, you know, math informal way, like the standard chain of thought data, train a math model based on human preference, then I would say, well, perhaps we're just a math startup, right? But, while we are pursuing math, we're also doing things that do have transfer learning to other domains.

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

We're also thinking that this is going to be fundamental to verified reasoning, and we kind of talk a little bit about verified AI.

I think I have a lot of like rumor mill that I probably shouldn't like put it on the record. Like, I think, you know, like researchers talk, they play card games. Yeah.

There are really interesting reasons if they are or are not doing it. I think that's like kind of the takeaway I have, which is that if you're like at a frontier lab and the direction actually does change a lot for a lot of the reasons beyond your control. So I want to kind of like bring us back to the alpha proof moment, right?

Like alpha proof was such an amazing that really the 2024, 28 out of 42 performance was the IMO moment for me. It was not gold in 2025 because across 2024 and 2025 AI models could solve all the problems that are not combinatorics. The only difference is that, you know, if you get all the problems that are not combinatorics, you get 28 in 2024 35 in 2025 because there's only one combinatorics question in twenty twenty five.

After AlphaProof kind of like we didn't see a lot of the formal math, you know, or kind of progress from Google DeepMind. That's actually because of reasons that are not necessarily technical. But if you're at a startup and you have very singular focus that is formal math and verified AI, then you know, you get to work on a really cool problem for a long time and you have like a lot a lot higher likelihood to get to where you want to be in terms of like progress and breakthrough unlock.

So, yeah, just define that for us. Yeah. Like a lot of people think about formal verification as an ancient, you know, subject.

It it existed like as long as, you know, way before like deep learning and existed in the time of rule based computer science. There's this really strong push of like formal verification around like since ever since 1980s, really interesting historic anecdotes such as I think the Paris trade union demanded that the automatic switching of the subway system needs to be formally verified for safety purpose. So quite interesting trade union for for technology.

Yeah. And like, I think around the time of challenger, both before and after European space agency was using formal verification for the Ariane spacecraft. It's also interesting.

Boeing, Airbus for verification. And then more recent years, right, I I think like there's a lot of push about automated reasoning at AWS because they have a lot of enterprise customers that really require things to be be 100% verified and there's no edge cases missed and just general testing doesn't satisfy the need. So a lot of people think about verification as something that's like annoying because it's like tax and compliance.

Like it's making sure that we are good to go. Right. And like, that's really not the way.

And so we talked about like verification. I think our competitor, when they launched, they talk about formal verification, pre reasoning, they talked about it in the time of hallucination. And maybe for them, like formal verification is about the lousiness, the hallucination.

For us, no. Like, for us, verified AI is about the brilliance. It's about scaling and compounding super intelligence.

So this is a quite a deep point, sometimes it takes a little bit of explanation. So if you think about like, you know, the the place of brilliance, for example, Ramanujan, like, he's a brilliant mathematician. He was able to find a lot of, like, interesting formulas just by intuition before he know how to do proofs.

So he went to Cambridge, you know, work with Hardy and Littlewood. And, you know, in the famous movie, the man who knew infinity, there's this like storyline of how hard it was for Hardy to force him to no longer rely on intuitions and do proofs. After he learned proof writing, he came out as a much more powerful mathematician whose results like intuitions turn into theorems and future generations of mathematicians build on that those theorems.

So it is a way to kind of scale and compound the intelligence that we already have. Another example mathematicians kind of have been writing code in English or their respective country's natural language 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 mass community.

So the law.

in the community. So it's interesting, right? Because that is kind of human mathematician enforced.

Right? And so it's a peer review process, peer review of the paper currently takes two years. Okay.

So, but proof assistant and formal proof trackers like Lean still found its place. Right. And why?

If I'm a mathematician and my work can be peer reviewed by other humans. Like, why do we even why do mathematicians even play with lean? Right?

And why do we even talk about kind of like lean based assisted, like they're improving? It's because it handles a low level. For example, we're not even talking about AI.

We're talking about, for example, the grind tactic in lean. It can currently handle a lot of mass proofs, like at a very low level. And this is pretty shocking because I have seen, you know, actually another company working in the same space, like, you know, some of their demo.

And I look at the demo, like, it can actually completely be handled by grind, which is a tactic in Lean. Can you explain what Lean is to non Oh, okay. Yeah.

Think our order is like a little little wrong. Yeah. So Lin is a computer program a bit like for math proofs.

It is a formal language just like its cousin, isabel, c o q or rock and some other further cousins like Daphne, Agda, like these formal languages, Ho, etcetera. Yeah. And what what does it do?

It it basically, if you have a proof written in the program in Lean and then assuming there's not no any, like, weird things happening, like, you know, unintended, like use of sorry, which is a tactic that let you take things for granted assuming everything is safe. Hence people have tools like Comparators, Safe Verify and Acxiom recently rolled out Verify Proof that's like 100 times faster than Comparator. Then, you know, once you kind of execute that program, can like once it compiles and it tells you that it's correct, then it is the proof is actually correct.

So it's like a type checker? Yeah. That is based on this result called Cora Howard correspondence, which turns proofs into programs.

So I want to talk about the magic of Ling. Why I think it's a really good programming language is because on one hand, if you don't care about the formal part at all, you don't care about the logic part, you just want to use Ling to write code. Can.

Like we have had candidates actually currently, you know, the person is working at the Lean FRO. He wrote AutoGrad in Lean in our interview process. So it's a it's a Turing complete language.

That's right. So you can write you can do a lot of things with Lean. You can it's a it's a functional programming language.

Okay. Right? And then you can you can also use it to so you use it to do coding.

You can use it to do math. Two in one. Okay.

And kind of going back to what I was kind of getting at. If mathematicians are already enforcing that most proofs, you know, say say maybe not all mathematicians, but the Ivory Tower and people in academia, all proofs are correct. Why do we even need Lin, the model checker?

It's because Lean has tactics that help them handle the low level calculation or proof or deduction, not calculation, then for them to be able to navigate in a high level intuition space. So this is my point that it is not about like formal verification or verified AI. To us, it's not just about handling or like kicking out the lousiness, the hallucinations, the mistakes.

It's about scaling brilliance. It's about super intelligence. I actually Terence Tao has a great video also about using lean to as a way you can collaborate because you can use stories.

That's another point I want to I want to talk about. Right? A lot of people think about, you know, what is our what is our market?

It has to be some like really niche industrial societies area that is mission critical, safety critical. No, that's not the The TAM is all code. The TAM is is a a right of first refusal on all AI generated code, like right of first refusal, meaning you get to choose whether you want to verify it.

So this is the important part I want to kind of come across, which is that people talk about formal verification as almost like painful because it has all these like stringent requirements. Up until now it has been very painful. Yes.

Yes. And to us, it's actually verified generation means performance gain. It means higher sample efficiency.

It means a startup like us with like, you know, still we raise some money, but lesser compute budget, lesser data budget, then FrontierLab will be able to match and even exceed, you know, performance on superhuman tasks. In fact, for the Pan Am exam that we just competed December 2025, which we did in real time, Mass Arena, which is this organization that evaluates a lot of LMs, found the best LLM, DeepSeq, got 103 out of a 120 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 five winner score, got one one ten and we got one twenty.

So it's the first time actually, I remember when we were starting this, people were like, is it even possible that a formal mass, you know, system with so much orders of magnitude, last data can match or beat an informal LLM and Punnam is the first time it beat. Right. And so we're not thinking about it just about the painfulness, the challenges it pose.

LLMs. What what's different about what you do? Yeah.

So we heavily rely on kind of data called lean data. And we kind of talked about lean is all the data that we have that's lean proofs, you know, it's correct. So you know it's correct or not.

And that's quite important. So, know, we have a system of models. These models are post trained and using RL or SFT.

Yeah. And there's obviously an inclination for open source, you know, base models. So it does speak English.

Yeah. Probably knows how to code. Yeah.

But also you fine tune it or or continue Yeah. Pre the base model might be similar to what everyone else is saying as well. Right.

If they're not kind of pre training their model. Right. Yeah.

And then we basically do this, you know, RL for for formal math kind of. There's I think a standard pipeline or like, you know, tricks of the trade that people use. We try to innovate really on top of it as much as we can.

I think that we found scaling inference to have almost no law, recursively decomposing, you know, a proof goal into many sub goals and then learning to backtrack as well.

a system that can do really well in number theory can do well in give me, you know, another another field Yeah. Of Exactly. Well, actually, I think this is the way we think about it is it it depends.

It depends on whether topology has a lot of the existing definitions as almost like, you know, the the math infrastructure existing. Because what people have found in the past is when people were building out Mathlib, like, you know, for the algebra, you know, bookwork, like they they can just So MathLib being the lean, like, undergraduate library kind of stuff. So it's like all the proofs that you learn in undergraduate math.

Yeah. And they're all sort of in lean. Yeah.

So for example, some of my friends who currently are at Acxiom is, you know, crazy, like, full circle back moment. Kenny, we're like friends for, you know, five, six 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 than for for analysis. So so that's that's interesting because for analysis, a lot of the definitions around convergence limits sector becomes tricky. And so I don't think there's a lot of like topology in mathlib today in terms of like differential topology, differential geometry kind of stuff.

So, you know, system likely will not do very well on those domains because it doesn't even have definitions to build off on top of. For the places where the definitions are in, we actually are doing quite okay in terms of distribution diversity. We have good performance, you know, having solved open research questions in number theory, commutative algebra, algebraic, geometry, some discrete math that come into Rx and probability.

Is there is there like a weakness there in that specific domain? I would say so. For for OlympiA in math, people are seeing combinatorics being a little bit more tricky.

Seems like the steps are quite creative. So I I for I'm a human and, know, when I have friends who are really good at combinatorics, which I never consider myself really the the top of combinatorics. I'm kind of better at number theory, but I know some people who are just they're IMO gold, perfect score, Putnam Fettler, perfect score, and, like, all the way.

And then when they do, tricks in combinatorics, I'm like, I don't know how you thought of that. And but you know, after you give me that construction actually becomes a lot more trackable. I think a lean based system will struggle in those very creative places, which is why we at Acxiom actually also invest on something called mathematical discovery.

It is not used lean. And we have some major news in the coming weeks, basically open sourcing entire code bases of mathematical discovery coming up. You want to tell us a little bit?

Yeah, yeah, sure. So we are currently having two code bases being open sourced. The goal is for if you're a mathematician or you're 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 would suggest you follow the very detailed manual intended for mathematicians to run the code that we write. It's a tool for mathematicians to make mathematical discoveries. Mathematical discoveries is this idea that you know proof is not enough for math.

In fact before you kind of start proving something you don't know where you want to start. So you will try to construct some interesting examples. This can be usually say sequences, right?

If you want to understand the property of a sequence, you will write out a few of the first terms. This can also be graph. So if you want to, you know, figure out what the graph that you're looking for, should I have say a certain property, then you will start by doing some simpler version of the graph.

Now constructions cannot be done by a lean. So we believe in having AI for mass discovery and we have, you know, one of the OGs in that field Francois Charton, member of technical staff at Acxiom. And he previously have done pattern boost and end to end, you know, settle disprove a thirty year old conjecture by finding a counterexample, found the solution to a 130 year old problem, the globolempoena function that is a kind of mathematical object showing up in the three body problem.

So we are thinking that, you know, mathematical discovery tools should be open to the mass community. So we are open sourcing entire code bases for them. So discovery meaning it gives, it makes new conjectures or it That's a yeah.

It's a pre conjecturing step actually. Oh, see. Yeah.

So you start to form intuitions. Right? If you're a mathematician and your goal is to solve a really hard, hard conjecture, axi improver can't just solve it for you.

You might want to try to formulate some sort of lemmas conjectures that you want to say then give to axi improver. 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.

Now the code bases that we're gonna open source is gonna help you hopefully significantly.

you know, does is able to do some things. Yeah. So, I think like it's very clear that you just like there's theoretical result telling you, you cannot formally verify all programs, right?

But I think it's good to formally verify majority of the useful programs, right? So you know, like I remember there's this MIT, like little, like documentary or another documentary, like an advertisement for, you know, people who are admitted students. And then there's this famous line by Tame, the the beaver, the mascot of MIT saying that what does theory give you?

Which is which is kind of like it doesn't stop us from trying to push it as much as possible. Mhmm. Yeah.

So the goal that we have for the future is suppose you are, you know, doing the coding, you want to wipe code a really complex task. So, know, currently it's front end websites, but in the future we might want to wipe code much more complicated things, whole distributed systems even. Then we want to be able to say decompose it and there's maybe a high level kind of like sketch plan this we can make, other people can make.

But say you know you have Claude give you like you know kind of break it down into 10 things. And at one point, it will decide to call Acxiom. And Acxiom will give you a computer program that you know is formally verified or it will say this is still too hard for us.

So you you write the program? Yeah. You give it to Acxiom?

Yeah. It makes changes to it, maybe. So we're talking about kind of two sort of phases.

It is possible that we are the verification partner. So you already have a computer program and you want us to verify it. In fact, like, you know, GPT found a proof to an unsolved Erdos problem and our competitor Harmonic, you know, Aristotle, you know, verified it.

We we can do want to do verify generation. Right? Might want to say, hey, you know, this little component, everything that we generate and provide for you is is formally verified.

I see. So so the idea would be you you generate you co generate both.

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

Right. That's quite hard. You will likely, you know, break that down into multiple steps.

Mhmm. And then it will continue to break down these steps into more fine grained steps. Yeah.

And at one point, you want something that is absolutely correct. Yeah. And then this is also something that is likely within reach.

Then we want to generate, you know, both we want to generate a piece of computer program, and underlying is a guarantee that there is also the proof that has been generated, which tells you that the thing that you specify this, you know, program can solve for you. So so so the vision we have is anything that can be which anything is you know, it's a little bit marketing because as you said, the theoretical bound, but mostly, I'm assured you hopefully, anything that can be defined can be executed, anything that can be specified can be proven. So the way I think about it is if you have a program times a, you know, a program times a times a statement or problem, it maps to verifiability conditions times a proof.

So while the verification community has given you say the verifiability conditions, and we're trying to kind of recruit a really strong team to help us do that, Accident Prover is gonna give you the proof.

code verification benchmark that's supposed to be limb friendly. And so, you know, every problem is a coding problem. And the goal is to generate there's a code part and there's a proof part two different computer programs.

And then the goal is to generate code with proof. So you know, the code that supposedly solve this problem and then to prove that this program indeed does solve the problem. Now how do people do on this benchmark?

I kind of want to like talk about this a little bit because it's interesting. It was wrote out I think by Berkeley and Meta researchers in 2025 and they found I think whatever version of GPT they evaluated does like pass one like 3.6% iterative something like 22%.

Now, you know, how does the formal math systems models do? COBRA which is a system because in a system you iterate and define so PAS one doesn't quite work but still they evaluate it, pass one of the system about like, I think 11%, 12%. And then also Deepsea Prover and Godo Prover, very strong.

Prover model 11%, 12%. And I think our competitor has released last year on the only Proof part 96%. And we actually recently with no modification to the Punnam system, saw a 99% out of the 189 problems.

We solved 187. We missed only two code whizproof. So if you if you want to train something to do code with proof and you want to do reinforcement learning, it's actually quite annoying because look.

It's it's mixed. If you want proof to be informal math, it's it's very annoying because then that's like just mixed objective function. Your code is something like Python, prove it's a natural language, math proof.

You will not have very strong RL kind of performance. Right? But if you have proof as lean and you have, you know, code, you can choose Rust, which is a strongly typed language.

It's it's more conversion. So you're gonna have much better performance.

You will basically look at the coding problem and you look at the program and then you like try to see if it satisfies the verifiability conditions.

conditions and see if it does actually satisfy that. So so suppose suppose like we are looking at like, you know, a piece of computer program. Yeah.

Right. And then whether it does actually solve the coding problem, you will have a judgment about that. Right?

Yeah. So you will not solely rely on testing, even though that is the way. That's why So somebody looks at the proof and says, yeah, that actually solves the problem that we think it's supposed to be something.

But then but then now you're you're basically producing a, you know, formal verification program Yeah. That satisfy the verifiability conditions Yeah. About this program and the statement.

you know, the like specification. I think the word is gonna, know, even if we say successful, like anything that you know, we will have a specification problem. Yeah.

So like here comes a bank saying that like, please do I have a really safe financial audit? Sorry, like prove the financial audit for me. Right?

Yeah. Like, what does that mean? Like, we can't specify.

Humans are bad at specifying everything that we want. Right. There's always like some sort of saying that we are not specified.

And if it's not specified, it's not proven.

you know, like again, the the vision as of currently is anything that can be specified can be proven. Okay. Now, obviously there are people who have been really good at, you know, that's a weird maybe weird that's the informal kind of reasoner coming.

Right? The informal reasoner can and this is I want to kind of, you know, call the literature of testing, like testing are great because testing is like, hey, have you thought about that? Right?

Like, I want to highlight the work mutation based, you know, LM unit test generation by Accident CTO, Chubo, he was a director of Facebook AI research. Like the way you kind of think about it is like the AI will be like, hey, have you thought about this case? Like and so this is a little bit like So the conjecture is going to help with the specification.

so that when we're actually giving good speeches I think this is a future of coding. Yes. I think this is a future of coding.

And I think this is where, you know, as this is where I think even if we are supposed, like given the assumption that everything can be formally verified, you know, like studying sort of like, you know, automatic test generation is still interesting because it is basically giving you the specification proposal. Yeah. Right.

And then another thing is, let's talk about auto formalization, right, which is the ability to define it. It is kind of converting something that is informal into something that is more formal, the formalization. So suppose I have a coding problem that is written for ICPC and this problem is written in English like Alice and Bob blah blah blah.

Okay. Now I want to convert that into a formal statement, like a formal spec. How do I do the auto formalization step?

Right? Now this is going to be because I have not solved the problem So I don't have any signal. I don't have any grounding.

and then the but the proof is completely unproven. So lean is actually quite annoying because it's like a lot of the times it's proof. So you don't actually have the numerical answers to ground it.

So autophormalization is quite quite a hard thing to do. Because, you know, what's generally happened is you can't you just it's hard to ground the autophormalization of a statement. You can obviously ground the autophormalization of a proof, but because you can then just run it.

But you need human to eyeball it.

What what we believe fundamentally is we are building a reasoning engine. Mhmm. And we have seen action improver deal with really huge trees that are like, you know, tree of a proof.

Okay. We have seen it scale from 40 notes to 4,000 notes. So what sorry.

Axiomprover is the is the LLM? Axiomprover is an ensemble system of multiple Yeah. Models that we do post training.

I see. Okay. Yeah.

And also it also includes, obviously, the tools that Axle that we have Okay. Open released. Sorry.

Yeah. No worries. Yeah.

So so we have seen it being able to deal with more and more complex task. I see. We don't think it's partially bound.

You could ask, you know, is it bounded at one point on the pre trained base model? Yeah. I think that's a good question.

I think, you know, mid training could be very interesting because it does actually, you know, a lot of the sort of capability gain does come from that part, right? If you could argue that even if you try to reinforce and learn some person who is not very talented, that person might behave perform a lot less well than an on post trained Ramanujan. You can argue that way, very sad reality of things.

But so at one point we might consider doing that.

really the mathematical discovery renaissance has come, action prover does try to prove everything. You end up with like tens of thousand lines of limb proof. So first of all, it's auto informalization is a lot easier than auto formalization minus of no grounding, right?

So, you know, model has seen a lot of text and a lot of lean. So you can always, you know, convert that lean back into back into informal. And then there's the problem of, well, how do you know if you're correct or not?

You can rely on cyclic like consistency so you then formalize it again, like proof like program equivalence, something like that. So that's Oh, so you like informalize and then formalize and then make sure that you still Yeah, yeah. Like and although informalization is you know, obviously less hard a problem.

So you can always do that. So for a lot of the, you know, the link code that we output, we can have an informal summarizer of like big chunks of links. It's actually doing okay.

So, you know, that's the thing. And there's have another question of like, which I think is very interesting is I think there's a panel at ICML Vancouver last year at the AI for Mass Workshop. There's like Leo DeMora and Jeremy Aligod and Shubo and CTO was there.

And they were talking about like, will humans or mathematicians at some point stop trying to understand what's going on there? Because like, suppose you're a really ambitious mathematician. You're like, I want to prove free my hypothesis.

And bang, here's a limb proof. And like, it's actually correct. And it's just like, you know, problem 1,000,000 lines.

it goes with process as it gets messy. Was about to get there. Right?

It's like, well, will will that negative outcome happen? Was the question the panel was discussing. It's completely hypothetical.

No one's no one's like, you know, model system can prove Rheumatoid hypothesis. Right? So the disclaimer, please don't cut that part.

It's just standalone. But like, you know, will people still trying to understand what's going on? And I think the answer is usually is always yes.

I think curiosity and the desire to understand what is going on, you know, mathematically or in other domains as well, it's a basic human need. And I think that is like, I think a dose of optimism in an era of, I think verifier superintelligence, suppose we get there is that even if all the outputs are going to be produced and at a much faster pace and much more exponential volume compared to what humans could possibly consume, they're still going to try to consume it. And if they're still going to try to consume the ones that they deem important.

So then basically attention is the bottleneck. And if attention is the bottleneck, then really intuition and taste, you know, of which statement is probably worth the consumption of human and also maybe in a finite compute resource, worth the consumption, the sort of spending of compute resources. That's where human mathematicians' taste will always guide us.

And I think that's incredibly beautiful.

have you essentially thought about training your models to be elegant in some way? Yeah. At one point, we're gonna get to there because, know, I think the conjecture will probably depend on what what, you know, will probably depend on what we mean by taste, elegance.

Feels like an alignment problem to me. You know? Like, know, who who gets to say what is elegant?

Humans get to say what is elegant.

There's something about hard work, right? That what what you work on hard is what you're gonna be good at. Yeah.

Yeah. And we're gonna have a problem about that. I think like pretty much in a lot of the domains as well.

Right. Not just math. How do you be that senior programmer with, you know, really good high level understanding?

Well, guess full stack understanding high level and low level if you haven't spent the year of training.

maybe how the education system, the pipeline works, which is that if you do not show early signs of brilliance, you don't sometimes go through the process of pre training in math. Yeah. Yeah.

Right. Like so so that maybe you can argue that you don't need to say, you know, learn everything to develop a sense of taste. But there's like a threshold you kind of need to meet.

Yeah. So for example, you probably need to be able to code even if you don't need to understand assembly language. And that thing might transfer my intuition or, you know, my intuition might transfer from the Olympiad math problems into some other research areas and I tried to pursue and Komnatharas transfer is more direct, very similar and number theory could be further but still okay.

And then when it gets to like something that's a lot more different than Olympian mass transfer is that strong, but kind of like, you know, you need to diligent as you said, right? Like you need to diligently go through some amount of training. Yeah.

And if people over rely on strong AI, that doesn't happen. I wanna switch gears. Yeah.

In terms of kind of what we believe in, we believe the future of coding is going to be somewhat constrained by verification capability. And we believe in solving formal math is a very natural starting point. And then by extension, you can increase the verification capability across hardware and software.

And for hardware, for example, that's quite revolutionary. I mean, is, there is no, as we know, there's no partial credit for a mostly verified GPU.

It's all nothing. It is all or nothing. And you do need a perfect prover.

I want to stress that, which stress this point, which is that suppose I am a, you know, I'm someone who loves solving math. I think there are a lot of Twitter users who enjoy Pokemon like hunting or those problems. And then I just try to, you know, use a non deterministic OM like GPTSA, to try to get the full proof for that.

Yeah. Now I can do that many many times and 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.

So for those kinds of domains, I call like hardcore verification needed, it is a pain point. It is a current pain point. There are hundreds of humans and thousands of licenses being dedicated to solve one local grid problem verification.

project is like one to three, one to four. One to three, one to four. Correct.

Both in say, team size and then duration. Yeah. Right.

So if you multiply that. Yeah. Yeah.

Square. And then I think so so that's that's a I would say like, you know, it's a must cover. And now for the software verification, it is interesting right because you know as probably we all realize like my nephew wipe codes a lovable website.

There is absolutely no need to formally verify that piece of code. Like why would you? Now I heard a story from K Mads, actually that New York Times reporter who told me the story which is like, however, if you think about like, you know, in the time of agents, MyOpenClaw can probably do all sorts of things and probably can do some bad things.

Like MyOpenClaw can decide to like text something bad to my professor. Right? Like and and and you can say that perhaps is that 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 you don't need to rely on formal verification.

So you can have a lot of cases, but you can think about, know, maybe an enterprise that is dealing with a lot of regulatory kind of self using agents. They might want to do something like it's their choice. But I will argue that the improvement of verification capability, both in latency, you know, and inaccuracy, all these stuff, the performance holistically is going to determine whether people rely on formal verification or not.

Sure.

I think when it comes to faith, you either have it or you don't. So either dream the dream with us or you don't. And that's okay.

Because when we realize the dream, the company is gonna be worth 10,000,000,000. Yeah. So I think that's kind of the the feeling that I have, which is that we believe verification is the critical, 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 that I'm gonna say on the record, we do not believe that an informal mass system is going to be the mass AGI solution.

Yeah. So you can say that if you're doing Frontier Math and you have like sorry, sorry, Frontier Lab and you have like infinite resources, why does that there's this by definition no running out of gas. Right?

If you think like infinite means there's no running out of gas. I don't think it's going to scale to superintelligence. So you think that you run out like you run out of money basically, you run out of power.

Sure. Sure. We as a startup, first all, cannot do that.

We, first of all, as a startup cannot do that. Yeah. We generally think that formal math and by sort of converting math proof to programs to code give us much better performance.

If you really like, you can have a both informal and formal system. And that is going to be I see. I see.

Very strong. The thing that I kind of like, I think my my suspicion about like, you know, whether we can scale to mass AGI just by the informal approach is you're going to keep having, you know, the LMS judges solution or you have human experts who grade and they're just human experts like doesn't scale that well. And then if you really argue infinite infinity, then sure.

Then you also have infinite money and you can pay infinite. Is there there's so many is there really infinite number of people who can understand and prove at say like about like, you know, a result a natural result in Langlands program? I think, know, good luck finding those people.

And in fact, I think how Frontier Math came together is because they couldn't assemble a benchmark by their expert pool. So they have to, you know, collaborate with Epoch to do it. Right.

And I think that's kind of what I worry about about having the human part. So they have LMS judges and then now stochastic judging.

Basically, they are users of the system we are developing and that iteration loop is very fast. It is extremely fast. You have like some of the strongest, you know, mathematicians and both in research and Olympiad contests.

And you also have people who are, you know, mass lib contributors, maintainers, developers, lingers really, and combine them with people who come from like applied ML, really strong organizations like Meta Fair and Golden Age Affair, as well as people who have cogen expertise who work with like compilers like KernelGen have kind of these backgrounds of people together. I think that sort of interdisciplinary way of thinking about things quite helpful. We think AI for math has traditionally been quite interdisciplinary.

People are borrowing techniques from even AI for science, pure tech borrowing tech techniques from the cogen literature and people are borrowing techniques from obviously the broader, like, you know, frontier, like applied ML to try to apply on the niche problem AI for mass. So we also think having this sort of very special, special team is a differentiation. We also think that, you know, as you say, there's no permanent mode, the proprietary data that we generate and a little bit of a flywheel we are seeing is a time mode.

Well, me personally, I love math. I think, you know, I kind of have been doing math since I was very young and like math sometimes gets really hard when the problem you're solving are just a little bit out of reach and it gets a bit depressing. And times to times I wonder if I can just have an AI help me.

And and yeah, I think why I figured why not build such a thing. You did a master's at Oxford in neuroscience.

That's a great question. I think like my, you know, experience with neuroscience is you learn very well about what's hard and what's impossible. I mean, very interesting.

I think that year of neuroscience like give me some feelings about what's hard and almost no feeling about what might work. So but I think I was kind of under the pretense of neuroscience, hanging out at the UCL Gatsby Institute and was fortunate to do AI research with some really cool faculties. And so I think that was a very productive year of AI study and non neural study.

So you're it was mostly for you studying AI. That's right. That's right.

I think in The UK, if you back in the twentieth century, if you call something AI, you will not get the donation, but if you call something brain science, you might have a chance. So the UCL Gatsby, which is a premier AI hub where a lot of people actually go, you know, from their journey to DeepMind, including Demise himself. It's a very wonderful research environment.

I remember those kind of like tea time talks were very amazing and people were basically just doing It's called the Gatsby Computational Neuroscience Yeah. I think how that kind of you know happened was because so I in the Master of Neuroscience program and then quickly realized that you need to like kill rats and kind of don't want to do that. And computational neuroscience sounds more appealing.

And and when you look at the project and you see like transformer, you're like, you absolutely want to do that. Yeah.

you started a math PhD program at Stanford? I started actually one year full full time at the law school. Oh.

Because the JDPHD program is structured in a way where you have to spend full one full residency year. So that was also a very fun year of learning things that like are just quite fascinating, like criminal law, looking at homicide cases.

could access your a plans and improve? Question. I think for a lot of things, it's definitely underspecified.

For some other things, I was actually quite excited about sort of transfer learning from his medical reasoning to those specific fields. Think appellate litigations, legal gymnastics, you see some really good appellate scholars and lawyers that just come from mass training. Not many, but like Lawrence Tribe for one, Harvard Law professor, one of the strongest like appellate litigation and SCOTUS briefs like brains on the left, democratic party.

And I think there's a lot of other domains such as antitrust that's incredibly flowcharty, contract law sometimes also flowcharty, bankruptcy tax more on the corporate side. I just love litigation side. I mean, yeah.

the proof and then just formalized it. Yeah. So actually what happened was our competitor Harmonic decided to publicize that they have solved unsolved problems Erdosian number one hundred twenty four and four eighty one.

And then we trusted their literature review believing that these problems are really truly unsolved. And we were really young company at the time. We wanted to test if our system can attempt to try the problems that our competitor can.

We fully did not expect that actually solve them, but turns out that we were both wrong that in fact, the problem has been solved before. I see. So that's It's not the only time that we relied on others literature research and you know, we should own it.

The other time was this paper called Dead Ends in Square Free Walks, you know, professor Miller have this problem that actually turns out to have been solved. But we we I mean, we really should have done our part. That is that is, you know.

You know, there's this, like, Japanese, like, advertisement of, like, a whole company, like hundreds and thousands of people, like, apologizing in the in the advertisement. And it's like, you know, sorry, we raised our price by like 5¢. And that's the advertisement.

I was like thinking that maybe I should just do that.

claim they have solved Erdos problems that might not. I don't know. It's, you know, there's a I think Terence Tao and a lot of other people have a database about all the Erdos problems and the status.

I think, you know, like it is really, by the way, like it's a really easy mistake to make because there are so many Erdos problems that actually have been solved. Right. And I think that's kind of indeed, I think like, you know, search and retrieval is a hard problem.

Like you don't know if that argument or an equivalent version of that. In fact, think the most interesting part about that entire database is there are a lot of problems that are not directly solved, but can be just a very easy extension, almost a trivial extension of another result that has been solved or not sometimes not even resolved. Sometimes I think in this dead end square free walks case, which is nothing to do harmonic complete accident's fault that we actually didn't realize.

And then professor comments on the origin actually pointed to us and to professor Miller is that it was actually from a stack mass overflow or stack overflow post. Like a user pointed out that there is a nineteen thirty six results. It's fascinating.

component of any Okay. Any company. Yeah.

data in in some sense, but the the and and this may maybe is a competitive advantage for you. I think I think everyone is trying to accumulate like a data, which is not a mode, it's just time and time mode. Yeah.

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

This is a wonderful question. I think that's a very interesting approach, actually. Yeah.

I think we believe in something which is that like, you know, suppose axiom prover can be a really strong mathematician and then really the the thing that it is proving every day should hopefully help it improve. Right? I think this sort of self improvement design is extremely valuable.

And I think there are other people in the AI for mass community. I think Professor Gabriel Paresha's work is very interesting. I think there are some of the kind of more conjecturing type of exploration.

Suppose we just kind of change, you know, a lot of the there are specific things you can do in certain ways that can try to see if your system can learn to contracture and build theories.

trying to use

That was a great piece of work. There's also Mini f two f. These are all formal math work at OpenAI.

those guys are doing something? No. No.

They all left. Oh, they all left. See.

So that's my point, which is that if you are like, you know, an intern, I guess you can be an intern forever. So let's say you're like a junior, you know, like member of technical staff, and you want to work on something for like as long as it takes to solve it. Weirdly, people think about startup as this sort of your runway can just run out and they can just like all fall apart thing.

You might have a better chance of staying focused on the same problem for as long as it takes at say a startup like Acxiom or one of the other new labs. Yeah. If you're aligned to the Then mission of big tech.

Company rather than like somebody decided that what you're doing is no longer Yeah. Yeah. It can be your VP lost some political fight.

So yeah. Yeah. So No.

Obviously, if we succeed, then they're all gonna, you know, start doing that again. Yes. And then, like, I guess as a talent, then there are more like, you know, potential places to choose from as well.

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

especially at scale. So you wanna talk a little bit? Yeah.

Yeah. So we just released Axle, a x l e, stands for Acxiom Lean Engine. And it's really a set of kind of proof validation and manipulation tools that are built for Lean in the language of Lean.

So it's a bunch of meta programming tools. Now meta programming talents are extremely, I think like, you know, hard to find and we're so grateful to have like a really crack team working on that. And we want to kind of like release it to the community for to use for free because we think that there are probably other people doing also like large scale lane operations and these tools gonna make their stuff go a lot more robust and faster and do so at scale.

And Axle is currently I think 14 like such tools starting from verify proof, which is the sort of to make sure that there's not nothing weird, you know, going on, like no no sort of cheating by by link code. You don't axiom something out. You know, we don't we don't assume.

We're saying is if you axiom n plus n equals n, you can prove to prove two plus two equals two, which you're, you know, for sure not that's not a right answer. There are also like, you know, a lot of other kind of generation tools. For example, you can try like different repair attempts.

So, you know, broken lean in and then good lean out. And, you know, there are like currently, you know, other repair methods by LM. So hopefully this what we provide can be just a lot cheaper and more kind of, you know, straightforward.

And it's just, you know, I think strong strong and better engineering can can get you to to a place that's quite far. A lot of the people from the Ling community has been using Axle, if it's just been a week to do all sorts of different interesting things. We have seen people from the kind of blockchain community use it to to do interesting things in sector.

And we have seen also we have heard from a lot of the people that CLOUD plus Axle is kind of their go to setup for for now. We think that these are really interesting tools. Think famously, I think today there's this mathematician who said he formalized the Donald NUS, you know, using CLOD to prove, I think a result, a Ramsey result, and then to formalize the the the LIMPROOF.

And then that is also using Axo tool. So we are really glad to see people kind of already using it.

like myself, you might be able to participate in the, you know, sort of like an effort to prove a larger theorem or something like that. Yeah. I think that's that's very interesting, like, Ville, which is that, like, if you think about, like, mathematics has been not, like, as collaborative as software engineering.

You don't have, like, hundreds and thousands of people working on something together. I think Polymath was an instance when that happened, that was fantastic. So if you have a lot of really good sort of setup, indeed, like commoditized kind of access, then people can all participate in.

In fact, that's how I think some of the large formalization projects have been done. Things are divided into subtask. But really the blueprint writing process by, say, Terence Tao and Alex Kondorovich of assigning the task to different people and how things kind of fit together.

That blueprint writing part is extremely important. And there has been, I think, result about sphere packing, I think, by one of the other companies out there. And the blueprint part for the A dimension is still pretty much built on what the sphere packing community, the Ling community, the humans blueprint and similar with some of their other results as well.

The blueprint part has still been human generated. And I think auto generated blueprint is going to be a technical bottleneck that many people are trying to solve around the same time.

Depends are you trying to formalize or are you trying to prove?

Do actually have seen people use Lean and formalization and they try to do it by hand, you know, not using any AI as a way to learn mathematics. It's, all the formalization, Well, you don't have that it's interesting because I think a lot of the my friends who started, you know, working on Lean and MasLib was because they are in PhD and this problem is really hard. We get stuck all the time.

And we want to kind of review some of the undergrad classes, a time where we still understand what the math was about and we do so by, you know, doing lean. I think that's materials. Very Yeah.

But if you have, for example, like, you know, access to action improver that also can formalize all the formalized things, then you don't have you lose that part of the learning process. Yeah. Yeah.

But I do think that, you know, like for for for, you know, you and I, we can set up like Axle and try to like see, you know, what results we might be able to prove. And I think that's quite interesting. And thanks to Axle sort of making the speed a lot faster.

You don't have to wait very long. Yeah. I remember the exam day.

We were all like in the war room. It was a Saturday. We're all really excited and we just got the exam paper from the official, like organizing the proctor of the exam.

We just like, we're looking at like how much workout Axle is like getting. And without it, we couldn't have solved it with, I think the eight problems within the time limit that would definitely not not within the time limit. And I think the one thing about these tools is like, it's very interesting in that potentially you can have interesting reward for RL as well.

What do you mean by that? So for example, verify proof can be a reward for just basically a proof is completely correct and validate it. See.

I think formal verification tooling can be interesting direction to pursue with RL.

these formal tools, right? Like, and you will have some sort of score.

used what I just described. But you're saying just to learn how to do lean. So the value proposition which is interesting about FrontierLab is that suppose you are a to see business, then sure, you you can just not do what we are doing.

And we have since, for example, deep seek, alright, like originally having a formal team and then later dissolve that team because of strategic direction change. That's all completely reasonable. Now suppose you are 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, further your strength and moat. Yeah.

You can partner with Acxiom. Just like how, for example, Frontier Labs partner with startups that work on search such as Excel and Parallel. Just call it API for search and potentially, if you're a Frontier Lab, I think you should call Acxiom API for verification.

Better composition. It doesn't make sense. I mean, it's just, you know, potentially, I think the talent, finickiness of Lean, the sort of data code like, like, you know, there's there's no reason to.

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

I think, like, almost as soon as I started the PhD. I just started fundraising. So it wasn't like Oh, really?

Yeah. Was that the plan? Or did you did you start there and you're like almost immediately realized that this is Right.

Right. So the year of law school, right, was very, very interesting to me, like on an intellectual level. But it's also the first year where I had no science, technology or math whatsoever in my life.

It's a weird year, right? Like I'm reading a lot. I'm learning how to write.

I'm learning how to read like, and but like, I'm just kind of, I want to like be obsessed about something in technology. Like that was also what's going on that year. So yeah, the year of law school, right?

And it was very, interesting to me because it's like, okay, like I just I need to be obsessed with like a technical thing because otherwise I get to I don't think I'm bored because I really love like everything about about law. I really really loved it. It was it was something that's incredibly interesting to study.

But I just I mean, I've been basically like, you know, very excited about like the progress of reasoning. I was looking at a lot of the post training camp papers. I was I was learning all of these like just by myself.

And then at one point it got to a point where I'm like, I think this is for sure happening. And like I think talking to Shubo, right, at Verve like every weekend also like it didn't help like soothing this thought. So I got more and more obsessed.

And at a point I'm like, okay, if I'm doing this like literally every minute and I can't think about something else, what what you know, I need to do something about it. I mean, it's like you I I fall madly in love with the idea that AI is gonna do math. And like, now do I do I do math?

Like I it's really, really crazy. Like at a time where I remember the obsession was quite I just couldn't get out of it. And then I went to this Nighthansi event, Nighthansi Scholar Denninghouse like hosts all sorts of like free lunch events and those are great because you get free food and you get interesting intellectual exposure to things.

And I remember Julie Draw who was I think a Facebook first Facebook PM came to speak. And then after that, I just like basically walked up to her and I said like, what do you do if you want to do a start up and you really wanted to do academia because you kind of love math? And then she's like, well, you know, what's your time spent on these two different things?

And I'm like, a 1000%. And then she's like, well, you kind of have to follow your energy.

obsessed with it. Yeah. I was completely obsessed with it.

I thought it's gonna be big. Mhmm. And I thought like it it just it just has to be a for profit start up because like it's so much broader than making mathematical breakthroughs.

If you think about like recursive self improvement and like really the kind of more high level like concept of like, you really want to have just AI AI scientist. Like, the math reason is gonna be is gonna be a pretty big part of it. And now trying like, I think the the the sort of belief by by Cursor and Claw and other folks is like, okay, like, just like math transfer to coding, code coding transfer to math as well.

I think that's true. It's just that like, you know, why not push it directly? I don't get it.

You need to push that directly. And then there's this other like, you know, thought which is that, and maybe kind of going back to the collaboration point, right? Verification has traditionally been thought of as okay, well, there are some industry where there's lot of guardrails.

So if you're working in defense, military use, okay, you need to like basically satisfy a lot of barriers to entry to meet those stringent like requirements. So it's something that's verification is for the industries that are closed. But it's for the first time now, I think Verified AI is to open up collaboration.

Either it's human AI collaboration. Well, before Blueprint, that's human collaboration. And Lean was a grounding, was a verification formal language.

And then human AI collaboration like we're seeing now, future AI agent agent like collaboration. So like, I think verified AI is for openness. It's not for meeting the requirements of closed industries.

And I think just like I think verification should not be about, oh, I remember, like, you know, there's this article like chatbots mixed up of is AI the solution to sorry, it's math solution to hallucination. Verification to me is not about lousiness. Verification to me is about scaling brilliance, compounding brilliance.

It's like just kind of going back to the collaboration point. It's about Ramanujan being a much stronger mathematician. He was already a really strong one, but verification helps him extend the brilliance, like both kind of like scale up and scale out.

So verification rigorous. Verification to me is not about, you know, like erasing the mistakes, the lousiness, it's about scaling brilliance. And and the third point is that, like, verification to me is not about, like, the sort of, just talking about rigor.

It's actually about performance gain, right? It's not just about the stringent requirements, the hurdles that you need to overcome. It is about like actual verified generation is gonna make it so much better.

And I think like kind of these three points, I think the last point is that a lot of the people think that you work on verification because of your distrust for technology. Like it sells really well to I think the general public, including like my parents, oh, why we're doing verification because like, you know, technology make mistakes. It's no, we don't think verification is based on is because of the distrust for technology.

It's because that's what like expected rapid exponential scale up and the deployment and the creation of technology and technological progress is what that compels and demands. It's a very mathematical perspective, right? Because you're saying proofs are proofs are drive math.

Right? A lot of math is based is is about proofs. Yeah.

And math drives a lot of science and innovation in the world. And the innovations in math drive innovation in the world. So they But it doesn't need to even go through, like, in in terms of, you know, the solve math, solve everything thing, like, obviously stands.

Like, my point is like transfer learning doesn't like transfer learning is about like pushing math math reasoning. It just so so there are kind of, I guess, like, are a a couple narratives here. Like, for some people is that you you solve math and then math are the, you know, fundamentals of sciences.

So that's actually the from AI for math, like take this radical layer of AI for science is that narrative. We actually believe in just like general transfer learning. Like, think Acxiom is Acxiom is on the infrastructure stack.

Yes. I think it's so again, there are like, you know, multiple multiple kind of like beliefs. One belief is that there's math and there is like, you know, formal, the power of formal verification.

Suppose we actually, you know, solve math and have a really strong informal math reasoning engine. We do not expect that term to be as large as solving math through the formal way. Why?

I mean, as as it is language, but it is indeed on the more structured end. Yes. It bridges informal and formal.

Yes. What we are doing is it's not informal versus formal. We're not taking this sort of like completely formal of approved approach.

Like it's bridging between informal and formal. It is bridging between high level and low level. It is a direct sort of like a direct improvement through reasoning, so transfer learning.

And it's also indirect in that like, okay, well, like math is gonna unlock a little science and sure. And that is really what we're seeing. So you think that it enables transfer learning?

Yeah. I see. I think that is that is pretty much a consensus.

I think it is a consensus and there's a bet that has been pretty much kind of overlooked by others because math sounds pure and it doesn't sound like there's any commercial value. Well, I do obviously understand the opportunity like the opportunity cost if you're like a really like a frontier lab of of solving this problem. But I definitely think this is a problem that if you're like a well resourced startup, you should be doing.

That's an interesting Yeah. Perspective. Did you get everything else that you wanted say?

I think it's like, you know, like the question of like, is Acxiom math or is Acxiom verification? The DNA of the company is math. We think best verification is the best first market.

Yeah. And we think that sort of like solving math and especially like formal math is going to like help us like tackle the really ambitious quest of verified AI. Now, we're done with that, we might have other that second markets, including AI for science, we just talked about.

But on the theoretical layer, right? I think real world testing is important and potentially we can stay in the digital world and and soft software stuff and for other things to be to be to be getting real world like physical world signals.

you know, software verification and hardware or whatever. Yeah. But okay.

So now what about biology? What about chemistry? So that could be one.

The other one is then, like, really how far are you to recursive self improvement?

Yeah. I think there is this sort of question and different people because of their probably different backgrounds have different it's it's really where your energy and your passion leads you. Like for some people actually, I have heard this actually, you know, with my friends, they want to work on AGI because they believe soft AGI solve death.

There are other people who come from a more like medicine background. They really believe they can solve death and they don't solve AGI and then solve death. They just solve like AI for science.

Yeah. Now which way is correct? I don't know.

It's that combination that enables really good recursive I think recursive self improvement is going to happen anyways. We're trying to have like formal verification earns place. So we we like, again, the whether formal verification can be welcomed and deployed and become a consensus depends on how well we execute.

So I think we're in a market where people like to start like, you know, like a thousand people, they don't join forces, they start a thousand things. I think that's actually the biggest like kind of bubble indicator. I think there are a category called bubble and there are like other categories where there are moonshots.

It's not bubble, just looks a little bubbly. In the field, if people who are like really legit backgrounds decide to join force and work in the team for the mission rather than for ego, for kind of the status NeoLabs founder, I think that categories I'm really bullish other and vice versa. So I think the bottleneck actually is about potentially I think I think it's it's it's annoying because it's like we are in a if if you believe we are in an age of research, if you believe in like deep tax are the interesting directions to go after.

The market sort of conditions currently is good and bad and that good, it enables these sort of long term long horizon bets to be funded, bad because there's too much noise in the market and some other like irrational players. We try to work with really incredible venture firms like they are the partners, they are our intellectual partners and there's a lot of alignment and we really bounce like very cool ideas, technical and non technical each other, for long hours. And we spend like a lot of time off work and weekend together to really intensely build the company.

But there are also other people who just want to like park like capital somewhere. And, you know, while we don't work with them, these encourage these are market conditions that encourage fragmentation. And when things get fragmented, like no one gets there.

Like, I think every category, regardless of how right the idea is, is pretty much in a sort of earning the right to exist stage. And if that is the case, for example, great deep tech company SpaceX and people do actually join force to work on that dream and potentially in that case, a very charismatic founder. I think a really kind of concerning thing for me personally, that for other, probably some categories that I'm personally quite bullish about their action about and just like looking at things generally, fragmentation is a problem.

like, AI landscape. Okay. Yeah.

I think AI for math is a category that is actually not a bubble because it is not fragmented. Because people who are really amazing talents do like to join force. So for example, the fact to get Ken Ono and Francois Charton on one team, like this is fantastic.

Like you have someone who's a core contributor frontier math tier four, really great benchmark setter, Francois who's on the AI for math discovery, have proven and discovery. They work together. Then you are suddenly a player with both proving capability and construction capability.

And that's fantastic. And I believe, you know, as you said, like Harmonic probably also have some really great talents like joining forces together. I think AI for mass is a good category because of the absence of fragmentation.

But even, you know, from our perspective, the sort of, for example, you know, RL right being, I don't think that's like a category per se, but, you know, RL talents currently, it's quite hard to attract and retain, right, for for literally everyone. And there are a lot of companies being started and then sold like three months later. And and just the the each month where you could have worked on like a technical problem and you're instead working on deals, it's a month that is wasted.

Where is it going? What is the thing that everyone just really wants to break? I expect fragmentation to start to happen as Acxiom and Harmonic establish category leadership.

Mhmm. So I expect people kind of, you know, that's one thing. But I also think that another bottleneck could be the pressure of short term versus long term.

I think that we are doing things in a very sort of fast paced manner. But that does not mean we can always or it does not mean it is always correct to do things in the most fast paced manner. Like we did things in a fast paced manner because while we were founded on the day of the International Mass Olympiad, so we couldn't have competed in that anyway.

The next Mass Olympiad is Putnam. And we're quite excited because it's I mean, it's undergraduate exam. And this year's IMO 2025 IMO was easy on the MOHS scale, and PUNDAM could be hard.

And in fact, it was harder than the IMO and the MOHS scale. If you look at AI, you know, how much how many scores the AI has has retained on average and on the max, you know, difficulty of the problem. PUNDAM is harder in both both axis.

So we want to try. And so there's only a gap of four months, but it doesn't mean I'm always gonna set four months goals. If I build a company only setting four months goals, I might build a really shortsighted company.

So there are like, I think longer horizon problem. I think, for example, market forces could force other players into trip verification. Well, it is possible that co verification, it's a holy grail.

It's possible that if you solve that, then you also naturally solve chip verification with some amount of like Epsilon caveat of like distribution shift. But I strongly believe that like a bottleneck like could be the pressure. But I think the Axiom is fortunate that one, we are early enough to we are like a team of just incredibly, like, high agency people that our execution generally surpasses expectation.

But I think, like, what I think could be a bottleneck for the entire Aframas field is that potentially trying to prove commercial value is going to distract significantly from the core capability improvement.