Latent Space: The AI Engineer Podcast
Hosted by Alessio Fanelli
Watch the full show on YouTube: https://www.youtube.com/watch?v=xlXIi6GZNGY
5,520 words · 3 speakers
Speaker names marked ? are inferred from speaking time and the show’s known hosts — they are not voice-verified.
Hey everyone, welcome back to another Lit and Space Lightning Pod. This is Alessio, Partner and CTO at Decibel, and I'm joined by swyx, founder of Small AI.
Hi, hi, hi. We are very happy to finally have Dr. Jasper Zhang of Hyperbolic on the pod. Welcome.
Thanks for inviting me. Great to be here.
Yeah, the story of Hyperbolic, you know, I feel like we will do a full podcast on Hyperbolic at another time. But maybe like a quick two seconds on what's hyperbolic and then we can go into the IMO stuff.
Yeah, sounds good. Yeah, so I'm the CEO and co-founder of Hyperbolic. And I face like a lot of pain when I'm trying to get access to GPUs during my PhD time and also my CRL time. So I decided I want to make sure that any AI team who want to build or use AI in the future, they won't get constrained by compute. And so we decided to build Hyperbolic, which is the on-demand AI cloud made for divided person. So everyone can get fast, affordable access to compute and inference.
Yeah, by the time that we release this episode, we should be publishing Jasper's talk at AIE as well. So you can go over to his talk and see more about the story there. But we're actually coming here today to talk about something slightly different, something that you also have experience in, which is Math Olympians. And maybe, yeah, you know, the sort of headline, not to bury the lead, is that, you know, both DeepMind and OpenAI have claimed to have gold medal level performance at the IMO. And then you started being like super involved in like sort of breaking down what the story is. Maybe can you sort of recap what happened and then we can go from there?
Sounds good. Yeah, so on Friday, so I like participating in different Math Olympians in the past, won a few gold medals. And I have a lot of friends who actively involved in IMO. And so I was just chatting with my friends on Friday and around like 3:00 PM, one friend told me-
Me that wow, uh China team won the IMO again, uh uh and and also uh DeepMind also won the gold medal. And uh so I just started posting on X. I mean, I tried to let everyone knows the news. So uh I posted on X. Uh some people got excited, but then never confirmed by DeepMind. And so it's a little bit, a little bit weird because I thought like DeepMind was the, would be the first one to kind of announce that news. Uh and then uh at at one AM Saturday, OpenAI starting uh starting posting, a lot of OpenAI people starting posting about like
them winning the IMO uh IMO gold medal and kind of like stole the the spotlight. Um and so I initially thought Google was just slow due to their marketing approval, like the process. And so I posted another one to just like share my thoughts. Uh and then I got pinned from Google, like someone, someone from Google just told me that it's actually like IMO and Google themselves need extra time to verify. Um and so like kind of raised a question to me like, why? Why did mine need to verify, but then uh OpenAI didn't, didn't need to do that? They can just release? And then it turns out like OpenAI uh actually didn't involve officially with IMO.
They just like use the the problems, but and then um just like use their model to test the the results and ask like three previous uh IMO medalists to review them. Um I think I I read, I read the proof, the uh it's still correct, uh but it's just like less official. And that's why uh people kind of like, kind of, OpenAI re- re- receive a few backlash uh over the weekend. And on Monday, DeepMind uh officially confirmed uh they have the gold medal uh and uh also fully verified by IMO.
Yeah, and I mean, so congrats. I I I think, you know, like, the relationship between OpenAI and IMO and all that, I I honestly, it's a that's between them. The what matters is that they have a model, both both labs independently achieved a model that reasons in natural language. Uh, you without internet, without tools, uh, which I think, you know, this time last year, it was we didn't think was possible.
Yeah, so, uh, I have a feeling that this year, uh, there there at least like an AI model can win, uh, can win IMO gold medal. Because, uh, last year, uh, by using like formal verification, formal language, uh, Google DeepMind can uh, already won a silver medal. And, uh, so maybe I should share some background about IMO. So usually, uh, IMO is basically the uh, the top tier competition, uh, for high school students, right? Uh, it doesn't require you to really understand like the advanced math. It should basically, it's problems about
uh, simple knowledge, like common semantics, uh, number theory, geometry and algebra. Uh, but then it kind of require you to have very strong problem solving skills. You need to know how to do contradiction, you need to know how to create like counter examples, you need to do like observation, etc. And so, uh, people treat this as like the, uh, one of the the bar for AI to hit. Uh, before they become the real mathematicians in the future. Um, so last year, Google already won the silver medal. And, uh, seems seems to me that they already figured out a way to to to make it work. Uh, it's just like need a little more time, a little more resources, a little more data, a little more compute.
And so, uh, naturally, I I would say, uh, Google will win gold medal. What's surprising is this time they don't use formal language, by instead they just use L M. And so last year, when they tried to do, uh, the IMO, they need like a, uh, like a human to kind of translate the natural language problems to Ling, and then they use Ling to kind of prove the the the problems, uh, to prove the, uh, solve the problems and and this year, uh, no longer need need that, and the same for OpenAI too.
Yeah, I think that this dropping the need for lean and you know other other sort of specialized systems like you know I was covering this last year with the the Alpha proof and Alpha Geometry team and you know it seemed like a very complicated system some of these solutions took 60 hours which is way longer than the 4.5 hours that IMO limits have for humans and so yeah these these subsystems took up to three days and you know I think that's that's a huge step you know it's it's I don't even think it's like a incremental like oh scale this system more they
just have to throw away the whole thing and do something else and then I think also like I think people can also just look up the problems you know I think yeah what's what's cool about you is that you can actually analyze and study the problems I think that there's some different ratings of different pastries or different problems I think probably either problem two or problem three was like the quote unquote easiest and you know it's like it's like just a few paragraphs is not not not a not a lot but like it involves a lot of creative thinking right or what are they testing basically?
So I would say different problems having different skills for example like the the if you look at the problem one we can stop one problem one is like a combinatorial geometry so it kind of involves like integer you need to kind of it kind of asks you a question about the all the possibilities for different cases like for different N for the any any positive integer that greater than a greater or equal to three and so it requires you to find a key lemma which is like for any N greater than three like let's say N N equal to five you can
Reduce the problem to N equal to four and reduce the problem to N equal to three. And so this is, uh, there are different ways to do this like induction. Uh, but uh, like Google has one method and then uh, OpenAI uh, AI also have another uh, method. Uh, but both kind of works. Basically, you just reduce any N to three. And then you just do case by case analysis for N equal to three. And so I'll say, um, this is probably not that challenging. If you are very good, uh, like Math Olympians participants, but uh, it kind of surprised me that AI can can kind of come up with this. Uh, like ideas.
Yeah, it's it's crazy.
How do you think about rating like the taste? I actually used to do uh, Math Olympics too, but I got third. I never made it to IMO.
Uh, and so it's hard for me today to judge, but is it? How important is taste in your mind where, hey, you can actually take then some of these results? And maybe build on top of it versus sometimes it's kind of competition for competition sake. You know what I mean? It's kind of like with code. It's like, hey, look, you just wanted to compile. Like, is taste created a lot in the competition? And is the useful? Or do you think we're better off every models that can just brute force some of these things? And we can focus on more interesting stuff?
Yeah, so uh, so I think, um, we we basi- I I basically think like, I basically look at my my journey from from like high school. I like high school to PhD, right? And I I realized that IMO kind of like it's a good exam to test certain aspect of math skills. Which is like problem solving or you need to have like really uh, complete chain of thoughts. Uh, like logic, etc. Uh, but it doesn't test like your creativity in terms of like research. It doesn't test your uh, Your your capabilities of doing conjectures.
Uh it doesn't test your uh capabilities of learning like advanced knowledge or like applying advanced knowledge. And so I think uh we probably should just treat this as like one step stone. For AI to become the real mathematicians in the future. And I would say most of the problems here are more like Brent Teeter's style, so like you can solve them. But it doesn't mean that you are good mathematicians. And uh and and yeah, I I mean, I mean, I can I can feel the AGI vibe from the solutions. But I think we're still we're still not there.
Uh yeah, I mean, uh you you did the CMO, right?
Yeah.
Uh your your your background. Uh how does it compare, by the way, CMO versus IMO?
Uh so uh I mean, CMO is Chinese Math Olympiad. And so uh in terms of difficulty, uh CMO is uh kind of similar to IMO. Uh I would say it's super competitive in China. So there is a saying like if you if you if you guess it's harder to get selected for the national to become the national team. Instead of uh than like getting getting the gold medal IMO. And so so it's similar. And I I mean, like, there there are many like uh it's it's all about probability, like. There are so many people can compete as CMO. And so like a lot of students are pretty good, but just like six people um was selected.
Yeah, yeah, um I mean, that's uh that's also very common in terms of any elite institution. It's harder to get in than it is to uh come out of it. Um, okay, uh any other like any other overviews of the IMO problems? Uh I I saw some I saw a minor piece of discussion around how the the five problems that both AI solves were of the same kind, or or the sixth problem was like a clear discontinuity. Uh which I think is normal, right? Like IMO always has a sixth problem that is like challenging. Um this is part of like the Ilija Yudkowsky Bet. Um but like I just wanted to, you know, you you you perhaps you you're kind enough to prep some show notes which which we're gonna publish.
Um but you you actually had some analysis of like the the the problems and maybe you wanna sort of talk about uh what you thought about the problems.
Yeah, so I'll say, uh, so in for IMO, there are like four, four categories, right? Algebra, combinatorial, geometry, number theory. Usually, combinatorial is, uh, is kind of more, the most challenging and creative. Especially for AI. So like, at one time, I, I was at like this conference, which is a frontier math symposium. So basically, they invited like, uh, thirty to forty mathematicians to kind of assess the capabilities of uh, of many high and many other advanced AIs. Uh, we realized that if, if it's like a textbook stuff or like, uh, step by step, uh, problem, then, then it's, AI can solve it.
But however, if it's require like creativity, uh, especially like in combinatorial, so you kind of need to create uh, some example and then try to prove them. Uh, that it's the minimal bound or like the upper bound, uh, it's the lower bound of the upper bound. Then AI kind of sucks at that. And so I think, uh, this is why no AI can solve the last problem. Uh, but it also is super hard for human as well. And, and like, if you look at the first five problems, you can, basically, when you look at a problem, you already know how to decompose the, uh, how to decompose a problem into several steps. And then you, you know that if you can solve each step, then you can solve the whole problem.
Uh, but then for the last problem, you kind of need to do a lot of uh, experiments or like, you need to look at this smaller examples and try to create some example, try to create some solutions for that small examples and try to figure out if you can prove it, uh, that is the, is the minimal bound, minimal number.
How do you think we can get the models to do that? Do you have any intuition on how to get there? Or AGI? Do you have any idea of like, how can we get the models to solve those problems? Is it just a matter of better RL? Is it something fundamental about what data they need to get? Yeah.
Yeah. So are you talking about the Komben of Torres problem? Or like the real research problems?
No, like these problems that you're saying, the format. You're busy saying, look, if the type of problem is this type, the models are not good. Do you know why that is? Or how we're gonna get them to solve them?
Yeah, so just kind of come to one thing that I'm just like doing as a hobby project, which is like, we think we need a better benchmark for math. Right? Like, most of the benchmark that people are using right now is like AME, IMO, USAMO, all these like competition math problems. But like, they just test like a certain aspect of other math skills that a mathematician have. And so what we're doing here is like, we really want to think from first principles, like what makes a human a mathematician? And then we break down all the skills that are required for a human to become mathematicians.
And then we kind of create problems or like benchmark based on those categories. And so we kind of, right now it's like still in progress, but we're working with like several PhDs, professors and like AI researchers in different AI labs together to kind of, to produce like this more holistic benchmark. But basically, we kind of organize the skills into three categories. So one is mathematical knowledge and understanding. And so you need to know all the math knowledge, like definitions, theorems, lemmas, etc. And you also need to understand theories, right? Like, how to apply them, why they're true, what are the history of those theory?
And you also need to understand how to do calculations. You know how to do like analytical skills, etc. And then the second is like problem solving and communication. So you need to kind of have a holistic problem solving framework. Basically, you want to understand the problems, you need to, you need to know how to explore examples. And you need to know how to apply key strategies like contradiction, decomposition and analogy, etc. And the same, and then also you need to have logical thinking and you need to be very good at writing and presentation. Then I would say for IMO, uh, problem solving and communication probably is the, the most skills that you require. Uh, and then lastly is like learning meta skills and creativity.
So you need to know how to learn new knowledge, you need to know how to, uh, you need to how, how to think abstractly. And then transfer tools across domains. For example, like you want to use probabilistics method in carbon cars, then you kind of know how to do this transfer learning stuff. And, uh, and a mathematical modeling, right? You need to how to translate real world scenarios into formal mathematical models. Uh, and then generalization, which is you look at a few examples in base, you immediately come up with an idea. Okay, I can generalize this to a more powerful theorem and see if I can prove that. Uh, and, and one, one, one very important piece of mathematician is like creativity.
So you need to very, very creative, like when you look at, look at, at one object or one example, then you basically say, okay, now I think. Uh, I can invent some new methods and you can invent some new theory. Uh, and lastly is like intuition. So you look at the, for example, the geometry, you look at the geometry problems and you kind of already know, okay. These, these two line are parallel or these two line are perpendicular or, uh, even just look at algebra problems and. And you know, like, okay, this, this group has this structure. And so those are like the main pieces, uh, I think will define a mathematician. Uh, and then in terms of how we are, we can get there, um, and it really depends on different skills.
So for example, uh, for the logical thinking and reasoning, I think we can, uh, a lot of people trying to use Ling. Because like. I L works super well for verified demo. And so if we can just use link to kind of become the verifier, then uh it's it's easy. So I think uh we probably will see very powerful reasoning models uh in in term in math uh very soon. Uh but then and then for creativity, this is a little bit hard because uh there is no measurement. Increase temperature.
Increase temperature.
Yeah, this decrease temp. No, we want we want it to be more. Increase. Increase uh but then you also need to uh have the the taste like right. You need to know like which direction is right, like this is a common uh problem in I L. And so I would say uh you need a new way, like you need to define a new reward function to kind of capture how good this model is uh in terms of creativity and uh and just like in these times, you need like specific domain knowledge to kind of create this reward.
Uh and I I I think I started seeing more and more mathematicians working together with A I scientists, researchers. And I think this is a good combo because there there if you are just like A I researchers, you actually don't know what makes a mathematician good. Then there's no way that you can come up with a reward function well. Uh but then if you're just a mathematician, you maybe know the the concept, but you don't know how to apply that to to A I research. And so uh so basically, I think we will see, we will start seeing more and more mathematicians working together with A I scientists. And uh my my guess, I mean, different people have different opinions. And then my guess is I believe in I L.
So uh if for each category, we can figure out the a way to auto evaluate the results.
Then after that, it will just be compute and data.
Yeah, I just want to offer a few links for listeners and viewers. This is the symposium that you went to two months ago, and these are the people involved. And this is obviously leaning on the frontier math work that was done by Epoch and OpenAI. And this is some example of the kinds of problems that they're working on, which is like not even English to me.
But like, yeah, I mean, it's, I think it's very nice how you broke down the different levels of reasoning. I feel like this is very cool in a sense of, yes, this is particularly applied to math, but it does generalize. It does generalize to like, this is how we, these are like the higher level skills of intelligence other than predicting the next token. That, that, you know, that people wants. And, and so you have a framework of like, you know, knowledge and then going all the way down to communication, which is actually really cool to me. I'm gonna think about that a lot more.
Thanks. Yeah. Stay tuned. We probably published the first draft, first version in a few weeks.
This is a different work from, from the frontier math people?
Okay, okay.
It's a so frontier math, still problem focused, but then I think we need more skills breakdown.
Yeah. Is this like, is this related to hyperbolic at all? Is it like a personal project?
So, I mean, hyperbolic, the goal of hyperbolic is that we want to democratize AI innovation and try to accelerate AI evolution. And so I will position this as a hobby project, but
Okay.
We, we will probably give people some credits if they actually can solve. We will give some researchers some GPU credits if they can actually solve some problems in the benchmark.
And then I think the, the last follow up I had was about a comment that you made, maybe like three comments into your, your comments. Which is about, about the usage of lean and, and like sort of verifiability. I saw some mathematicians actually say like, so, okay, on the one hand, if you're very bitter lesson pilled. And if you're very pro scaling AI and all that, it's a win to reason purely in natural language, purely within your weights. No, no tools, no, no, nothing. Um, you know, the OpenAI output was very raw. It could have been fine tuned for human reliability, but like it was still, it was still fine. Like it still got the right answer. GDM was a bit more polished.
But ultimately, the, the, the answers were hard to verify. You had to have, you know, you had to hire like three former IMO gold medalists to go and read it. And then say like, yeah, this looks right instead of like, no, they didn't get lucky. Or like, or like they just got lucky, right? And I think like the, I saw some arguments from mathematicians that are saying like, actually using lean is good because then we can trust that that is uh good reasoning. You know, do you have any perspectives on that stuff?
Yeah, I think um the different approach have different challenges. Like uh natural language is easier to get a data, but it's harder to verify. But it it's more human readable, right? For lean, um there, there are not enough data for lean, right? There are like probably one million tokens uh in uh about lean right now. And, and I know a lot of like professors and PhD researchers are trying to build the biggest lean data set in the future. We, if we can reach like one trillion token, I think then you can start doing some cool AI training on top of that.
And but uh but I think that's like a more, personally, I feel like it's probably a more clear approach. I was super surprised when I saw OpenAI and Google DeepMind didn't, didn't even use lean and can solve that. And as many of you know, like AI neural networks is basically a black box and it's like a experimental science. So I, I can't make any prediction whether we will start, we will first see like a mathematician AI built on top of lean or built on top of natural language. But um by general, I feel like both approaches might, should work.
And I, I think mathematicians would like both of them. And besides that anecdote, I know some professors at, in, in London are trying to using, uh using lean to write the proof for Fermat's Last Theorem. And so that's, that's pretty impressive if you can, you can do it.
Do you think, do you think it's possible? Uh, I, I mean, I, I knew that, uh, Fermat's Last Theorem has been proven.
Yes, I have.
But also, I, I don't know if Ling is, you know, complete enough to, to get to that level.
So I would say, uh, it's, I think definitely possible.
Um, yeah.
Like, he, he, so the professor is Kevin Buzzard, and he got like a grant. And now he's just like focused on writing the proof for Ling.
Wow.
He's hoping to finish that in like two or three years. Uh, and, uh, and then basically like if Ling is not complete, then he can just build more.
Yeah, more libraries on top of that. So, so everything is doable. It's just time. And I think he got time and he got, uh, resources. So I'm very excited to see that happen.
Okay, cool. Well, I'm looking forward to the, the skills breakdown. Um, we'll, you know, share it whenever it comes out. Um, any other, uh, thoughts on, on just this IMO chapter of, of, uh, I guess the 2025 edition of the IMO? Uh, you know, any speculations on like what breakthroughs either lab has done?
Can, can you say that again? What do you mean by breakthrough?
Do you want to speculate? Uh, is there, is there any credible speculation on what has been the breakthrough that?
That.
Um, that either OpenAI or GDM have done in order to achieve this? Like, um, you know, they, they, all they say is like, oh, we scaled test type scaling more, but like, I don't think that's enough.
You don't think that's enough? You don't think like, uh, I, I, to be honest, I feel like a lot of, uh, AI. Uh, like, uh, a lot of AI models built in industry is just like a bigger scale of. Uh, of like, uh, in, uh, like research results. They, um, the, probably they will use like existing research, but it's just more.
More like larger scale, more systematic and more data. Um, I mean, I know, um, I know, uh, when I read like the Google Deep Mind report, they said they can, they can now do like parallel thinking. Basically, the, the model can, um, can like parallelly try different new ideas. Uh, they try to like leverage more multi-step reasoning.
Uh, sorry, they, they try to like figure out new reinforcement learning techniques that can leverage multi-step reasoning. I think that's probably like a, a very important, important step. Uh, I know, uh, I always pretty bad at multi-step, uh, but now seems like they, they figure out a way to kind of, uh, train, uh, using I R for multi-step reasoning. And I think that's like a pretty impressive in terms of the, the solution. Uh, and, uh, but then I, I would say most, none of this will probably worth like the best paper in at new herbs, but it's more about like it just be the best in terms of each technique and just get more data, get more compute.
Yeah, a lot, a lot of people are focusing on this sentence where they say, we provided Gemini with access to a curated corpus of solutions to math problems. And they were like, oh, okay. Like you, you train on test.
It's not.
Uh, but no, but the, uh, I think a smaller cover story that people may have missed is that there was a second Gemini model that was also submitted to IMO, uh, with no, no pre, uh, in context learning and they also did got the same result. So, uh, yeah, that's, that's, that's a big win. Um, yeah, I think it's reasonably, uh, known that Deep Think and O three Pro, um, and uh, Grok four heavy are all like parallel thinking, right? Like they, they all just run like 10, uh, different variations of the, the, the same model. And then they have a, a judge model choose the best result. Um, I, no, yeah, I'm not sure. Like I, I, I think that the existence proof that there's been something qualitatively different is the, is the wall clock time going from 60
hours to, to, you know, under four point five. That's, that's an order of magnitude change and it is not, that typically that is not achieved by scaling up, um, existing ideas. You have to just do new ideas because this is a, it's a efficiency, uh, issue.
Can we like, I mean GPU getting better, now you get B two hundred, it's faster. Uh, like even.
Is it one order of magnitude better? I don't think so, it's like two times better.
And then inference, inference speed also improve a lot, right? Like, uh, if you look at, if you want to run like Lama three and, and like now compared to now, it's like three X, two X better. So, so kind of.
Maybe, maybe.
Maybe, but I'm definitely agree. It's a, it's also like, um, the, the model is more powerful. And you can solve the problems faster too.
Uh, cool. Any, uh, what, what's next? What, what other like IMO, uh, what other math like, uh, you know, you, you have like frontier math. You have, uh, your benchmark that you're putting out, uh, any other like milestones that you're looking for in, in, in this part of the world?
Yes, uh, so I would say, uh, a lot of benchmark is just like, it's just like exams, right? Like, you take, the purpose of becoming a mathematician is not to take exams. It can give you like, uh, it's, it's the same for any, any, any job too. It kind of give you a, like a benchmark or like a, uh, like a matrix to see how good these model are. But you really need to put them into the battlefield, right? And, uh, the goal of a mathematician is you want to push forward the frontier of math. And so I would say the, the next step is trying to solve some open problems. That's like open for thirty years, fifty years.
And then I think the ultimate goal is to solve like a very challenging problem, like create a new theory. And then win a Fields Medal. That's how, how I define a math AGI in the, in the future. Yeah.
Field medal. Okay, let's go.
That's my dream. That's my.
Uh, cool. Um, Alessio, any, uh, party thoughts, questions?
No, that was it. Maybe I should go try back and do the problems this afternoon.
Let's, uh, let's solve some, uh, IMO problems together, together.
Awesome, man. Thanks for joining us.
Yeah, thanks for inviting me.
Page updated October 26, 2026 · transcript and summary are machine-generated