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

I think that we are at a threshold of mathematical renaissance which is to realize that there's so many unsolved problems that will currently take say researchers um months to to crack that

we believe is not sort of out of reach for today's AI technology. The world is realizing that we need verification like you know we can have very cool like gloable websites but like how do I vibe

code nuclear reactor our world view is mass reasoning is a true reasoning layer of AGI from mass you kind of get to code and from code you can run a lot of real world experiment in the software stack

is a beautiful vision is for all the theoretical problems to be resolved in a satisfactory way >> hi I'm Matt Turk from firstark welcome to the mad podcast today my guest is

Karina Hong founder and CEO of axi Karina is a 24-year-old road scholar who's had an incredible personal journey from competitive math Olympian in China to MIT, Oxford, and Stanford Law. She

started Axum less than a year ago to build an AI mathematician, a system designed to be 100% correct 100% of the time, effectively solving the AI hallucination problem. We talked about

hallucination problem. We talked about how Axum's AI aced the notoriously difficult Putnham math exam and then went on to autonomously solve four open research conjectures. Why verification

research conjectures. Why verification is becoming the missing layer in AI. how

Axiom works under the hood and what this could all mean for the future of AI.

Please enjoy this great high signal conversation with Kura Hong.

>> Hey Karina, welcome.

>> Hi, great to meet you.

>> So you are building an AI mathematician.

Why does the world need an AI mathematician?

>> Yeah. So I think that the idea where you have like infinite number of mathematical reasoning agents going out to the industrial society to solve like all the theoretical problems. I think

that's incredibly compelling. I think

through solving math we also realize that it can solve a lot of other problems such as verification such as optimization is actually I think that math is great and if you solve math you

can have physics you can have a lot of logic and property and you can extend to a lot of things. Um the world needs more math.

>> Great. Uh and what kind of math are we talking about? Is that is that high

talking about? Is that is that high school math? Is that competitive math or

school math? Is that competitive math or is that deep research math? Yeah, I

think people generally start with competitive math because it's kind of you know that you have like a non-solution and then you um kind of start heel climbing the infinite sort of like infinitely high mountain of math.

Um there are actually two axis of difficulty. One is how creative the

difficulty. One is how creative the solution is and the other one roughly speaking is how abstract the mathematical object is. So say a qualifying exam can be incredibly um

abstract but the sort of creativity required to solve each problem might not be that high might be very standard. On

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

>> You guys are ultimately a young startup but you've already had incredible success. So let's talk about the

success. So let's talk about the platinum uh last year first and maybe define what the platinum is for people that may not be in the math world.

>> Yeah, 100%. So we started out um in July, mid July and so Putnham uh was December and we were like a four month startup. We were kind of like looking at

startup. We were kind of like looking at Putnham as this like really hard mass competition and u most of the people actually got Daro. So over 50% of humans

got zero and um I think over the 100 year history of Putnham there's only five human perfect scores. Um

>> and it's you have six hours to do it and 12 questions is that >> that's right. You have you have 12 questions. You have three uh three-hour

questions. You have three uh three-hour sessions. You have morning and

sessions. You have morning and afternoon. So yeah that's a setup. I

afternoon. So yeah that's a setup. I

think it was a Saturday. It was December 6 and um we all kind of gathered at the XM office and decided to put XM prover in the real-time test. So it's not a benchmark. It's uh you know we got the

benchmark. It's uh you know we got the exam from the proctor of the of the ponam exam and then we just basically throw it to the approver and um we announce that we got a perfect score. Uh

>> so 12 out of 12.

>> That's right. Um eight within the time limit and then 12 out of 12.

>> And then uh the more recent challenge that you guys solve I think you you solve four challenges. Maybe talk to that. That just happened.

that. That just happened.

>> Yeah that's right. So I think that because we have like a lot of mathematician friends and they all have a lot of really hard research conjectures. So for example, professor

conjectures. So for example, professor LG fail and he has like four fail conjecture and this is the last one still standing and he's a Israeli professor at the Technon University and

there are also um Dawi Tren a Boston College professor who's an algebraic geometer and he um knows actually professor Kenono who's our founding mathematician for for years and they

recently met at this joint math meetings conference. So he also supplied a

conference. So he also supplied a problem. So people start sending

problem. So people start sending problems to us and then we just put the system into test and recently I think like a couple weeks ago we just announced that Axium prover solved um these four research level open problems

and it's quite interesting because it's probably the first AI to solve a research conjecture completely end to end and self-verified that means the output are fully verified 100% correct

>> and that was without uh human >> without human intervention that's right >> okay my very uneducated understanding of world class level math is that a lot of

the top informations today in the history ultimately operate through a combination of like you know she IQ deep knowledge and all the things but a lot of intuition and a little bit of

serendipity where does that fit >> yeah I think like kind of two parts one is there are like some really important mathematical breakthroughs that happen like you know once in a decade um or

maybe perhaps more one once once in a decade for each each domain probably, but those require like very um you know interesting sort of ureka moments um

deep intuitions and and um very sort of almost like lucky kind of moments. Um

and there are a lot of other questions that are sort of proficiently um routinely applying the standard bag of tricks and I think that a lot of the research questions can be solved by a

combination of of both. So a little bit of intuition, a little bit of sort of just just kind of like one step at a time. I think that we are at a threshold

time. I think that we are at a threshold of mathematical renaissance which is to realize that there's so many unsolved problems that will currently take say researchers um months to to crack or

even technical lemas in those really long-standing conjectures that we believe is not sort of out of reach for today's AI technology but only through I

think very intricate you know design of system and hybrid kind of use of different methods um and that's what what Axiom is trying to do These are the first like batch. We hope to have a lot

more coming. We actually have actually a

more coming. We actually have actually a few more research conjectures that's being proven every week uh just by the supply of mathematicians um you know from the world and and we try to put

those problems into use.

>> Fascinating. And is the system solving problems in predictable way? Where I'm

going with this is the whole move 37 discussion where you find AI um solving problems in a in a almost alien kind of way. Is that part of what you're doing?

way. Is that part of what you're doing?

Is that what you're seeing or is that something that's coming up in the future?

>> It it's interesting because there's I think like a hindsight problem. So it's

like we didn't know how to do it. I

think like I definitely have no hope in solving those conjectures and our founding mathematician professor Ono didn't know how to do it either. Okay.

Now we saw the ling code right like thousands of lines of ling code and sort of read through it understand it and uh maybe we see some of the techniques as

sort of standard but I think the application of them and the combination of them is also not entirely I think it's somewhat at the level of a junior

math professor say like you know a posttock or a junior researcher obviously a lot of junior researchers do amazing work and they have their move 37 moments in some very long-standing open

questions, but there are a lot of sort of day-to-day um of research that it feels like it's at that level. There's

also this question of like because it's solving the problem in limb, which is a kind of machine language, not a human natural language, uh the proofs actually look quite different. So, we actually analyzed all 12 problem solutions of the

punam exam and we found that a lot of the solutions actually differ from the human solution. So because it is a you

human solution. So because it is a you know leanbased system it is really good at sort of routine bookkeeping and it will actually choose a lot of the more

mechanistic you know arguments over the ones that require like a clever say one picture solution and on the other hand you know there are a lot of these sort of casework that humans shy away from um

it's just very you know easy for for the machine there might be like a slightly bit of what's difficult for humans versus AI are different >> so you mentioned mentioned lean a second

ago and I guess that's going to take us a little bit into um how the the the product and the model work maybe for people again who are not in the math world what is lean >> so lean is a programming language for

math proofs I think that's kind of the oneline high level uh explanation u there's this kind of concept called ker Howard correspondence which basically

allows you to kind of code math up as computer programs and so lean is like similar to Python but it also can serve

as its like self-verifying uh function.

So in the computer science analogy it's roughly both the C language and the GCC compiler. So so two in one it's a formal

compiler. So so two in one it's a formal language. There are a lot of sort of

language. There are a lot of sort of other improving language before lean such as Isabel such as um COQ um now now called rock roq and such as whole is

actor. So there's this sort of like

actor. So there's this sort of like family of like formal languages and LIN is one of them and it's a very popular language. There are a lot of people um

language. There are a lot of people um mathematicians around the world that use lean that choose to code their um proofs up in lean and they can just run it and

then they will see a check mark which shows that it's a correctly logically correct proof and if there's an error message maybe there's like a bug somewhere or there is some sort of

syntax or you know type mismatch just like any other programming language. The

fun fact is you can actually use lin as a functional programming language. you

can write an autograd for example and that's that's very interesting because basically it allows you to both math and code at the same time. Um so if you

think about a security protocol you can uh try to implement the code in ling um but also prove that prove its soundness in ling. So it's a very flexible

in ling. So it's a very flexible adaptive language.

>> Great. People may have heard of both openai and Google deep mind sort of winning IMO the international math olympiad and other very hard to crack

kind of like math problems. How does their approach differ from what it is that you guys are doing?

>> Yeah, I think the sort of concept formal theorem proving actually uh existed like automated theorem proving as a field existed before before deep learning. So

I think there are a lot of uh researchers a lot of them in Europe in 20 say 2018 and even even before then we're doing sort of like automated uh

reasoning without without the LM component and we actually have some of these people on our team like they were the authors of ATP boost um and uh it's

very interesting time in 2019 um from source chart and gimmo uh the co-founder Mistra they have a paper which tries to put transformer own sort of symbolic

integration and realized that it can beat like computer algebra systems such as mat lab or mathematica. Uh I think Elia was actually the reviewer of the paper and he actually tweeted about it.

There is this other field medalist um Tim Gower said it was uh either amusing or gamechanging because it was it was in on open review people don't know if it's correct or not and that was not amusing

that was the beginning of AI for math and Frano is now also at Axiom. uh this

is like a long history of what people are trying to do with it and I think uh Google you know started the alpha geometry effort in uh 2021 and that was

very exciting effort they realized that if you convert the figures and lines triangles circles intersection points in the symbolic uh expression in the vector

language a specific domain specific language for geometry ukarian geometry uh you can actually try to do those geometric problems like a lot a lot easier and than using using machines and

that's very interesting because it's just like draw back to my childhood time where I was doing mass Olympia and I never I could never solve one ukarian geometry problem. I don't know what's

geometry problem. I don't know what's wrong with my brain like it's usually the easiest problem of every competition. So it's like if you go to a

competition. So it's like if you go to a math competition, you don't solve the geometry one, then like obviously you can't solve the inequality one and obviously you cannot solve the number theory or the commentatorics like you know holy grail like it's like that's

like the one problem you must know how to solve and I don't know how to solve it and I remember my teacher the coach taught me how to do the complex coordinate one which is a very tedious way of converting everything that shows

up on the figure into a complex coordinate and just basically manipulate those algebraic expression and and through that I can solve it. I will

solve it a lot slower than other people but at least I will solve it. But it's a very interesting philosophical point which is you can convert like you know geomet geometrical figures into algebraic expressions and I think that's

what they what they did. I mean not exactly the human uh version but alpha geometry and then that led to alpha proof in 2024. I think Google sort of

silver medal in in alpha uh in IMO u missing the gold medal only by one point. Uh that was my moment. That was

point. Uh that was my moment. That was

my moment of immo at least and then they couldn't solve the two common toxics problem and in 2025 no one solved the one common toxics problem either. So

2025 there's only one common problem and I think that was kind of the the history of things. There were also um other

of things. There were also um other players in the field and also a lot of really great academia labs doing it. We

kind of take the approach of you know we we think that it's important for the system to be able to reason both informally and formally and in a way sort of bridge across these different abstraction from high level intuitions

to low-level like more like lean sort of formal checking and >> what does that mean formally versus informally?

>> Yeah. So informal is like say reason in natural language in English and uh mathematicians quite fascinatingly they have been doing reasoning in in in English I mean for for thousands of

years. I mean they write formulas as

years. I mean they write formulas as actor but but mostly they they they write you know arguments proofs in in English and I think um it's to us math is code in a way mathematicians have

been coding in English for centuries and thousands of years the formal language means you know lean and you know the the sort of output will be lin machine code I mean wouldn't be super readable to

humans but I think the there are two beautiful things going on here one is first time this sort of formal proving doing kind of comes in to assist

mathematicians which is a traditionally informal reasoning subject. The second

thing that's interesting is you can play the strength of both informal reasoning and formal reasoning. So you're kind of like you can bridge across these different sort of like level of

abstractions and uh autoformmalization which is the sort of um capability of converting uh the natural language reasoning to say the formal language and

that's harder than translation because it's it's different than say translating between two programming languages.

you're translating something that cannot be verified natural language into something that can be and that direction is obviously very challenging but also very uh very promising. There's also

auto informalization which is kind of trans translate back I mean from lean to to English that's easier than auto formalization because most of the machines AI have seen a lot more English than l

>> and just to make sure I understand so are we saying that the open AI and Google DM approach would fall into the informal correct >> whereas you'd be falling into the formal

>> Google was doing I think formal until I think as of the previous year's IMO 2024 the alpha proof system was a formal system >> um >> so it's English and my words not yours

but like more of a brute force kind of approach versus what you do is more neuros symbolic is that accurate >> that's how I would describe it I think uh first of all is that we are you know

we are supportive of scaling we think scaling works uh in in a lot of the scenarios uh there's also this question of simple efficiency which is kind of you know how effective uh scaling is

potentially um and I think for the sort of informal like way to solve mathematics require like vast amount of like training data. Uh you basically throw everything you can possibly find

uh on the internet to it. Now my

question of that is what if you also throw these vast amount of mass tax data to your AI but you throw the lean version of them as well. I think that's

you know we believe in doing things at big scale and internet scale data set of link. uh I think that in addition to the

link. uh I think that in addition to the internet you know scale data set of mass going to be quite interesting and and I think that we shouldn't we shouldn't do pre-training we shouldn't try to just

only train from scratch I think kind of focusing on uh post- trainining uh reinforcement learning uh can potentially get us better performance gain

>> and uh to that exact point like help us contrast and and compare so RLVR uh versus which is reinfor sort of

running with verifiable rewards against what it is that you do. Is that those just completely different approaches because they both seem at the same thing which is to basically get to uh

perfection.

>> Yeah, I think we um we the world is realizing that we need verification.

Verification mean very different things in math. I think in 2020 early 2025 or

in math. I think in 2020 early 2025 or late 2024 uh it means the numerical answer associated with each problem. Now

the thing is like one is you know reward hacking like you know we have seen from say frontier math and other benchmark which only compels a numerical answer

that it doesn't actually necessarily reflect the model's capability in the logical reasoning. So it's able to get

logical reasoning. So it's able to get to the answer without reasoning through it which is quite fascinating. I mean

there's always these when I did math olympia before and there's always this like classmate who's really good at guessing the answer. I don't like AIM which is this exam um that all the answers are between 0000 to 9999. Like I

remember there's one year where my friend told me that like you know he just basically guessed three questions correctly versus the rest of us need to like reason it through and like Jesus Christ he just put like a zero in there

and then somehow that answer is indeed zero. It sounds very unfair and you know

zero. It sounds very unfair and you know in a way in high school the teacher will like ask you to show your work. So for a while I think like verifiable reward means that final numerical like output.

I think that like people are now realizing it doesn't scale to the sort of mass AGI and however you define it.

Most of the sort of adult mathematics mathematical research are proof based um require sort of step-by-step rigorous deduction based on logical reasoning and a lot of them don't even have a

numerical answer. Like a lot of the

numerical answer. Like a lot of the problems are prove that something exists. um prove that something cannot

exists. um prove that something cannot exceed a certain value. You know, very seldomly, I mean, beyond the mass olympiate kind of high schoolers context, you would have a mass question where getting to the answer at the end

of it, it's a lot more difficult to get verification reward for the intermediate steps, right? And so, if you want to

steps, right? And so, if you want to have a reasoning engine that really truly masters at logic and mathematical reasoning, then you need to somehow get verifiable reward for the proof steps.

Coding is great. Like I mean people have seen like RL and coding have incredible gain and can we turn math into code and LIN which we just talked about the car Howard correspondence exactly turn proof

into computer program >> so that makes RL like you know possible in our setup as well >> and just to uh drive it home for people in case that's not obvious by now what

we're talking about is building an AI that is 100% correct 100% of the time right so completely solving the hallucination problem or the

stochastic um issue.

>> Make AI perfect, the perfect prover.

>> How generalizable do you think the approach that you guys are using is?

>> I think the the one thing if you talk about perfect AI, I think people's first reaction is wow that's really valuable, right? I think a lot of the you know

right? I think a lot of the you know different labs are trying to uh reduce a hallucination uh or increase sort of the accuracy um through many many different ways. If you have a lot of the sort of

ways. If you have a lot of the sort of industries where mistakes are extremely costly um that's a block to AI deployment if you don't have that sort of provoke guarantee and now that's a value of like say catching the edge

cases and there's this additional value of trusting that your edge case can be covered. So two two additional layers of

covered. So two two additional layers of value um to sort of you know reliable consistently correct AI. In terms of like how general this is I think we start with math our war view is mass

reasoning is a true reasoning layer of AGI and I think a lot of the labs share that view. Um labs across US, China,

that view. Um labs across US, China, Europe and you know from math you kind of get to code. Uh math gives you proof of property and code gives you output.

output um and property affiliated to it are two quite important part of the digital world and so from mass you go to code and from code you can run a lot of real world experiment in the software

stack then you can have a lot of other things we don't claim to be doing things that are in the physical word at all we are obviously not doing things that are nonverifiable say just like you know

sometimes mathematicians are uh stereotypically not the best sort of writer we are not kind of building a you know an AI that's very really good at literature But I think in a lot of the

fields such as um from math and code um verification and sort of verification applied to many different domains it's it's incredibly valuable >> and do you need a a lean equivalent for each one of those domains as you expand?

It's a very interesting question I think so uh as you can see even within math right sometimes creation of domain specific language like the vector language for Uklan geometry have its

gains um there could be the case where in other domains um something that is not exactly the abstraction of lean are the right sort of medium but in that

case you know you can sort of do code translation and you can kind of build out you know the sort of uh stack that's required to use your like lin based um

serroving engine. I think the sort of

serroving engine. I think the sort of gap between say for example lean and another like strongly typed language like rust is a lot closer than the gap

between lean and English and I think that's a lot of the commercial value. I

mean if you can sort of reason in between informal and formal space that I think is going to unlock a lot of the things beyond just the power of a formal theorem prover.

>> Yeah. And do do you have a sense for where that threshold is? So if you have math on one side and English on the other side, effectively with your approach, you're going to be able to

cover kind of like all of science and the second you start getting into non-scientific fields, then the approach doesn't work anymore or you don't know yet and you're about to explore.

>> I think we want to try to figure out like what are things that can be done in software. One is I think math and code

software. One is I think math and code they really complement each other very well. I mean there a lot of great code

well. I mean there a lot of great code generation company uh we can provide proval guarantee and code verification.

There are a lot of other like domains where just that sort of verified generation capability is incredibly valuable like hardware and then I think if you can have a lot of theory and you

can have partners who are really good at real world testing then that is you know AI for science and I think that's also incredibly promising. I feel like this

incredibly promising. I feel like this is a generational effort. It's going to take like a long time. Um, we're going to see the DNA of the company remains math and we're going to see best first

market, maybe verification, best second market. I don't know what that is. Could

market. I don't know what that is. Could

be optimization. A lot of the things I think are waiting to be explored. Um but

just the generation verification loop I think itself is going to have a large TAM and then I think you know there are a lot of things that we're also learning together with the potential customers.

>> Yes cuz you're also a a year old company not 10 months old.

>> Uh 7 months old.

>> Seven months old. Okay. Amazing. Before

we go further I you mentioned uh your background a couple of times in passing and um as I was prepping for this is just so fascinating. I want to spend a few minutes uh talking about it. We

covered it in in some other podcast, but I think the story is just uh amazing.

So, taking it from from the top. So, you

you grew up in China and you were a competitive math kid.

>> Yeah.

>> Just uh tell us that story.

>> Competitive math kid is such a great term >> because you can like you can break in different ways, you know, competitive math kid. Competitive math kid.

math kid. Competitive math kid.

>> So, which one was it?

>> Both. Well, I think I like to win.

>> Yes. So, um, walk us through, uh, what what is that experience and how >> formative was this?

>> It it was extremely formative, I think.

Um, years of mass Olympia training. You

have one goal that is to score as high as possible on whatever that is next mass competition. You have people that

mass competition. You have people that are in the same sort of community circle that are also doing the same thing. You

are friends with them. You're

competitors with them. There are a lot of sort of like you know background reading learning exercise you need to do to overprepare for every competition. I

remember I did 75 exam papers to prepare for a competition that I didn't know if I will be selected for and I didn't end up being selected for it. Um

>> how old were you at then were in high school?

>> I think it was like 14 15.

>> I think I learned um a few things. One

is resilience.

It's just like I think you get addicted to pain and suffering. So that like the word resilient is like almost a paradox because it's like you like it. It's like

failure is like a given. I think um throughout that time I mean just the exam get keeps getting harder and the number of people competing keeps shrinking. Like elementary school I have

shrinking. Like elementary school I have like 10,000 friends competing for you know the spots for the middle school.

>> Then middle school is like 90. Okay. and

then like high school 25 that means vast vast majority of your friends lost the opportunity to compete >> and that's a very interesting thing I think it does to a child but then I also

like learned some like you know other side you know not just the math olympi when I was I think 14 15 I got into the Ross math program which is one of I think the best like high school uh math

camp uh in the states uh Ohio State University um I think my first trip to the United States um was that summer it It's like you know summer of like eternal joy like every day I will be

learning cool research math like they taught us undergrad math and they asked us to like deduce everything from the grounds up like we were asked to prove zero times everything zero um by like a

limited number of axioms and that was very defining. It felt very different

very defining. It felt very different from mass competition. It's not like how many people will win that award. It's

like there is a vast amount of math that you just have no idea about and you get to build it yourself almost like one brick by another right from the limited

number of theorems you are provided you prove new things. So we are given like about 25 30 problem sets and each of the problem set have problems that like are

probably just bookwork theorems and you would just learn it in college but instead of presenting it as something that is like a given fact it asks us to prove it. So we our world of

prove it. So we our world of mathematical knowledge is constrained to how much we can prove and that's actually what's going on right now with action prover like action prover has access obviously to a lot of the words

information but because the lan data is so scars it's like a lot less than say the amount of code data out there um it's only two-digit million number of tokens out there in the open open world

action Imper learns to prove things and it kind of self-improved in a way where all the things that it proved got fed back into it into a kind of a skill library can be like apply for the next

challenge. There's also this sort of

challenge. There's also this sort of like self-challenging conjecturing component that keeps giving it harder problems just like my camp counselor gave me the problem set. And this is a

very beautiful process. I think like without this sort of right order, sequential order of introduction, I wouldn't like kind of go this far in

math or love math as much as I do. Um I

think the sort of curiosity and discovery is a basic human need and that definitely exists in like back then the tinted child and that being used to

motivate and inspire u mathematical learning. I think that was a very

learning. I think that was a very beautiful process.

>> Amazing. And then um on um some other incredible things that you've done. So

you did um MIT in three years I believe.

Then you went to the UK on a road scholarship to study neuroscience. Why

neuroscience? Was it all part of a grand plan towards AI or was it just your interest naturally carried you? Yeah, I

think the roads program like did a really good job and probably too good a job to encourage us to just like shift direction. Like it has this sort of I

direction. Like it has this sort of I mean broad sort of belief that you need a lot of disciplines and studies to help you become a global leader. Um that's

what the road scholarship is trying to sort of nurture. People who have a background in STEM, they will encourage you to go into liberal arts. I wasn't

fully encouraged to go into liberal arts. So I picked something that's kind

arts. So I picked something that's kind of in the middle like neuroscience.

Obviously I think at Oxford I have a lot of math friends and so kind of still math was part of the equation. Um, I was also trying to apply math in my

neuroscience study specifically maybe because I just am afraid of animal experiments. Like I'm not going to I I'm

experiments. Like I'm not going to I I'm I'm probably just going to stay in, you know, data analysis, computational neuroscience. I was quite interested in

neuroscience. I was quite interested in topological data analysis and persistent homology and uh but later I realized I think it was like two three months after

the school year started I realized there's something called UCL Gatsby UCL Gatsby is this like premium like you know AI hub in London and um Oxford to London is a short train and there's so

many world-class faculties there like um doing really cool research in say like the radical uh machine learning um like you know analyzing the neurodynamics of

stuff. They're also doing like various

stuff. They're also doing like various other like applied AI research and some from like cognitive science motivation but but but really the core is core is AI.

>> Then you topped all of all of this with a joint PhD in math and JD uh in law at Stanford. All of this been fascinating not just in terms of

achievement but in terms of like range and um I'm I'm just uh curious like how you were able to do all of this and whether there's any lesson for anybody

else. I mean clearly there's an element

else. I mean clearly there's an element of like of the chart IQ but there must be something else. I I think there's a lot of things actually. My junior year, I mean my last year at MIT, I'm like I

kind of grew up with a very sole focus and goal to do mass olympiate and then do mass research and the very next step is to probably go to grad school directly and probably not even do the

rose scholarship. I'm not sure because a

rose scholarship. I'm not sure because a lot of the road scholars are like you know politicians or aspiring lawyers, judges. I'm like, I just want to have

judges. I'm like, I just want to have some fun intellectually.

>> At the end of the neuroscience, I was like, okay, I want to go to Stanford to start my math PhD, but also there's this incredible opportunity of Stanford Law School, literally one of the two, I think, first ranking law schools in the

country. And uh they have really good um

country. And uh they have really good um IP professors who marry like AI and copyright law. they have really good

copyright law. they have really good professor uh Mitch Pollinsky in law and economics where you basically are doing differential equations but you're like analyzing like difference and like retribution uh the ratio of each sort of

criminal law measure and there are a lot of like other things cool um methods to apply textualism to constitutional law that's very similar to looking up definitions in math textbooks and so I

was like okay that's very cool so I did my I mean the JD PhD is like you have to spend one full resident year in the law school so that was my first year I spent like one year being a diligent law

student. I was even trying to apply for

student. I was even trying to apply for clerkships. It was a fascinating year

clerkships. It was a fascinating year and uh I learned so much and then the second year which is kind of a very interesting year where I was browsing all the AI for math research paper and

realized that wait a second there's so many ideas I mean from draft sketch pool uh proof to to uh I think STP selfplace are improving there's so many exciting papers and I wish I just have the

resources in industry to like execute and that was like when I think very very soon after I just basically decided to do a like fully focus on the company.

>> Fascinating. Thank you for that. So let

let's um actually go to the into the product now. So we alluded to some of

product now. So we alluded to some of this. Let's unpack how it actually

this. Let's unpack how it actually works. So you mentioned there were three

works. So you mentioned there were three components. What is the architecture?

components. What is the architecture?

What do those components do?

>> So I think like our kind of very broad vision is that we are going to have a contractor, we're going to have a prover and then there is knowledge base. in a

way your knowledge base is like let me take a metaphor I think for the because this is like quite I think like in the niche area of like very like subfield of of AI but uh suppose you're like selling

on an ocean right and like where do you know where to go and sort of your ship um that basically decides where to navigate that's your conjecture and then you like you know sail and tour one

direction um and then you land at this island okay well like do you know if you have been on this island before you don't necessarily they know basically you need to look up your knowledge base

u you want to make sure that this is indeed uncharted territory and then once you realize that it is uncharted territory like how do you know if it's like say India or west Indie right like

so is it I don't know um is it going to have some rare metal um that's kind of where your prover starts coming in to basically prove this new conjecture that

is not in the knowledge phase that is mathematically correct and has merit and so that's kind of the and then there's auto formalization which is the ability to um reason across informal and formal

space kind of weaving all these >> uh great and so the conjecture part is it LLM based or are you in a completely non LLM world

>> uh so we do post training on say like you know open source like LLM >> okay so there is an LLM so how does that work then what creates the conjecture is

that based um like what what what goes into it >> yeah I think I would say here like the conjecturing part is still the underdevelopment part like we have been in the last I think seven months very

focused on prover and also made a lot of progress on the knowledge base so so in the pandmic exam right you don't need to conjecture you have 12 problems they're incredibly hard and they are like you

know basically test for your prover so action prover uh tried on pandmic exam got perfect score the the kind of you know underlying system is a system of

ensemble of models and there's also a set of deterministic tools and also there's like a proprietary data set that's very large. So um kind of a

combination of these three things that led to that success specifically um I think that for the deterministic tooling it's quite interesting because these are

actually written for lean in the language of ling so um a bit like meta programming uh and that's that's very interesting we are actually going to release them uh on the public like API

on these all these those end of pools uh very very soon beginning of March right >> um >> is that a big announcement Yeah, today on the podcast >> I mean it's uh releasing the infrastructure for mathematical

reasoning. Um it's called Axiom Lin

reasoning. Um it's called Axiom Lin Engine Axel. It's um interesting because

Engine Axel. It's um interesting because there are a lot of sort of grassroot effort from the open source community to try to provide infrastructure tooling

for Lin the proving because LIN is a really sort of you know it's a relatively new language and there are a lot of reasons why uh it could be a bit

slow sometimes. Um there could also be

slow sometimes. Um there could also be you know things where if you assume like an axiom that's mathematically incorrect like if you assume n plus n equals n then you will be able to prove 2 plus 2

equals 2. You don't want that right 2

equals 2. You don't want that right 2 plus 2 equals 4. So a lot of the sort of like verify verify prove is actually you know one of our prover tools that's about to be released and that's actually

um a 100 times faster than the other counterparts that are the open source like effort called comparator. So um a lot of them are hopefully going to make everyone prove more theorem.

>> And in this architecture that um you just described compared again to uh what seems to be becoming the norm in other parts of of AI for fundamentally this

pre-training LLM plus post-raining system. Is there a tradeoff to uh your

system. Is there a tradeoff to uh your system in terms of uh is it more or less comput intensive? Is it uh more or less

comput intensive? Is it uh more or less uh fast or slow? We we had a little bit of a sort of co-star problem, right? I

think the data was quite quite scarce.

>> So well there are more than one trillion tokens of code probably a lot less um for lean. So we had to basically take

for lean. So we had to basically take where data to generate a lot of lean proprietary data.

>> Um so that's one difficulty >> and how let's uh double click on that.

So how did you do that? So so you created synthetic lean data.

>> That's right. So it's it's interesting because you know when people talk about synthetic generation in the unverified domain is you really don't know the quality right like you how do you know

the synthetically generated financial advisor data is like actually good then they have human experts to try to label it and grade it. Here you have lean so

you know that your thing is correct at least and if you do good quality control on the statements then you will have things that are of mathematical merit.

And um when we kind of take data beds, we use things like all the formalization to convert existing math from informal language to formal language. We also do

things kind of that are more formal system inspire such as repair fuzzing is actor to make there a lot more synthetic variants of the existing formal data

that we currently have. So the other difficulty I think is like lean runs on CPU and then the sort of LM par runs on GPU. So you have a little bit of uh CPU

GPU. So you have a little bit of uh CPU GPU means engineering uh just like a very interesting effort where ideas are out there. You need a very strong

out there. You need a very strong industry strength engineering team to execute the many good ideas maybe some academia researchers have produced some of our researchers have produced this

sector in terms of kind of how computer intense it's not like horribly comput intensive like definitely not compared to pre-training I think that like data

is a large part of it I think that like good sort of infra engineering is another part of it >> so as I was researching this there were some numbers

on a putnham question basis where there were millions of tokens. Give us an a sense for like the order of >> really really varies. I think there are like you know there have been cases

where a heart problem takes like 1 million tokens and stuff but there are also like a lot of other things we could do. We uh in house have something that

do. We uh in house have something that can shorten proof. So for example you can shorten a proof significantly 20 times shorter. It's like different

times shorter. It's like different levels of how you would like to count like how kind of bulky a proof is.

>> And then uh still bearing in mind that you're a very young company, what is the current state of the product? Are you

mostly focused on MVP kind of product that can solve this amazing problem but that's not industrialized yet? What what

part is research versus what part is engineering and product? So far

>> uh we focus a lot more on I I say so there's this sort of like you know team of really strong machine learning researchers and engineers and they're all like both researcher and engineer in

one they're like really amazing um we have a lot of really good people from meta from Google brain from anthropic etc and we just um we keep hiring you

know more and more uh sort of frontier lab researchers um this part I think is like you know focused on developing the uh core capability of the system. So we

want to basically push the the goalpost like forward right. So from putnham perfect score that was four months in then two months later was the four research conjectures and then you know

during this middle we also have tested something that is transfer learning from mass to code verification. So another

evaluation on a community recognized benchmark. We want to kind of try where

benchmark. We want to kind of try where we can get because we have really great mathematicians telling us how we should think about certain research problem

target and we currently have really hard research math problems in house that we are tackling. It's showing some problems

are tackling. It's showing some problems is also obviously getting stuck. Um so

there's this part and this part is like you know the current focus of the company and once we know where the frontier is then we can try to say okay let's make it robust let's make it sort

of um production grade. So when 1,000 1 million people hit it, you know, it doesn't break. But but this part is kind

doesn't break. But but this part is kind of sort of an effort that's surrounding that. And sometimes people like jump

that. And sometimes people like jump between different task as well. Now we

learn something about the applied uh use cases. We also have a lot of subject

cases. We also have a lot of subject matter experts and we are hiring we are hiring subject matter experts to to join us to work on trip verification to work

on code verification. to just double click on something you just said. Um, so

is is there a long list of just pure math challenges ahead you know for the uninitiated? Is there an Everest in in

uninitiated? Is there an Everest in in in math? There is there is so roughly by

in math? There is there is so roughly by uh I mean journal submissions a lot of other factors obviously but uh I mean you can think about currently the the

batch of um papers axim prover has autonomously proven and mathematicians have written can probably get into journal of number theory journal of algebra like that level well that's a

very different question from endos of mathematics or js invention that's one big jump I think you know to get to that sort of result requires a lot of

pushing. And we are not pushing it to

pushing. And we are not pushing it to just chase the amazing feeling which is quite amazing of proving something that is like grand and open for a long time

but also at the same time we are basically teaching the model um things that it could not do before such as a more complex reasoning tree. So on the

easy end of the pandm we have 40 nodes on the hard end of research questions in-house we currently have a research problem with thousands of nodes. So it's

a much wider and much deeper tree >> and we want to see are we going to hit a limit >> or not. We currently are not seeing one.

So we we we really want to basically scale the complexity of the reasoning of the problem. We want to make the AI be

the problem. We want to make the AI be able to do library learning that is we have seen it actually quite promisingly auto formalize definitions which is really really hard. So in math you have

theorems proofs lemas propositions basically you have definitions and that's very hard to ground. Um, so you you want to be able to auto formalize

definitions. You want to be able to have

definitions. You want to be able to have the model system explore definition to they'll be relevant for for the proof >> to progress through this series of of

problems. So if this is not super GPU intensive and this is not super fairly >> and if you've built a way to create

synthetic data that that works, what is the fundamental bottleneck? Is that

doing more of the same thing across more domains or is there an architecture evolution?

>> There's scale up and there's scale out.

So we we're currently scaling up in difficulty. Uh we believe that is a

difficulty. Uh we believe that is a defensible mode. We believe we are

defensible mode. We believe we are currently doing certain things interestingly um and are ahead of the curve in terms of how we get rid of

running out of context these kind of problems. How we scale learning from experiences? how we scale inference. I

experiences? how we scale inference. I

think we are doing that and we are also scaling out in a way of both there are some mass problems they are not solved not because they are like or they're not auto formalized actually there there are interesting things you can do you can

choose an existing math result and try to auto formalize it or you can choose an unsolved math problem and try to prove it both are incredibly valuable I think people talk about unsolved problems all the time and there's a lot

of value in actually picking good targets to try to auto formalize it a lot of these are un unsolved or you know not completed um because they are very

complicated in terms of the sheer volume of that result. So that's kind of scaling out within the domain of mathematics and then there's also scaling out from mass to other domains

such as code verification um and then hardware verification.

>> Do you think that AI can uh win a fields medal? There is this friend uh who uh

medal? There is this friend uh who uh taught me a lot of things about math and he said that like you don't celebrate when you win the field medal you celebrate when you get into the short

list of fields medal. Uh so obviously there's like only a finite number of awards and I think that we really want action prover to be able to solve one

long-standing problem in mathematics that you can objectively objectively say even though if it's an AI you know or double blind whatever that will be in the short list >> and and just to unpack that why short

list why why is the >> because then there are reasons you know whether >> because then it gets political >> well not quite political I mean sometimes fairness for example of a certain domain just got you know it's

Yeah.

>> Yeah. But to

>> but the short list that is sort of the objective standard >> and and and to the broader creation that I guess we alluded to a little bit earlier in the conversation of just uh

creating brand new sort of groundbreaking science like do you think AI is well on its way? I mean obviously it's doing some but like in terms of

humanity altering kind of groundbreaking discovery >> the first couple well not the first couple months a couple months before we actually start executing it was

incredibly exciting for me on an intellectual level like every day I have this sort of excitement like it's like I drink like six cups of coffee kind of

excitement for months and and the main source of that excitement which I would tell tell you actually about you know my my colleague uh Shoubo good friend uh

he's excitement of this in in a bit but my excitement is like just like we're now realizing that we are at the threshold of mathematical renaissance we could also be at the threshold of

theoretical discoveries in science mass massive massive scientific discovery at the theory level and and I think what I

mean by that is we have been in a very mass poor board the supply of outlier mathematical reasoning skill is so lacking that people are like in a

scarcity mindset like you will like hear discussions of oh like this problem is so interesting unfortunately I'm solving that problem they should all be solved

everything that human mind can conjecture find interesting find tasteful could be solved by hopefully majority of

them by improver And then you have the question of hypothesis when they talk to mathematicians um generally they will have interesting opportunities for

collaboration like I actually have this paper with professor Kenono and and others uh Shingong Jang and uh uh Michael Merren uh which addresses like the elliptic expansion moonshine

conjecture and that kind of stem from like you know three I think three theoretical physicists they they conjecture this based on their observed or like physics like phenomenon that

that I know frankly not not not very much about but I can solve the math part. They come to the conclusion that

part. They come to the conclusion that what they believe are a beautiful phenomenon that they find it worthy to formulate as a conjecture and publish as a paper have a proof because they know

some mathematician. Well, that that that

some mathematician. Well, that that that doesn't seem right. Like I think that the the really the beautiful vision is for all the theoretical problems, all the curiosity, all the lack of

understanding to be resolved in a satisfactory way across all scientific subjects >> and beyond this right there are things that we still cannot solve that we will

get a closed form sort of not a close form solution we'll get a very like you know approximation as precise as possible I mean there's a lot of value for example to know Say

what is after the 1,000 or 10,000 digit compared to what is after the third digit. The word is actually a lot of the

digit. The word is actually a lot of the times not diminishing return. The last

mile carry a huge amount of value like in search for example if you cover some edge case you likely win you you will be a market winner. In for example writing right if you write just that extra bit

or any sort of creative art getting that extra mile correct or or done has a lot of value like optimization you know precision. We we can try a lot of these

precision. We we can try a lot of these things as well. And then as math kind of helps with both first principle understanding and trial and error, it just kind of this cycle like you have you have some first principal

understanding, you try testing it, you try some trial and error and you maybe give some sort of you know risk bond uncertainty principle um robustness estimation and and then you go back to your first principles and then you go go

to your trial and error again. You have

this sort of circle of of discovery and this is really not not the end of it. So

that's that's why I'm already very very excited. I think this is going to be

excited. I think this is going to be amazing. Ideas can diffuse between

amazing. Ideas can diffuse between different fields a bit like you have like abacus and now you have like trade and commerce. You have uh calculus

and commerce. You have uh calculus integral integration. You have like

integral integration. You have like thermodynamics mechanics industrial revolution, you have the Babage engine which is to calculate lock tables faster and okay well you have the prototype of computer science. The rest is history.

computer science. The rest is history.

You have number theory, you have RSA, like you have all these kind of mathematical tools, you know, kind of open up new discoveries and new use cases and in turn demanding more

mathematical tools and beyond this cycle and this cycle marrying science. Here

comes code. We haven't even talked about that and that's why actually Shubo is very excited. Uh so Shubo CTO of Axium

very excited. Uh so Shubo CTO of Axium before that was like you know long-term like meta veteran. Uh he was an IC director. He believes in code is math.

director. He believes in code is math.

Okay. So, so through through all my good friends telling me about lean telling me about Curry Howard correspondence, I believe math is code. He believes code is math. What does that mean? Okay. So,

is math. What does that mean? Okay. So,

it means that you can try to fulfill the dream of Donald News literary programming. Have computer scientists,

programming. Have computer scientists, programmers enjoy the luxury of mathematicians where they can read in a natural language.

>> And this is kind of starting to happen, right? Web coding like front end, right?

right? Web coding like front end, right?

Like you know, we can have very cool like glovable websites. But like how do I v code a nuclear reactor?

>> How do I v code control flow?

>> How do I v code complex systems that require like quite honestly superhuman hierarchical reasoning skill?

>> It's interesting because you're not in code alone. You have code and you have

code alone. You have code and you have math. So you have in addition to the

math. So you have in addition to the flywheel we're already seeing in the coding companies an additional layer of flywheel of verified code and the sort

of mass start to come in and these kind of flywheel of data keeps compounding you have actually two or even if you're counting the science part three orders of flywheel. How far do you think we are

of flywheel. How far do you think we are from that world where we have already >> that's why we have to execute like you know something every couple months like we have to move extremely fast like

there's so much to do I think Axiom is a very very young company and we are at like you know the very very beginning tip and and we are already I personally feel some sort of shock and emotional

response and I know some of my mathematician friends Scott commoners who's a Harvard uh microeconomics professor also Morgan Prize winner we're good And we all have this sort of

emotional response when axi prover approved fa conjecture proves that almost all primes are partially regular partial vendor conjecture which is one part of the original vendiver conjecture

that have been open for 90 years. The

parity of differentials um for services genius zero and one by algebraic geometry paper. We are really just

geometry paper. We are really just leaping across a point. I mean pund marked I think the end of AI trying on mass Olympia. We are very glad that we

mass Olympia. We are very glad that we got a perfect score. It's a really good period point. Pundam 2025 is by a lot of

period point. Pundam 2025 is by a lot of sort of experts grading harder than IMO 2025. So it's a hard hardest reward mass

2025. So it's a hard hardest reward mass Olympia test. And now we are leaping we

Olympia test. And now we are leaping we are leaping to research. And I think I'm going to have another similar emotional response if it really does solve one of those breakthrough mathematics problems.

Interestingly, I think there are a lot of experts in domains that are currently overlooked by a AI development. So, so

if you're a software engineer, you feel like, oh, web coding really change and improve your quality of life in a meaningful way. There are people who are

meaningful way. There are people who are in industries where because of lack of provable guarantees, they couldn't use AI. And there for example, Aerero Astro

AI. And there for example, Aerero Astro for example like I think defense um for example there is no partial credit for mostly verified GPU is a all or nothing

>> or mostly flying plane.

>> Yeah. Yeah. Yeah. A mostly verified formalized hypervisor. I think for these

formalized hypervisor. I think for these experts that are currently kind of handholding a lot of the traditional goals their life has not been changed.

And I want I want to see I want to see the AI for math movement that Axiom is you know hopefully leading and to to transfer to these domains and to try to solve some of those problems as well.

>> Speaking of emotional response is the entire math field super excited about uh math AI or do they feel like the rest of

us possibly uh disiniated and replaced by AI? So I think a lot of the like

by AI? So I think a lot of the like adverse reaction about um from the mass community about AI is actually coming from the fact that they cannot verify an

informal solution. So suppose like GPT

informal solution. So suppose like GPT generate a mass proof a million lines.

No one's going to check that like I I'm not going to check that like you know like I know there are a lot of really great sort of data labeling you know services. They couldn't have that sort

services. They couldn't have that sort of level of expert to verify proof of that link. It's just hard to do. On the

that link. It's just hard to do. On the

other hand, if you have a formal certificate like a stamp certifying that this is a correct link proof, I think people are a lot more receptive to it.

That's why actually a lot of mathematicians, especially almost all of the new school of mathematicians are accepting lean. Uh what they want to do

accepting lean. Uh what they want to do is to have human to formalize lean. Now

it's really fun for humans to do lean.

We have a lot of the initial mass li people here at Axiom and it's a very fun team to see them formalize some statements. But when when it comes to

statements. But when when it comes to say like hundreds of thousands lines of link code which is already not a hypothesis like automated reasoning team

at some big tag currently have 260,000 lines of their improving code not lean to to verify one component of a hypervisor or CPU utilization. So so

that that cannot I mean that they actually did write it by human but it's just not quite sustainable. So maybe uh just to close just one sort of final chapter in this conversation. So while I

was uh listening I was thinking about um how someone with such a deep background in math becomes a CEO and what that transition was like and whether there's

any lesson for anyone uh considering making that job or you know or any founder out there. I remember that like reading the like anecdote of Hamilton

that he writes down all his like flaws and shortcomings every night and forcing himself to correct correct them. I I

know what my like kind of habits and flaw shortcomings are. I'm a very spontaneous person. I I don't have the

spontaneous person. I I don't have the best ideas when it's planned. Uh which I think sometimes that's like you know in the course of research you have like math research. you have these kind of

math research. you have these kind of very interesting Eureka moments I think.

So I try to overcome that in my day-to-day. I try to do scheduling very

day-to-day. I try to do scheduling very intensely. I try to surround myself with

intensely. I try to surround myself with people who inspire me to execute faster.

And that's basically the entire team.

And I think it's a great honor to be working with them every single day. I I

think like I I go into the office and I look around and I hear the discussions and I'm like, "Wow, I'm like so I'm I'm so lucky to be here." Uh, and I think that's something that in this kind of

talent market, I think people like to work with people who value their intellectual judgment, >> respect their voice and opinion.

>> And I think Axiom has this sort of very flat like non- hierarchical. Everyone's

a member of technical staff or a mathematician, right? if you're earlier

mathematician, right? if you're earlier founding plus that um this culture is really great for sort of I think the sort of open communication of ideas and debate of ideas and >> and that helps with the pace

>> it helps with the pace of iteration uh helps with being more correct a lot of things I'm learning very rapidly I mean it's been very interesting roller coaster like 7 months when I was in math

I mean there's this sort of idea where um you have like taste and uh sometimes these taste are can be interpreted as arrogance and I learned that ego is a

really really bad thing and we should just basically get rid of it.

>> Do you hire people for taste and if so how do you evaluate it?

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

>> Okay.

>> And I think that's a very interesting kind of >> how do you select people? How do you evaluate someone's taste? Is that their prior work?

>> Right. So, so one is basically that means I have to learn every day because I need to have a certain ground you know a basic amount of taste and also the

other people who are senior the the company uh need to have research scientists have need to have that sort of amount of taste and what makes us excited and when we are excited we just

go after that person um we have had >> a lot of uh I think extraordinary hires from amazing and interesting backgrounds And we we we like we really like this

team and I think that we raise the bar for hiring actually um continuously. So

uh we we recently have a uptick in the number of people who who like to join us and our candidates that we excited about. We we take recruiting very very

about. We we take recruiting very very seriously. And how did you secure that

seriously. And how did you secure that founding team uh initially because um that's kind of ridiculous in terms of

like caliber of just world class mathematicians world class. How did that all come about? One of them was your mentor, right? So now technically you

mentor, right? So now technically you mentioned you very flat but like technically working for you as CEO, right?

>> How did that come about? So um quite interestingly I think at the start of this um I realized that there is a movement and this movement of AI for math is very much by and large in

academia or actually people are hiding in in labs like secretly doing AI for math where their like day job is something else. Um so when I talked to

something else. Um so when I talked to each of these people like it was a very I think mutually exciting feeling from both parties and basically it's like two veils and just kind of realized that

only they can communicate in that like frequency range and that happened like multiple times. I got very inspired by

multiple times. I got very inspired by this like I think there were a lot of times at the beginning where fundraising was quite hard. I think I mean I'm I'm I'm a nobody. No one should trust me with their large amount of money and uh I think that was very difficult and

challenging but it was those conversations that basically made me realize I have to do this. I just I just have to and like you know and I have to be the best deal for this for this team because my team deserves the best of the world. And those kind of like you know

world. And those kind of like you know intellectual alignment were like a main theme. And the other thing I realized

theme. And the other thing I realized was they they found say the maybe the other AI for math opportunities is not not particularly attractive for one reason or another. maybe they don't want to move geographically to to London or

to China or uh maybe uh you know it's just a different kind of vision. So kind

of gathering them was relatively natural process. Um and then after that I think

process. Um and then after that I think when you have a bunch of really smart and nice people you just attract other like smart and nice people and

especially people who are um adventurous like rebellious people like to disrupt who come from cogen want to disrupt cogen people who are come from math want to disrupt math and disrupt and I guess

like elevate as well because they do have a lot of like affection still with that field so I think it's a very interesting it's almost like a tribe I seem like tribe and we have more and

more people joining us and sometimes I feel like both in those initial conversations and still now and and even after all these sort of like you know talking to the world about what we are

doing we still feel like secret keeper we still feel like we cannot fully elaborate and emphasize the thing that we are seeing that is the next frontier of AI that is a generation and

verification loop >> that that is the discovery of verified knowledge >> feels like a wonderful place to leave it. This is all incredibly fun,

it. This is all incredibly fun, compelling, and inspiring. Thank you so much for spending time with us.

>> Yeah, thank you so much. Yeah.

>> Hi, it's Matt Turk again. Thanks for

listening to this episode of the Mad Podcast. If you enjoyed it, we'd be very

Podcast. If you enjoyed it, we'd be very grateful if you would consider subscribing if you haven't already, or leaving a positive review or comment on whichever platform you're watching this or listening to this episode from. This

really helps us build a podcast and get great guests. Thanks, and see you at the

great guests. Thanks, and see you at the next episode.