🔬Scaling Past Informal AI - Carina Hong, Axiom Math

Summary

Latent Space: The AI Engineer Podcast

Episode: 🔬Scaling Past Informal AI - Carina Hong, Axiom Math

Date: June 3, 2026
Guests: Carina Hong (CEO, Axiom Math)
Hosts: Brandon Anderson (Atomic AI), RJ Honicke (Mirromics)

---

Episode Overview

In this episode, the hosts sit down with Carina Hong, CEO and founder of Axiom Math, fresh off a $200 million Series A at a $1.6 billion valuation. The conversation dives into the frontier of AI-driven mathematical reasoning and formal verification, the evolving AI-for-math landscape, and the much broader implications for code, science, and the foundations of "Verified AI." Carina explores why formal verification is not just a compliance tool, but a driver for scaling human/AIn collaboration and "compounding brilliance," as well as what differentiates Axiom’s approach, its team, open-source initiatives, and vision for the future of superintelligent, verified AI.

---

Key Discussion Points & Insights

1. The Vision Behind Verified AI

• Verified AI as Openness, Not Compliance

  • Carina challenges the view that verification is about “tax and compliance,” arguing it should be about scaling “brilliance” and enabling mass collaboration.
  • Quote [00:00]: “Verified AI is for openness. It's not for meeting the requirements of closed industries… Verification to me is about scaling brilliance, compounding brilliance… It’s about Ramanujan being a much stronger mathematician… verification helps him extend the brilliance.”

• Formal Verification Moves Beyond Safety

  • While formal verification has origins in safety-critical systems (e.g. Paris train unions, ESA, Boeing), now it's about unlocking new AI capabilities, not just preventing errors.

2. Axiom Math's Milestones and Business Case

• Impressive Funding and Achievements

  • $200M Series A at $1.6B valuation, positioning the company alongside the annual US math research budget.
  • Achievements: perfect score on the 2025 Putnam, first AI to prove (and discover) research conjectures with formal verification.

• Why Formal Math (and Lean) is the Best Beachhead

  • Carina describes Lean—a programming and proof assistant language—as both practical (helping with low-level calculations) and symbolic (community standards for rigor).
  • The DNA of Axiom is math, but Carina views formal math and Lean as an ideal first market for verified AI systems, due to their structured data, transfer learning potential, and proof of horizontal scaling.

3. Formal Verification vs. Informal Methods

• Efficiency and Sample Gains

  • Carina explains that verified generation is not just about avoiding hallucination—it's about higher performance, efficiency, and unlocking superhuman capabilities even with smaller data/compute budgets.
  • Quote [14:05]: “For us, verified generation means performance gain… a startup like us… with less compute budget… will be able to match and even exceed… performance on superhuman tasks.”

• Comparisons to Frontier Labs

  • Most labs post-train LLMs on informal, preference-based math data; Axiom uses Lean proofs for data integrity and compositional reasoning, recursively decomposing proof goals and learning to backtrack.

• Limitations & Open Questions

  • Distributional shift: Transfer across mathematical domains depends on the availability of foundational "infrastructure" (as in mathlib for algebra, less so for analysis/topology).
  • Combinatorics remains a hard area (“very creative … Lean-based systems will struggle in those creative places”).

4. Open Sourcing Mathematical Discovery

• Supporting Human and AI Collaboration

  • Axiom announces open sourcing two codebases for mathematical discovery—aimed at helping researchers experiment and find constructions as a precursor to proving conjectures.

• Discovery Precedes Proof

  • “Mathematical discoveries is this idea that proof is not enough for math…Before you, kind of, start proving something, you don't know where you want to start… Now, construction cannot be done by Lean. So we believe in having AI for math discovery.” [20:45]

5. Technical Deep Dives: Lean, Verification, and Limitations

• What is Lean?

  • Lean is a functional programming language and proof assistant for writing formal proofs; based on Curry-Howard correspondence (proofs as programs).
  • It serves both as a verification framework and programming tool.

• Verification Bottlenecks

  • Rice’s Theorem and Practicality: You cannot verify all programs, but can target most useful/needed programs.
  • Specification Problem: Formal verification is only as strong as the initial specification—which is notoriously hard for humans to provide comprehensively.
  • Auto-formalization (translating English/informal specs into formal Lean) remains an unsolved challenge.
  • Scaling Law Unknowns: No clear answer yet on how Lean proof size scales with program size, though sometimes one line of code needs 20 lines of proof.

6. Verified AI in Practice

• Hardware and Software as Business Markets

  • Chip (ASIC/GPU) verification is all-or-nothing: current industry spends massive resources on formal methods—ripe for disruption.
  • Software verification: Not all code needs it, but as agentic AI rolls out, higher assurances will be needed in regulatory or mission-critical domains.
  • “No Partial Credit for a Mostly Verified GPU. It's all or nothing…and you do need a perfect prover.” [46:10]

• Partnerships, APIs, and Ecosystem

  • Launched Axle (Axiom Lean Engine): API/tools for proof validation/manipulation, open to the community.
  • Tools support Lean operations at scale; integrate with Claude for convenient coding/proving workflows.

7. Team, Talent & Competitive Moats

• Axiom’s Unique Team Structure

  • Team integrates math Olympiad medalists, mathlib contributors, applied ML experts, and compiler engineers.
  • Proprietary Lean proof datasets can offer temporary advantage, but execution speed/quality drive long-term moats.

• The Importance of Focus

  • Carina argues that startups (vs. big labs) can maintain singular focus until true breakthroughs—less exposure to shifting priorities.

8. Philosophical & Strategic Reflections

• Why Not Just RL/Informal LLMs?

  • Formal approaches are orders of magnitude more sample efficient, scalable, and compositional.
  • Human expert judgment doesn’t scale; even with infinite resources, infinite qualified reviewers don’t exist.

• Elegant Proofs, Taste, and Human-AI Synergy

  • Future includes training models for elegance or taste (an “alignment problem”—what’s elegant is a human preference).
  • Stakes: Without engagement in proof and formalization, mathematicians or programmers could lose fundamental skills or intuition.
  • Collaboration: Common formal toolchains could induce a math “renaissance” similar to open software.

• Recursive Self-Improvement and Transfer Learning

  • Formal math, formal verification is foundational for recursive self-improvement in AI and thus pathways to AGI.
  • Transfer learning is more viable from formal approaches; solving math is a springboard for science, law, and beyond.

9. Challenges and Industry Bottlenecks

• Fragmentation vs. Teamwork

  • Market-wide: Large-scale progress is hamstrung by fragmentation—too many founder-driven micro-startups competing instead of combining forces.
  • However, in AI for Math, leading teams are consolidating top talent (Axiom, Harmonic), which could create non-bubbly, robust paradigms.

• Short-term vs. Long-term Prioritization

  • Commercial pressure to prove value can distract from core, long-horizon capability development.

---

Notable Quotes & Moments by Timestamp

• “[Verified AI] is about scaling brilliance… It’s about Ramanujan being a much stronger mathematician… verification helps him extend the brilliance.” (Carina, [00:00])

• “$200 million… one of your colleagues said… basically the entire US MA budget for math research each year.” (Brandon, [01:29])

• “If you have more structured and form data, it's going to be a lot more horizontal than the specific vertical we are tackling.” (Carina, [03:17])

• “For us, verified generation means performance gain… a startup like us… with less compute budget… will be able to match and even exceed… performance on superhuman tasks.” (Carina, [14:05])

• "What does theory give you? … it doesn’t stop us from trying to push it as much as possible.” (Carina, [23:53])

• “I think curiosity and the desire to understand what is going on… mathematically or in other domains as well. It's a basic human need. … even if all the outputs are going to be produced… at a much faster pace… they're still going to try to consume it.” (Carina, [41:01])

• “We believe the future of coding is going to be somewhat constrained by verification capability.” (Carina, [46:10])

• “If you are completely obsessed with it…” “Yeah, I was completely obsessed with it. I thought it's going to be big. And I thought like, it just, it just has to be [a] for-profit startup because… reasoning is going to be a pretty big part of [AI scientists].” (Carina, [78:02])

• “We do not believe that an informal math system is going to be the math AGI solution.” (Carina, [50:50])

---

Timestamps for Important Segments

• [00:00] – Carina on philosophy of verified AI (openness, not limitation)
• [01:27] – Milestones and funding context
• [10:52] – What is Lean? Explanation for non-experts
• [13:23] – Total addressable market: “TAM is all code”
• [14:05] – Verified generation as a performance gain
• [16:07] – Axiom’s technical pipeline, lean data, model structure
• [20:47] – Open-sourcing mathematical discovery codebases
• [23:53] – Rice’s theorem and limits of formal verification
• [25:53] – Code/proof co-generation, real-world benchmarks
• [41:01] – Human desire to understand proofs, impact on discovery
• [46:10] – Why hardware/software verification markets matter
• [62:16] – Provenance, search, and problem duplication in math
• [66:57] – Axle: API and open-source infrastructure for Lean verification
• [69:59] – Math as collaborative enterprise, blueprinting, auto-formalization
• [78:02] – Carina’s personal motivation and founder story
• [86:06] – Fragmentation as bottleneck for the field
• [90:30] – Bottlenecks specific to AI for Math community (urgency vs. depth)

---

Summary Flow

1. Introduction & Funding:
   Carina’s vision for “verified AI,” stunning $200M funding, Axiom’s math/tech milestones.

2. Formal Verification Philosophy:
   Moving verification from “tax/compliance” to “superintelligence/compounding brilliance.”

3. Technical Foundations & Lean:
   Why Lean and formal proof assistants are central to Axiom’s approach and the limits compared to informal LLM methods.

4. Discovery, Proof, and Tools:
   Supporting human and AI mathematical discovery, open source, and the “TAM of all code.”

5. Practical Markets and APIs:
   Business case for hardware/software, partnerships, and the launch of Axle.

6. Talent, Culture, and Bottlenecks:
   Team makeup, market fragmentation, execution speed, and the field’s need for collaborative focus.

7. Big Picture:
   Formal reasoning’s centrality to AI, automation, and recursive self-improvement; the drive toward a collaborative mathematical and scientific future.

---

For those who missed the episode: This conversation is a deep exploration of the rising role of formal verification in AI, with specific emphasis on how Axiom Math is using Lean to push the boundaries of what AI (and human/AI teams) can achieve in math, code, and beyond. It links philosophical perspectives, technical advances, funding realities, and organizational culture together—a must-listen for engineers, researchers, and founders at the intersection of AI, mathematics, and verification.

Transcript

[Karina Hong]

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. 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 makes up of is math solution to listen. 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.

[Brandon Anderson]

Welcome to the Latent Space AR for Science podcast. I'm Brandon Anderson. I build RNA therapeutics at Atomic AI. And I'm joined by RJ Honicke, the CTO of Mirromics, working on spatial transcriptomics. It's a pleasure to. Karina Hong, CEO and founder of Axiom Math. Axiom has made a splash in several different areas. First, they got a perfect score on the Putnam last December. I think they also have the claim of the first AI to prove research conjectures using formal verification. And very exciting. They just yesterday announced quite a large Series A. Yeah. Welcome to the show.

[Karina Hong]

Thank you for having me.

[Brandon Anderson]

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

[Karina Hong]

Is that true?

[Brandon Anderson]

Actually, According to his LinkedIn post, yeah.

[Karina Hong]

Okay. Wow.

[Brandon Anderson]

250 million is our apparently annual math budget.

[Karina Hong]

You think we should spend more on math research?

[Brandon Anderson]

Yeah, it's kind of sad.

[Karina Hong]

Yeah, I know.

[Brandon Anderson]

But anyway, like, you know, as a, you know, as a nerd who loves math, that's like, really cool. But I mean, I'm just like. That kind of blew my mind. Like, what? Like when I heard that, like. Okay, so, like. Yeah, how is it? 200. 200 million? I guess. 1.6 billion valuation. Yeah. I don't know.

[Karina Hong]

Yeah, well, super, super excited to be here also, I think, like, you know, this is a Series A, so it's very, very interesting. Timely, timely podcast. We're like a seven, eight months old company, so it definitely means a 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 we need to, to 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 Axiom well as us as a mass startup, so mass 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 fundraiser is going to let us explore some of the applied domains. As my colleague CTO Shubho said in the little launch video of the Series A we had is it lets us broaden our dreams.

[Brandon Anderson]

So yeah, but still like $200 million and I guess a 1.6 billion valuation. How is there a market for that? I mean like, obviously you're not doing this just for the fun of proving things, although I'm sure there's a lot of that.

[Karina Hong]

So let's bring us back to 2024. So when you know, 01 reasoning models like just came out, what was anthropic kind of like secretly working on back then? It was coding and everyone knows they're working on coding, like OpenAI meta accent. Everyone has full knowledge that anthropic working on coding and they just like overlooked it. They thought, oh, they are at B2B plays. They just want one vertical. People 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, you know, a monopoly in the, in the future of reasoning. And I think that's, that's really, really shocking. The people who are working on coding, I think back then believe in something that we believe, you know, similarly with math and Lean now, which is that if you have more structured and form data, it's going to be a lot more horizontal than the specific vertical we are 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 you know, while we are pursuing math, we're also doing things that do have transfer learning to other, to other domains. Um, so I think that's kind of like the broader, 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 are seeing on a batch of research conjectures. In fact, we have another batch coming. We are also thinking that this is going to be fundamental to verified reasoning. And we kind of talk a little bit about verified AI. I want to talk a little bit about verified AI next because I think you have another.

[RJ Honicke]

Yeah, yeah, yeah. I have a several things I want like, so I want to hear about the verified AI. I do want to dig in a little bit. So do we know that, you know, anthropic and OpenAI and everyone, they're not doing formal verification and using that for their rollouts and whatever.

[Karina Hong]

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. But 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 lots of 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 and 35 in 2025. Because there's only one component Rx question in 2025 after Alpha Proof. Kind of like we didn't see a lot of the formal math, you know, results or kind of progress from Google DeepMind. And that's actually because of reasons that are not necessarily technical. But if you're at a startup and you have 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.

[RJ Honicke]

So yeah, just define that for us.

[Karina Hong]

Yeah, like a lot of people think about formal verification as an ancient, you know, subject. It existed like as long as, you know, way before like, like deep learning. And it existed in the time of rule based computer science. There's this really strong push of like formal verification around like since ever, since 19 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 technology and 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. I think there's a lot of push about automated reasoning at AWS because they have a lot of enterprise as customers that really requires things to be, to 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 annoying because it's tax and compliance, it's making sure that we are good to go. That's really not. And so we talked about verification. I think our competitor, when they launched, they talk about formal verification and 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, for us verified AI is about the brilliance. It's about scaling and compounding super intelligence. So this is quite a deep point and sometimes it takes a little bit of explanation. So if you think about the place of brilliance, for example Ramanujan, he's a brilliant mathematician. He was able to find a lot of interesting formulas just by intuition before he know how to do proofs. So he went to Cambridge, you know, worked 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 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 countries 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 out casted by your mass community like well, rules in the community. So, 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 a paper currently takes two years. Okay, so but proof assistant and you know, formal proof checkers like Lean still found its place. Right. And why like if you, if I'm a mathematician and you know any like my work can be peer reviewed by other humans. Like why do we even, why do Mathematic even play with Lean? Right? And why do we even talk about kind of like, you know, Lean based assisted like serum proving? It's because like it handles a low level. For example, we're not even talking about AI, we're talking about for example, a 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.

[Brandon Anderson]

Can you explain what Lean is to non experts?

[Karina Hong]

Okay, yeah, I think our order is like a little wrong. Yeah. So Lean is a computer program, a bit like for mass proofs. It is a formal language just like its cousin Isabel Coq or Rock and some other further cousins like Daphne Agda, like these formal languages, whole, etc.

[RJ Honicke]

And what does it do?

[Karina Hong]

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

[RJ Honicke]

So it's like a type checker.

[Karina Hong]

Yeah. That is based on this result called Carl 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. It's because on one hand, if you don't care about the formal part at all, if you don't care about the logic part, you just want to use Lean to write code. You 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.

[RJ Honicke]

So it's a trained complete language.

[Karina Hong]

That's right. So you can write, you can do a lot of things with Lean. It's a functional programming language. Right. And then you can also use it to. So you use it to do coding, you can use it to do math. Two in one.

[RJ Honicke]

Okay.

[Karina Hong]

And kind of going back to what I was kind of getting at, if mathematicians are already enforcing that most proofs, say maybe not all mathematicians, but the Ivory Tower, people in academia, all proofs are correct. Why do we even need Lean, the model tracker? 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.

[RJ Honicke]

I actually, Terence Tao has a great video also about using Lean as a way you can collaborate because you can use.

[Karina Hong]

Exactly. That's another point I want to talk about. Right. A lot of people think about, you know, 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 tam. The TAM is all code. The TAM is a right of first refusal on all AI generated code. Like right of first refusal, meaning you know, 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.

[RJ Honicke]

Up until now it has been yes,

[Karina Hong]

yes, and, 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 Frontier Lab will be able to match and even exceed, you know, performance on superhuman tasks. In fact, for the Panem exam that we just competed December 2025, which we did in real time, Mass arena, which is this organization that evaluates a lot of LLMs, found the best LLM, Deepseek got 103 points out of a 120 point exam. The best human, obviously we now know is a student from either MIT or Chicago, we don't know which because they don't announce the top five winner score got 1110 and we got 120. So it's the first time actually. I remember when we were starting this, we were like, is it even possible that a formal math system with so much orders of magnitude last data can match or beat an informal LLM? And PANDEM is the first time it beat. Right. And so we are not thinking about it, just about the painfulness, the challenges it poses. We are thinking about the verified generation performance gain gain, the improvement, the fact that you can, you know, just like you would expect RL for Lean to, to have improvement because of seeing evidence of RL encoding. So this is the second point I want to make about like how to think about verification verified AI.

[RJ Honicke]

So maybe we can talk a little bit about why can you describe what, what is different about what you do versus what the Frontier Labs, you know, at least when they're building your standard RL enhanced LLMs. What, what's different about what you do?

[Karina Hong]

Yeah. So we heavily rely on kind of data called lean data and we kind of talked about Lean is all the, 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, quite important. So you know, we have a system of models. These models are post trained and using RL or sft.

[RJ Honicke]

So LLM found like some sort of foundation model that you get off the shelf and you post train it or, or con. Continuous.

[Karina Hong]

Yeah. And there's obviously an inclination for open source, you know, based models.

[RJ Honicke]

Does speak English, probably knows how to code.

[Karina Hong]

Yeah.

[RJ Honicke]

But also you fine tune it or, or continue.

[Karina Hong]

Yeah. And the base model might be similar to what everyone else using as well. Right. If they're not kind of pre training their model.

[RJ Honicke]

Right, yeah.

[Karina Hong]

And then we basically do this RL for formal math kind of there's I think a standard pipeline or like 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 wall recursively decomposing a proof goal into many sub goals and then learning to backtrack as well.

[Brandon Anderson]

Well, is there a risk that like you start out with this, you know what, you know, in a certain domain of data sets and so on and then you start rolling out, you know, recursively in a space. But now all of your training data is localized in some domain that you. It still is only so like maybe logarithmically in some large space growing from your initial training data. So you could get trapped essentially in that. You know, you could be really good at this. But you just created a big jagged frontier where some other domains or just

[Karina Hong]

far from them distribution shift are we talking about. So yeah, so you know, it is an open question whether a system that can do really well in number theory can do well in. Give me, you know, another. Another field of math. Yeah, exactly. Well, actually I think this, the way we think about it is it depends, it depends on whether topology has a lot of the existing definitions as almost like, you know, the mass infrastructure existing. Because what people have found in the past is when people building out math lib like you know, for the algebra, you know, book work like they, they can just.

[RJ Honicke]

So mathlib being the Lean like undergraduate library. So it's like all the proofs that you learn in undergraduate math.

[Karina Hong]

Yeah.

[RJ Honicke]

And they're all sort of in Lean.

[Karina Hong]

Yeah. So for example, some of my friends who currently are Axiom is you know, crazy like full circle back moment. Kenny, we're like friends for like 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 Mass. A lot easier to codify algebra in mathlib than for analysis. So that's interesting because for analysis a lot of the definitions around convergence, limits, et cetera becomes tricky. And so I don't think there's a lot of topology in mathlib today in terms of differential topology, differential geometry kind of stuff. So our system likely will not do very well on those domains because it doesn't even have the 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 having solved open research questions in number theory, commutative algebra, algebraic geometry, some discrete math that come into our exam probability.

[Brandon Anderson]

So earlier you said that with the Putnam exam, the 2024 version, when all of the questions that were not not that alpha proof did not get right.

[Karina Hong]

The IMO International ap.

[Brandon Anderson]

Yes, for the imo all of the ones I got wrong were in combinatorics. Is there, is there like a weakness there in that specific domain?

[Karina Hong]

I would say so for Olympia in math people are seeing combinatorics being a little bit more tricky. Seems like the steps are quite creative. So I'm a human and you know, when I have 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 fellow perfect score and like all the way. And then when they do like tricks and 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 Axiom actually also invest on something called mathematical discovery. It is not use Lean. And we have some major news in the coming weeks. Basically open sourcing Entire code bases of mathematical discovery coming up.

[RJ Honicke]

You want to tell us a little bit?

[Karina Hong]

Yeah, yeah, sure. So we are currently having two code bases being open source. 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 supposed 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 proof is not, 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. These can be usually say sequences. 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 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 construction cannot be done by Lean. So we believe in having AI for mass discovery. And we have one of the OGs in that field, Francois Charton, member of technical staff at Axiom and he previously have done patent boost and end to end disprove a 30 year old conjecture by finding a counterexample. Found the solution to a 130-year-old problem, the global Lebanel function. That is a kind of mathematical object showing up in the three body problem. So we are thinking that it's mathematical discovery tools should be open to the mass community. So we are open sourcing entire code bases for them.

[RJ Honicke]

So discovery meaning it gives, it makes new conjectures or it.

[Karina Hong]

That's a. Yeah, it's a pre conjecturing step actually.

[RJ Honicke]

Okay. Oh, I see.

[Karina Hong]

Yeah. So you, you start to form intuitions, right? If you're a mathematician and your goal is to solve a really hard, hard conjecture action prover 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 axiom prover. 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 base is that we're going to open source going to help you hopefully significantly.

[RJ Honicke]

So one thing that maybe there's a lot of computer scientists listening and one of the things that will immediately kind of come up, especially when you're talking about formal verification and so forth is Rice's theorem and decidability and incompleteness theorem and, and maybe some arguments about computational complexity and LLMs. So I, I'm curious to hear Rice's theorem says you cannot prove non trivial things about programs for all programs.

[Brandon Anderson]

Right.

[RJ Honicke]

So how, how are you navigating this space? Obviously formal verification, you know, know does is able to do some things.

[Karina Hong]

Yeah. So yeah, I think like it's, it's very clear that you just like there's theoretical result telling you you cannot formally verify all programs. Right. But you, you, I think it, 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 not a documentary, like an advertisement for you know, people who are admitted students. And then there's this famous line by T, the mascot of MIT saying that what does theory give you? Which is kind of like it doesn't stop us from trying to push it as much as possible. So the goal that we have for the future is suppose you are doing the coding, you want to wipe code, a really complex task. So 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 Axiom and Axiom will give you a computer program that you know is formally verified or it will say this is still too hard for us.

[RJ Honicke]

So you, you write the program.

[Karina Hong]

Yeah.

[RJ Honicke]

You give it to Axiom, it makes changes to it.

[Karina Hong]

Maybe so, so we're talking about kind of two sort of faces. 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. But we can do, we want to do verify generation. Right. We might want to say hey, you know, this little component, everything that we generate and provide for you is formally very of it.

[RJ Honicke]

I see. So, so the idea would be you, you generate, you co generate both and so that, and I can imagine this fitting into, you know, the idea of a promise or a sorry, sorry and then a sorry, sorry, sorry meaning it's a Lemma that is unproven, but you're just taking it as given until you can take have the time to prove it. Right. Is that a good way to think about a sort of.

[Karina Hong]

Sorry, that is a good way to think about a story, but not necessarily in the coding context.

[RJ Honicke]

It's so I can imagine you're, you can say, assuming that this module is verified, then this module is correct and, and so that. That you can decompose a problem small enough that you can verify. Is this kind of intuition here?

[Karina Hong]

So, so let's say we want to, you know, like wipe code, control flows. Yeah, right. That's quite hard. You will likely, you know, break that down into multiple steps and then it will continue to break down these steps into more fine grained steps. And at one point you want something that is absolutely correct 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. An underlying is a gern that there is also the proof that has been generated which tells you that the thing that you specify this program can solve for you. So the vision we have is anything that can be. Which anything is a little bit marketing because as you said, the theoretical bound, but mostly, well, almost surely, 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 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 programming program 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. Action Prover is going to give you the proof.

[RJ Honicke]

So just help me map from the program to the proof because like I could say, you know, this two line lean program verifies, you know, sort of like whatever, whatever I claim it solves. How do I know that it actually verifies the thing that I think it.

[Karina Hong]

Yeah, so. So for example, there is this. Currently there's this benchmark called, called Marina. It's a code verification benchmark that's supposed to be limb friendly. And so you know, every problem is a co 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 solved this problem and then the proof that this program indeed does solve the problem. I see now, 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 copra, which is a system because in a system you iterate and define so path one doesn't quite work, but still they evaluate it pass one of the system about like I think 11 12% and then also deep seq prover and Godot prover, very strong Prover model. 11 12%. And I think our competitor has released last year the only proof part, 96%. And we actually recently, with no modification to the pandemic system, we saw a 99% out of the 189 problems we solved187, we missed only two codewhis proof. So if you want to train something to do codewist proof and you want to do reinforcement learning, it's actually quite annoying because look, it's mixed. If you want proof to be informal math, it's very annoying because then that's like just makes objective function. Your code is something like Python. Your proof is 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 code, you can choose Rust, which is a strongly typed language, it's more convergent, so you're going to have much better performance.

[RJ Honicke]

I can't wrap my head around how do I tie. So I like, I can say that this proof solves Fermat's last theorem, right? Yeah, I don't know that. Like, yeah, but it's two lines in Lean. Obviously it doesn't. So how do I know that the program that I wrote matches the proof that I generated?

[Karina Hong]

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

[RJ Honicke]

But like, how do I know, right? Like if I read it right, you know, like I can, I can like eyeball it and I can say. And then like traditionally, how mathematicians have done this is they, they, you know, they take the paper and they read it and they say, I agree that this proof solves the problem. And then this other person says, no way, it doesn't for, you know, like look at this. And then people disagree and eventually there's consensus that that like this Proof solves this problem. Yeah. So like how do, how are you.

[Karina Hong]

But you check it step by step, right?

[RJ Honicke]

Yeah, right.

[Brandon Anderson]

Right.

[Karina Hong]

Yeah, yeah. So you basically will look at the verifiability conditions and see if it does actually satisfy that. So, so suppose, suppose like we're 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?

[RJ Honicke]

Yeah.

[Karina Hong]

So you will not solely rely on testing, even though that is a way. That's why.

[RJ Honicke]

So somebody looks at the. And says, yeah, that actually solves the problem that we think it's supposed to solve.

[Karina Hong]

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

[RJ Honicke]

Okay. So I can see how this works in a benchmark. Benchmark. Then if I have, let's say I have a, a flight control system that is like very, then the problem becomes

[Karina Hong]

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

[RJ Honicke]

Yeah.

[Karina Hong]

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?

[Brandon Anderson]

Yeah.

[Karina Hong]

Like, what does that mean? Like we, we can specify. Humans are bad at specifying everything that we want.

[Brandon Anderson]

Right?

[Karina Hong]

There's always like some sort of saying that we are not specified. And if it's not specified, it's not proven.

[RJ Honicke]

Okay, so what do you do about that?

[Karina Hong]

Yeah, so we're not there yet.

[RJ Honicke]

Okay.

[Karina Hong]

Currently, you know, like again, the vision as of currently is anything that can be specified can be proven.

[RJ Honicke]

Okay.

[Karina Hong]

Now obviously there are people who have been really good at, you know, that's maybe where that's the informal kind of reasoner come in. 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, LLM unit test generation by XMCTO Subo and 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, have you thought about, about this, this, this case? Like, and so this is a little bit like conjecture. So the conjecture is going to help with the specification.

[RJ Honicke]

I see.

[Karina Hong]

And then the prover does the proof.

[RJ Honicke]

And so this is an interactive process, maybe that the person. So that when we're actually giving good.

[Karina Hong]

I think this is the future of coding. Yes, I think this is the future of coding and I think this is where, you know, 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 task. Still interesting because it is basically giving you the specification proposal. And then another thing is, let's talk about auto formalization, which is the ability to define it. It is kind of converting something that is more informal into something that is more formal. Auto formalization. So suppose I have a coding problem that is written for ICPC and this problem is written in English like Alice in 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 yet. So I don't have any signal, I don't have any grounding the test cases. Input, output pair is going to ground my formal spec.

[RJ Honicke]

So I know, I have to know I'm going to give this input, I'm going to give this output. It has to have these characteristics. And so, and so I write test cases and I write a. So is there the equivalent in lean of this right, where the specification where you just know the sort of like outcomes that you are expecting so that you like you. The statement of the, the result and then the. But the proof is completely unproven.

[Karina Hong]

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 grounded. Okay, so auto formulation is quite, quite a hard thing to do because you know what's generally happened. Um, you can't, you just, it's hard to ground the auto formalization of a statement. You can obviously ground the auto formalization of a proof, but because you can then just run it, but you need human to eyeball it.

[RJ Honicke]

How big is a lean proof of like a formalized, you know, of a formalized program of significant size. I mean do they grow with the size of the program or do they grow super linearly?

[Karina Hong]

Yeah, currently actually, you know, for each line of code written there could be like 20 lines of, of proof. Okay, it's not looking that great, but,

[RJ Honicke]

but is that like a linear relationship or is it as the complexity of the program gets greater than it like it, you know, sort of also grows

[Karina Hong]

so that It's a good answer. I don't have a good answer to the scaling law of that.

[RJ Honicke]

Oh, okay.

[Karina Hong]

Yeah.

[RJ Honicke]

Because I know that that's a problem in formal verification.

[Karina Hong]

That's right.

[RJ Honicke]

Right. Where you have these huge pro like you have to have these very, very long proofs for even simple. Yeah, yeah. So then do you. Are you going to run into sort of like limitations in, in the capabilities of LLMs when you start to get to large, larger.

[Karina Hong]

What we believe fundamentally is we are building a reasoning engine and we have seen Axiom Prover deal with really huge trees that are like, you know, tree of. Of approve. Okay. We have seen it scale from 40 nodes to 4,000 nodes.

[RJ Honicke]

So. Sorry, Axiom Prover is the, is the

[Karina Hong]

LLM AxiomProver is an ensemble system of multiple models that we do post training.

[RJ Honicke]

I see. Okay.

[Karina Hong]

And also it also includes obviously the tools that axle that we have open released.

[RJ Honicke]

Sorry.

[Karina Hong]

Yeah. In a worse. Yeah, so. So we have seen it being able to deal with more and more complex task.

[RJ Honicke]

I see.

[Karina Hong]

We don't think it's perfectly 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 reinforcement learn some person who is not very talented, that person might behave, you know, perform a lot less well than on post training. Ramanujan, you can, you can, you can argue that very, very sad reality of things. But. So at one point we might consider doing, doing that then. But we think there's so much to

[RJ Honicke]

push, so you just feel like there's so much overhead right now or so so much space to glow that, that you're not running into theoretical constraints at this point. I, I just wonder because you know, there's been recent results in the computation computational complexity of the problems that LLMs can solve fundamentally. And I don't think that they're really a concern for, you know, when I'm writing code with cloud code, but I can imagine problems becoming big enough in a system like this where you have a gazillion lines of lean, you can't get them into the context window. So you have to like be smart about that and then you have to summarize and then you're summarizing and summarizing and pretty soon you're like kind of losing track of what's going On. And it just seems like with a very large system like that, you might run into.

[Karina Hong]

Yeah, I think this is interesting. It's always a problem of abundance. So simply, you just like, keep. Really. The mathematical discovery renaissance has come. Action Prover does try to prove everything. You end up with like tens of thousand lines of lean proof. So first of all, it's. Auto informalization is a lot easier than auto formalization minus a problem of no grounding. Right? So, you know, every, every model has seen a lot of text and a lot of lean. So you can always, you know, convert that link 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 and like proof, like program equivalence, something like that. So that's.

[RJ Honicke]

Oh, so you, you like informalize and then formalize.

[Karina Hong]

Yeah, yeah. You can use it to graph. 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 link. It's actually doing okay. So, you know, that's, that's a, that's the thing. And there's another question of like, which I think is very interesting, is I think there is a panel at ICML Vancouver last year at AI for Mass Workshop. There's like Leo Demora and Jeremy Awigad and Shubo and CTO there. And they were talking about like, will humans or mathematicians at some point stop trying to understand what's going on there, right? Because suppose you're a really ambitious mathematician. You're like, I want to proof Riemann Hypothesis and bang, here's a limb proof. And it's actually correct. And it's just like, problem one million lines.

[Brandon Anderson]

Yeah. Isn't that a big negative for the community? Because usually when someone comes up with a big proof of something, often, sometimes

[Karina Hong]

I was about to get there, right? It's like, will that negative outcome happen? Was the question the panel was discussing. It's completely hypothetical. No one's model system can prove Riemann Hypothesis, right? So disclaimer, please don't cut that part. Just stand alone. But like, you know, well, people still trying to try to understand what's going on. And I think the answer is usually it's 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, verified superintelligence. Suppose we get there is that even, even if all the outputs are going to be produced and at a much, you know, faster pace and much more exponential volume compared to what humans could possibly consume, they're still going to try to consume it and it's, they are still going to try to consume the ones that they deem important. So then basically attention is the bottleneck. And if attention is a 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, worth the sort of spending of compute resources. That's where human mathematicians taste will always guide us. And I think that's incredibly beautiful.

[Brandon Anderson]

Is it worth like internally taking like results that you can prove one way and then trying to send your system at many different routes to get like orthogonal, conceptually orthogonal proofs and so you kind of get a diverse set of different ways of reasoning about the same thing. Because, you know, I think it could be very valuable if you give it a problem to say, oh well, like here's kind of the brute force natural way that like maybe some humans would do do it and then the, there's like a really much shorter, elegant way of doing it. So have you essentially thought about training your models to be elegant in some way?

[Karina Hong]

Yeah, at one point we're gonna get to there because, you know, I think the conjecture will probably depend on what, you know, will probably depend on what we mean by taste. Elegance feels like an alignment problem to me. You know, like, you know, who gets to say what is elegant? Humans get to say what is elegant. Right.

[RJ Honicke]

That's what makes human preference. Right. There's something about hard work, right.

[Karina Hong]

Yeah.

[RJ Honicke]

What you work on hard is what you're going to be good at.

[Karina Hong]

Yeah, yeah, we're going to have a problem about that, I think like pretty much in a lot of the domains as well. Right. Not just math. Like.

[RJ Honicke]

Yeah.

[Karina Hong]

How do you be that senior programmer with you know, really good high level understanding? Well, I guess full stack understanding, high level and low level. If you, you haven't spent the year

[RJ Honicke]

of training, I mean, I would argue that you don't. This is very philosophical but like, you know, I, I don't need to be good at assembly language programming. Right? Like, no, not many people are good at that. A few people are because it's important for their job.

[Karina Hong]

It's not experience, but curiosity.

[RJ Honicke]

Yeah. So. But but it feels to me a little different because not being good at like proving things, for example. Right. That seems like a fundamental, fundamental gap in like that maybe my mind doesn't develop in the same way if I am not doing that. Whereas if I'm just not good at assembly language program. Well, but I'm good at like higher level programming, so maybe that doesn't matter.

[Karina Hong]

I think that's probably because how the, 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 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. 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 combinatorics transfer is more direct, it's 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.

[RJ Honicke]

Yeah.

[Karina Hong]

And if people over rely on strong AI and that doesn't happen.

[RJ Honicke]

I want to switch gears.

[Karina Hong]

Yeah.

[RJ Honicke]

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

[Karina Hong]

Thank you.

[RJ Honicke]

So what's the, give us the high level summary of like what is the vision that you put in front of investors about why does this actually make a lot of money?

[Karina Hong]

Yeah. So first of all, this round is kind of preemptive. So it's, I think a lot of the investors have pretty high interest about, about Axiom 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 mass is a very natural starting point. And then by extension you can increase the verification capability across hardware and so software and for hardware, for example, that's quite revolutionary. I mean that is there is no, as we know, there's no partial credit for a mostly verified gpu. It's all or nothing. It is all or nothing. And you do, and you do need a perfect prover. I want to stretch that which stress this point which is that suppose I am a, you know, I am someone who loves solving math. I think there are a lot of Twitter users who enjoy Pokemon like hunting Erdos problems and then I just try to, you know, use a non deterministic LLM like GPT say to try to get the full proof for that.

[RJ Honicke]

Yeah.

[Karina Hong]

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 kind of domains which I call like hardcore verification needed. It is a pain point. It is a current pain point. There are, there are, there are hundreds of humans and thousands of licenses being dedicated to solve one local grid problem verification.

[RJ Honicke]

Just as an aside, the. My understanding is that the industry standard for design to verification in ASIC ASIC project is like 1 to 31 to

[Karina Hong]

41 to 3, 1 to 4 correct both in say team size and then duration. Yeah. Right. So if you multiply that square and then I think so that's I would say like, you know, it's a must cover. And now for 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 wipe. Would you. Now I heard a story from Kmatz 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, like my open claw can probably do all sorts of things and probably can do some bad things. Like my open claw 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 lim so you don't need to rely on for verification. So you can have a lot of cases, but you can think about maybe an enterprise that is dealing with a lot of regulatory kind of stuff using agents. They might want to do something, it's their choice. But I will argue that the improvement of verification capability both in latency and inaccuracy, all these stuff, the performance holistically is going to determine whether people rely on formal verification or not. So in a way we want to make it so good that basically we can make that choice.

[RJ Honicke]

So, so why did the investors think that you could do this? Right? Because I mean people have been working on verification for so long and I think everyone agrees it's an Important problem. And it. And I think certainly if I can just have a verification proof for every program that I write, like, hey, Claude, like, give me the proof also. And then it just produces it. And yep, looks good to me. I would absolutely do that. But. So why is it, what was it that the investors saw. Saw, in your opinion, that persuaded them that, okay, this is the moment I'm going to put in my 200 million or whatever?

[Karina Hong]

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 going to be worth 10 billion.

[RJ Honicke]

Yeah.

[Karina Hong]

So I think that's kind of the, the feeling that I have, which is that we believe verification is the critical, critical part. 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 going to say on the record, we do not believe that an informal mass system is going to be the mass AGI solution.

[RJ Honicke]

Why not?

[Karina Hong]

We just don't believe that.

[RJ Honicke]

I mean, the counterargument is, oh, you know, like, we just do a lot of good rf. Well and you know, we've seen GPT, you know, solving, you know, I think some artist problem and like, whatever. So why do you think that that runs out of gas?

[Karina Hong]

Yeah. So you can say that if you are a frontier math and you have like a sorcerer frontier lab and you have like infinite resources, why does that. There's by definition no running out of gas. Right. Do you think like, infinite means, like, there's no running out of gas? I don't think it's going to scale to superintelligence.

[RJ Honicke]

So you think that you run out, like you run out of money, basically, or run out of power.

[Karina Hong]

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

[RJ Honicke]

So it's just, it's your sample efficiency argument and so forth that you just, and maybe you just can't. That, that you can't bend the curb enough if you don't use formal.

[Karina Hong]

The thing is, the, the thing is the informal stuff is also available to us in a way. If you really like, you can have a. Both informal and formal system. And that is going to be. I see a 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 just human experts like doesn't scale that well. And if you really argue infinite infinity then sure then you also have infinite money and you can pay infinite. There's so many. Is there really infinite number of people who can understand and proof at say like about like you know, a result non true result in Langland's program. I think, you know, good luck finding those people and in fact I think how Frontier Math came to came together is because they couldn't assemble a benchmark by they are expert poor so they have to 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 the problem is like whether something is impossible to achieve versus something is incredibly expensive and like really incredibly expensive. Expensive and incredibly expensive to achieve. Get kind of like mixed in the end.

[RJ Honicke]

And then of course investors always want to know why you. Right. So I've read a little bit about your background and I think it. We would do a disservice to the audience if you didn't hear a little bit just about your personal story.

[Karina Hong]

I see.

[RJ Honicke]

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

[Karina Hong]

Yeah, I think Axiom is very special because there are really expert mathematicians. Basically they are users of the system we are developing and that iteration loop is very fast. It is extremely fast. You have some of the strongest mathematicians both in research and Olympic contest and you also have people who are mass lib contributors, maintainers, developers, Lingurus 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 Kernel Gen 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 borrowing techniques from the cogen literature and people are borrowing techniques from obviously the broader frontier applied ML to try to apply on the niche problem of AI for math. So we also think having this sort of very special team is a differentiation. We also think that 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 on me, personally, I love math. I think I kind of have been doing math since I was very young. And like math sometimes gets really hard when, when the problem you are 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 yeah, I think why, I figured why not build such a thing?

[RJ Honicke]

You did a master's at Oxford in neuroscience. Has that informed your thinking here?

[Karina Hong]

That's a great question. I think like my, my, my, you know, experience with neuroscience is you, you learn very well about what's hard, what's impossible. I mean, it's 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.

[RJ Honicke]

So.

[Karina Hong]

But I think I was kind of under the pretense of neuroscience, like hanging out at the UCL Gatsby Institute and was fortunate. AI research with some really cool faculties. And so I think that was a very productive year of AI study, if not your own study.

[RJ Honicke]

So it was mostly for you studying AI.

[Karina Hong]

That's right, that's right. I think in the UK, back in the 20th century, if you call something AI, you will not get the donation. But if you call something brain science, you might have the chance. So the UCL Gatsby, which is a premier AI hub where a lot of people actually go from their ship 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 AI. It's called the Gatsby Computational Neuroscience Institute. Yeah, I think how that kind of happened was because so I was in the Master of Neuroscience program and then quickly realized that you need to kill rats and kind of don't want to do that. And computational neuroscience sounds more appealing. And when you look at the process project and you see like Transformer, you're like, you absolutely want to do that.

[RJ Honicke]

Yeah, we're all excited about that.

[Brandon Anderson]

So after the Gatsby, you started a math PhD program at Stanford.

[Karina Hong]

I started actually one year full time at the law school because the JD PhD program structured in a way where you have to spend 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 that cases exciting. No.

[Brandon Anderson]

Do you ever feel like the legal system is under or overspecified in some way that maybe you could act and then prove.

[Karina Hong]

That's a great question. I think for a lot of things it's definitely underspecified. For some other things I was actually quite excited about sort of transfer learning from mathematical reasoning to those specific fields. I think appellate litigation, the 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. You know, Harvard law professor, one of the, you know, strongest like you know, appellate litigation and SCOTUS briefs like brains on, on the left Democratic Party and, and I think there's a lot of other domains such as antitrust that's incredibly flowcharty contract law sometimes also flow charity, bankruptcy, tax more on the corporate side. I, I, I just love litigation side like I, I mean y.

[RJ Honicke]

So actually just, just because we're talking about litigation, it's not the same thing. But there was a, there was a Erdos problem that that Axiom saw. I don't know if it was Axiom proofer or whatever. Is that right? There was a controversy about it because it had represented that it had solved the problem when in fact the proof had been. It had discovered the proof and then just formalized it.

[Karina Hong]

Yeah. So actually what happened was our competitor Harmonic decided to publicize that they have solved unsolved problems. Erdos number 124 and 481. 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 solved them. But turns out that we were both wrong that in fact the problem has been solved before.

[RJ Honicke]

I see.

[Karina Hong]

It's not the only time that we relied on others literature search and you know we, we should own it. The other time was this paper called dead ends in square free walks. You know Professor, 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 the

[RJ Honicke]

point I'm trying to maybe elicit is not, not like you guys did something wrong but rather you know there's this

[Karina Hong]

like Japanese like advertisement of like a whole company, like hundreds and thousands of people like apolog in the, in the advertisement. It's like you know, sorry, we raised our price by like 5 cents and that's the advertisement. I was like thinking that maybe I should just do that. It's so. It's so embarrassing.

[RJ Honicke]

No, but I think that the question of provenance of information and sort of like how do you. It goes back to the question I was asking before about like how do I. How am I connecting the answer to the question.

[Karina Hong]

Yeah, this is a great question. I think after the Erdo Shing we're like extremely careful and so we kind of like, you know, we didn't really look at the other erds problems. I believe that harmonics still continue to claim they have solved Erdos problems that might, might, 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 that's kind of. Indeed. I think like you know search and retrieval is a, is a is problem. Like you don't know if that argument or an equivalent version of that. In fact I think the most interesting part about that entire database is there are a lot of problems that are not directly solved solved but can be just a very easy extension, almost a trivial extension of another result that has been solved or sometimes not even resolved sometimes. I think in this dead end square free walks case which is nothing to do with harmonic complete axiom's fault that we actually didn't realize and Professor Rojan 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 1936 results. It's fascinating. I think it's hard to. Hard to find out why search is a hard problem.

[RJ Honicke]

I guess that means that you do. Does the conjecture engine or whatever does that use search as part of its process or is that something that you kind of the human does guys and then feeds.

[Karina Hong]

I think. I think knowledge graph or knowledge base is a very you know, important component of any. Okay. Any company. Yeah and I think, I don't think it's talked about enough and so.

[RJ Honicke]

And you guys with that it sounds like you don't want to give us too many details but like so you guys have a knowledge graph. I mean that brings up also I, I read somewhere that you guys have a really massive database of lean proofs that you've generated so synthetic data in in some sense but the, the end and this may maybe is a Competitive advantage for you I think.

[Karina Hong]

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, 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 data set, you know, accumulation but that is only just a buffer.

[Brandon Anderson]

Have you ever thought about doing something like an Alpha 0 for math where you start from nothing and let it just make up axioms and see what happens.

[Karina Hong]

Ah, this is a wonderful question. I think that's a very interesting approach actually. Yeah, I think we, 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 Perez'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 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 conjecture ambient theories.

[RJ Honicke]

I think that the, the topic is really interesting and important because it really. You're claiming that the. To get to super intelligence there's sort of this like it's just not going to be possible. Maybe if you had infinite resources you could just rl and it would work. Maybe. But the reality is is that you just can't be sample efficient enough or whatever it is to do that. So that you need some sort of verifier in the loop with the inference process rather than. Because you do have verifiers in like sort of during the training process and you just don't have them during the inference process.

[Karina Hong]

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

[RJ Honicke]

Yes.

[Karina Hong]

As well.

[RJ Honicke]

I mean I would, I was surprised that that like when, when open one was, you know, everyone knew O1 was coming but it did hadn't come out. I was sure they're going to announce that they're using Lean to, to do like formal verification of proofs and actually generate proofs and then verify them so that they're grounding and reasoning. I mean that was my.

[Karina Hong]

When Ilya was there there was gptf. That was a great piece of work. There's also mini F2F. These are all formal math work at OpenAI.

[RJ Honicke]

Okay, so presumably those guys, they're doing something.

[Karina Hong]

No, no, they all left.

[RJ Honicke]

Oh, they all left.

[Karina Hong]

I see. So that's my point, which is that if you're 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 it can just like all fall apart thing. You might have a better chance of staying focused on the same problem for as long you as. As it takes at say a startup like Axiom or one of the other new labs.

[RJ Honicke]

Yeah. If you're aligned to the mission of the company rather than like somebody decided that what you're doing is no longer.

[Karina Hong]

Yeah, yeah. It can be your VP lost some political fight and so.

[RJ Honicke]

Yeah, yeah, absolutely.

[Karina Hong]

So now obviously if we succeed, then they're all going to, you know, start doing that again.

[RJ Honicke]

Yes.

[Karina Hong]

And then like, I guess as a talent, then there are more like, you know, potential places choose from as well.

[RJ Honicke]

Yeah. So then your job is to go fast so that they, they're, they're struggling. So actually you, we haven't talked about it, but you actually also just released an, an API for doing Lean verification.

[Karina Hong]

Yeah.

[RJ Honicke]

And I actually tried it with Claude code because it's easier than setting up, you know, your own Lean tool chain.

[Karina Hong]

Yeah.

[RJ Honicke]

And you know, like tried to get Lean to prove some stuff and the infrastructure is maybe non trivial, especially at scale. So you want to talk a little bit?

[Karina Hong]

Yeah, yeah. So we just released Axle A X L E stands for Axiom 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 metaprogramming tools. Now. Metaprogramming talents are extremely, I think like, you know, hard to find and we're so grateful to have like really crack team working on that and we want to kind of like release it to the community to use for free because we think that there are probably other people doing also like large scale Lean operations and these tools going to make their stuff go a lot more robust and faster and do so at scale. And Axle is Currently, I think 14 such tools starting from Verify Proof, which is the sort of to make sure that there's nothing weird going on, like no sort of cheating by link code. You don't Axiom something out you don't assume weird things. If you axiom n plus n equals n, you can prove 2 plus 2 equals 2, which for sure that's not the right answer. There are also a lot of other kind of generation tools. For example, you can try different repair attempts. So broken lean in and then good lean out. And there are currently other repair methods by LLM. Hopefully 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 get you to a place that's quite far. A lot of the people from the link community has been using axo, even 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 do interesting things in actor and we have seen also we have heard from a lot of the people that Claude plus Axle is kind of their go to setup for. For now. We think that these are really interesting tools. I think famously, I think today there is this mathematician who said he formalized the Donald news, you know, using Claude to prove I think a result, Ramsey result and to formalize the limb proof. And then that is also using Excel tool. So we are really glad to see people kind of already using it.

[RJ Honicke]

I mean, I feel like this is a great opportunity for or the collaborations that Terence Tao was talking about as well, where once people have access to the common tools, then it becomes easy to do. And I mean like if, if you have an intuition, even not a strong mathematician 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.

[Karina Hong]

Yeah, I think that's, that's very interesting. Like view, which is that like, if you think about like math, 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 subtasks, but really the blueprint writing process by say, Terence Tao and Alex Kondorowicz 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 a result about sphere packing 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 lean 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 bottlenec. Many people are trying to solve around the same time.

[RJ Honicke]

So is there value in me as a, you know, cloud code user trying to attempt like some small lemma or whatever where I don't have a great understanding of the math? Maybe I have a high level understanding.

[Karina Hong]

Depends. Are you trying to formalize or are you trying to prove. To prove new things.

[RJ Honicke]

That's a good point.

[Karina Hong]

Yeah.

[RJ Honicke]

So maybe form, you would obviously probably start with formalization. Right. You know, the proof and you just can't get. Yeah, nobody has been able to get the formalization correct.

[Karina Hong]

I 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. No, it's, you know, it's all the formalization. You don't have that process. Well, it's interesting because I think a lot of the my friends who started, you know, working on Lean and Mathlib was because they are in PhD and problems really hard, we get stuck all the time and we want to kind of review some of the undergrad. That class is a time where we still understand what the math was about and we do so by you know, doing Lean and I think that's, that's

[RJ Honicke]

very beautiful the material.

[Karina Hong]

Yeah. But if you have for example like, you know, access to action improver that also can formalize all the formalized things and you don't have, you lose that part of the learning process. Yeah, yeah. But I do think that, you know, like for, you know, you and I, we can set up like axle and, and try to see what results we might be able to prove. And I think that's quite interesting. And thanks to Axos sort of making the speed a lot faster. You don't have to wait very long. I remember the Phnom exam day. We were all in the war room. It was a Saturday. We're all really excited and we just got the exam paper from the official organization, the proctor of the Pandemic exam. We just were looking at how much workout Axl is getting and without it we couldn't have solved it with I think eight problems within the time limit that definitely not within the time limit. And I think one thing about these tools is like it's Very interesting in that potentially you can have interesting reward for RL as well.

[RJ Honicke]

What do you mean by that?

[Karina Hong]

So for example, verify proof can be a reward for just basically a proof is completely correct and validated.

[RJ Honicke]

I see.

[Karina Hong]

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

[RJ Honicke]

Yeah. So you mean for example auto formalize the informal proof and then verify and then use that as a reward. Or do you mean no as in

[Karina Hong]

like you pass like Lean programs in these formal tools. Right, like and you will have some sort of score.

[RJ Honicke]

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

[Karina Hong]

The value proposition which is interesting about Frontier Lab is that suppose you are a 2C business, then sure, you can just not do what we are doing. And we have seen for example Deep seek 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 are doing. It makes a lot more sense for you to do co generation further your strength and moat. You can partner with Axiom just like how for example Frontier Labs partner with startups that work on search such as Excel and parallel. Right. Just call Excel API for surgeon. Potentially, you know, if you're a Frontier Lab, I think you should call Axiom API for verification. Yes, valid proposition.

[RJ Honicke]

Setting up your own info.

[Karina Hong]

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

[RJ Honicke]

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

[Brandon Anderson]

Why did you decide to start taxium.

[Karina Hong]

Right. What did I decide?

[Brandon Anderson]

Like you were a grad student at Stanford.

[Karina Hong]

Yeah.

[Brandon Anderson]

And you know, in math.

[Karina Hong]

Yeah.

[Brandon Anderson]

So what made you decide?

[Karina Hong]

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

[Brandon Anderson]

Oh, really?

[Karina Hong]

Yeah.

[Brandon Anderson]

Was that the plan or did you. Did you start there and you're like almost immediately realized that this is.

[Karina Hong]

Right. Right. So. So the year of law school. Right. Was very, very interesting to me, like on the intellectual level. But it's also this the first year where I had no technology math whatsoever in my life. It's a weird year. Right. Like I'm. I'm reading a lot, I'm I'm practicing well. I'm learning how to write, I'm learning how to read. Like, and, but like I'm, 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, 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 bo 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 kind of papers. I was, I was learning all of these, like, just by myself. Um, 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, 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, like, you know, I need to do something about it. I mean, it's like I fall madly in love with the idea that AI is going to do math. And like, okay, now do I do math? 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 night Henness event. Nihanci Scholar Denning House, 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 dro, 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 startup 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 hundred percent, zero percent. And then she's like, well, you kind of have to follow your energy.

[RJ Honicke]

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

[Karina Hong]

Yeah, I was completely obsessed with it. I thought it's going to be big. And I thought like, it just, it just has to be A for profit startup because like it's so much broader than making mathematics medical 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 scientists, like the mass reasoning is going to be, is going to be a pretty big part of it. And now trying like I think the sort of belief by Cursor and Claude and other folks is like okay, like just like mass transfer to coding. Coding transfer, transfer to math as well. I think that's true. It's just that like you know, why, why not push it directly? I don't, 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 a 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, 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 blueprinting, 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. 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 chat bots mixed up. Is AI the solution to. Sorry, is 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 about scaling brilliance. And the third point is that like verification to me is not about like the sort of, you know, 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 going to 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. It sells really well to, I think the general public, including my parents, like, oh, while we're doing verification because technology make mistakes. No, we don't think verification is because of the distrust for technology. It's because that's what expected rapid exponential scale up and the deployment and the creation of technology and technological progress is what that, that compels and demands.

[RJ Honicke]

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.

[Karina Hong]

Yeah.

[RJ Honicke]

And math drives a lot of science and innovation in the world. And the innovations in math drive innovation in the world.

[Karina Hong]

So that, but it doesn't need to even go through like in terms of, you know, the solve, mass, solve everything thing. Like obviously stands. Like my point is like transfer learning doesn't. Like transfer learning is about like pushing math reasoning. It just. So there are kind of, I guess there are a couple narratives here for some people is that you solve math and then math are the fundamentals of sciences. So that's actually from AI for math. Take this radical layer of AI for science. It's that narrative we actually believe in, just like general transfer learning. I think Axiom is on the infrastructure stack.

[RJ Honicke]

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

[Karina Hong]

Yes, I think it's so. 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 and engine. We do not expect that TAM to be as large as solving math through the formal way.

[RJ Honicke]

Why?

[Karina Hong]

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

[RJ Honicke]

Yes.

[Karina Hong]

What we are doing is it's not informal versus formal. We're not taking this sort of like completely formal alpha proof approach. It's bridging between informal and formal. It is bridging between high level and low level. It is a direct, it's sort of like a direct improvement to reasoning through transfer learning. And it's also indirect in that like, okay, well like math is going to unlock a little science and.

[RJ Honicke]

Sure.

[Karina Hong]

And that is really what we are seeing.

[RJ Honicke]

So you Think that it enables transfer learning. Yeah, I see.

[Karina Hong]

I think that is pretty much a consensus. I think it is a consensus and this is 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, 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.

[RJ Honicke]

That's an interesting perspective.

[Brandon Anderson]

Did you get everything out that you wanted to?

[Karina Hong]

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

[RJ Honicke]

Yeah.

[Karina Hong]

And we think that sort of like solving math and especially like formal math is to help us tackle the really ambitious quest of verified AI. Now when we are done with that, we might have other 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 software stuff and for other things to be getting reward like physical world signals.

[RJ Honicke]

But do you think that the, the sort of the capability of doing really powerful reasoning once you have that powerful verified reasoning engine that that's the moment when. Okay, now we've unlocked that for you know, software verification and hardware or whatever.

[Karina Hong]

Yeah.

[RJ Honicke]

But now, okay, so now what about biology, what about chemistry?

[Karina Hong]

So that could be one. The other one is then like really how far are you to recurrent of self improvement?

[RJ Honicke]

Okay, so just AGI.

[Karina Hong]

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 solve 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, then solve this. They just solve like AI for science.

[RJ Honicke]

Yeah.

[Karina Hong]

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

[RJ Honicke]

And so the recursive self improvement angle, it sounds to me like you're saying that the combination of verification plus the sort of like language which is informal, it's that combination that enables really good recursive self improvement.

[Karina Hong]

I think recursive self improvement is going to happen anyways. We're Trying to have like formal, where verification earns place. So again, whether formal verification can be welcomed and deployed and become a consensus depends on how well we execute. And I think when you boil down that problem into an execution problem, you should just go for it.

[Brandon Anderson]

Looking forward, what's the biggest bottleneck that you see in the field for both Axiom and maybe just the field abroad

[Karina Hong]

in terms of fragmentation? So I think we're in a market where people like to start like you know, a thousand people, they don't join forces, start a thousand things. I think that's actually the biggest like kind of bubble indicator. I think there are categorical bubble and there are like other categories where there are moonshots. It's not bubble. It just looks a little bubbly in the field. If people who are like really like of really legit backgrounds decide to join, join force and work in the team for the mission rather than for ego, for kind of the status Neolith founder, I think that category is I'm really bullish and vice versa. So I think the bottleneck actually is about potentially I think it's annoying because it's like we are in the, if you believe we are in an age of research, if you believe in deep tacks 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. You know, 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 like for long, long hours and we spend 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 park capital somewhere and while we don't work with them, these are market conditions that encourage fragmentation. And when things get fragmented, no one gets there. I think every category, regardless of how right the idea is, it's pretty much in a sort of earning the right to exist stage. And if that is the case, then for example great deep tech company SpaceX and people do actually join force to work on that dream. And potentially in that case also a very charismatic founder. I think a really kind of concerning thing for me personally is that for other probably some categories that I'm personally quite bullish about their action about and just like looking at things generally fractured fragmentation is a problem. Like the sort of you know, we see start pulling professors from university to work on something when it really is a really interesting kind of situation.

[Brandon Anderson]

Maybe this is a naive question, but like right now when you were talking about players in let's say AI for math, where you know, you Harmonic and then you know, the big labs. Right. Am I missing someone? Is like is that actually flow fragmented? Really?

[Karina Hong]

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

[Brandon Anderson]

Yeah.

[Karina Hong]

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 Keono and Francois Charton on one team, this is fantastic. You have someone who's a core contributor, Frontier Math, tier four, really great benchmark setter. Francois, who's on the A for Mass discovery have proving 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 force together. I think I for Mass is a good category because of the absence of fragmentation. But even you know, from, from our perspective, the sort of, for example, you know, RL right being. I don't, 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 l Everyone. And there are a lot of companies being started and then sold like three months later. And just each month where you could have worked on a technical problem and you're instead working on deals, it's a month that is wasted. And I say that like, you know, also with some amount of pain and suffering because having gone through two fundraises. Yes, yes, yes.

[Brandon Anderson]

Yeah, yeah. So what's the biggest bottleneck in AI for Math?

[Karina Hong]

For any axiom for aiform Math.

[Brandon Anderson]

Not axiom, but just the community.

[Karina Hong]

But the community of AI forms.

[Brandon Anderson]

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

[Karina Hong]

I expect fragmentation to start to happen as Axiom and Harmonic establish category leadership. 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 Math Olympiad. So we couldn't have competed in that. Anyway, the next Math 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 Putnam be hard and in fact it was harder than the IMO and the Mohs scale. If you look at AI, you know how many scores the AI has retained on average and on the max difficulty of the problem pandemic is harder in 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 going to set 4 months goals. If I build a company only setting 4 months goals I might build a really short sighted company. So there are like I think longer horizon problem. I think for example I market forces could force other players into chip verification. Well, it is possible that co verification is a holy ground. It's possible that if you solve that then you also naturally solve chip verification with some amount of epsilon caveat of distribution shift. But I strongly believe that a bottleneck could be the pressure. But I think that Axiom is fortunate that when we are early enough we are a team of just incredibly high agency people that our execution generally surpasses expectation. But I think like what I think could be a bottleneck for the entire AI for math field is that potentially trying to prove commercial value is going to distract significantly from the core capability improvement.

[RJ Honicke]

Yeah, that makes sense. Thank you for driving up and coming to see us.

[Karina Hong]

Thank you so much.

[RJ Honicke]

I know the traffic was, was horrible.

[Karina Hong]

Yeah, thank you.

[RJ Honicke]

And it's been really a pleasure speaking with you and we look forward to seeing how things develop.

[Karina Hong]

Yeah. Thank you so much.

[RJ Honicke]

Thank you.

[Karina Hong]

Awesome.

[Brandon Anderson]

Thank you.

[Karina Hong]

Thank you. Yeah.