Latent Space: The AI Engineer Podcast
⚡️Math Olympiad gold medalist explains OpenAI and Google DeepMind IMO Gold Performances
Watch the full show on YouTube: https://www.youtube.com/watch?v=xlXIi6GZNGY
24 Jul 2025 · 33:07 · transcript: transcribed · original
Sign in to retry the failed stages.
Processing stopped. Claims grouped (TransientProviderError: Error code: 429 - {'error': {'message': 'You have no credits remaining. Add credits to continue using the API at https://platform.openai.com/settings/organization/billing/.', 'type': 'insufficient_quota', 'param': None, 'code': 'credit_balance_exhausted'}}) failed, and the stages after it wait until it passes. A retry reruns only what failed.
137claims extracted
2speakers named
35%of speech attributed
383transcript segments
Claims
In the order they were said
“so I'm the CEO and co-founder of Hyperbolic.”
Claim: Jasper Zhang is the CEO and co-founder of Hyperbolic.
“And I faced like a lot of pain when I trying to get access to GPUs during my PhD time and also my state at all time.”
Claim: Jasper Zhang experienced substantial difficulty accessing GPUs during his PhD.
“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.”
Claim: Jasper Zhang wanted AI teams building or using AI in the future not to be constrained by compute.
“And so we decided to build Hyperbolic, which is the on-demand AI cloud made for developers so everyone can get fast, affordable access to compute and inference.”
“On Friday, so I like participating different math Olympians in the past, won a few medals,”
Claim: Jasper Zhang has participated in several math Olympiads and won a few medals.
“and I have a lot of friends who are actively involved in IMO.”
“And so I was just chatting with my friends on Friday and around like 3 p.m., one friend told me that, China team won the IMO again and also DeepMind also won the gold medal.”
“And so I just started posting on X. I mean, I try to let everyone knows the news.”
Claim: Jasper Zhang posted on X to inform people about the reported IMO results.
“Some people get excited, but then never confirmed by DeepMind.”
Claim: DeepMind had not confirmed the reported IMO result at the time Jasper Zhang posted about it.
“And so it's a little bit weird because I thought DeepMind would be the first one to kind of announce that news.”
Claim: Jasper Zhang initially expected DeepMind to be the first to announce its IMO result.
“And then at 1 a.m. Saturday, OpenAI starting posting, a lot of OpenAI people starting posting about them winning the IMO gold medal. and kind of like stole the spotlight.”
“And so I initially thought Google was just slow due to their marketing approval, like the process.”
“So I posted another one to just like share my thoughts and then I got pinged from Google, like someone from Google just told me that it's actually like IMO and Google themselves need extra time to verify.”
“Why did mine need to verify but then OpenAI didn't need to do that they can just release and then it turns out like OpenAI actually didn't involve officially with IMO they just like use the problems but and then just like use their model to test. The results and it asked like three previous IMO medalists to review them.”
“I think I read the proof that it's still correct, but it's just like less official.”
Claim: Jasper Zhang thought the proof was correct, but considered the result less official.
“And that's why people kind of like kind of open up with receive a few backlash over the weekend and on Monday DeepMind officially confirmed they have the gold medal. And also fully verified by AMO.”
Claim: DeepMind officially confirmed its IMO gold medal on Monday, and AMO fully verified the result.
“What matters is that they have a model, both labs independently achieved a model that reasons in natural language without internet, without tools,”
“which I think, you know, this time last year, we didn't think was possible.”
“Yeah, so I have a feeling that this year there is like an AI model can win the IMO gold medal, because last year by using like formal verification, formal language, Google DeepMind can already won a silver medal.”
“Yeah, so I have a feeling that this year there is like an AI model can win the IMO gold medal, because last year by using like formal verification,”
Claim: Jasper Zhang expected that an AI model could win an IMO gold medal that year.
“Yeah, so I have a feeling that this year there is like an AI model can win the IMO gold medal, because last year by using like formal verification,”
“Yeah, so I have a feeling that this year there is like an AI model can win the IMO gold medal, because last year by using like formal verification, formal language, Google DeepMind can already won a silver medal.”
“the top tier competition for high school students,”
Claim: The International Mathematical Olympiad (IMO) is a top-tier competition for high school students.
“the top tier competition for high school students,”
Claim: The International Mathematical Olympiad is a top-tier competition for high-school students.
“It doesn't require you to really understand like the advanced math. It's basically it's problems about simple knowledge like common mechanics number theory geometry and algebra but then it kind of require you to have very strong problem-solving skills you need to know how to do a contradiction you can know how to create like counter examples you need to do like observation etc and so people treat this as like the one of the”
“It doesn't require you to really understand like the advanced math.”
“It's basically it's problems about simple knowledge like common mechanics number theory geometry and algebra but then it kind of require you to have very strong problem-solving skills you need to know how to do a contradiction you can know how to create like counter examples you need to do like observation etc and so people treat this as like the one of the”
“simple knowledge like common mechanics number theory geometry and algebra but then it kind of require you to have very strong problem-solving skills you need to know how to do a contradiction you can know how to create like counter examples you need to do like observation etc and so people treat this as like the one of the”
“simple knowledge like common mechanics number theory geometry and algebra but then it kind of require you to have very strong problem-solving skills you need to know how to do a contradiction you can know how to create like counter examples you need to do like observation etc and so people treat this as like the one of the the bar for AI to hit before they become the real mathematicians in the future.”
“the bar for AI to hit before they become the real mathematicians in the future.”
“So last year Google already won the silver medal and it seems to me that they already figured out a way to To make it work, it's just like need more time, a little more resources, a little more data, a little more compute.”
“So last year Google already won the silver medal and it seems to me that they already figured out a way to To make it work, it's just like need more time, a little more resources, a little more data, a little more compute.”
“I would say Google will win gold medal.”
Claim: Jasper Zhang expected Google to win an IMO gold medal.
“I would say Google will win gold medal.”
Claim: The speaker predicts that Google will win an IMO gold medal.
“What surprised me is this time they don't use formal language, but instead they just use LLM.”
“What surprised me is this time they don't use formal language, but instead they just use LLM.”
“And so last year when they try to do the IMO, they need like a... like a human to kind of translate the natural language province to lean and then they use lean to kind of prove the the the province to prove the solve the province and and this year no longer need need that and the same for open eye too”
“And so last year when they try to do the IMO, they need like a... like a human to kind of translate the natural language province to lean and then they use lean to kind of prove the the the province to prove the solve the province and and this year no longer need need that and the same for open eye too”
“I would say different problems having different skills.”
Claim: Different IMO problems assess different mathematical skills.
“For example, like the, if you look at the problem one, we can start from problem one. It's 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 uh 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 uh for any n greater than three like let's say n equal to five you can”
“the all the possibilities for different cases like for different n uh 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 uh for any n greater than three like let's say n equal to five you can reduce the problem to n equal to 4 and reduce the problem to n equal to 3 and”
“so this is there are different ways to do this like induction but like Google has one method and then open AI AI also have another method but both kind of works basically you just reduce any n to 3”
“And then you just do case-by-case analysis for n equals 3.”
Claim: The described solution method handles the n = 3 case through case-by-case analysis.
“And so I'll say this is probably not that challenging for if you are very good like math Olympians participants,”
“but it kind of surprised me that AI can kind of come up with this like ideas.”
Claim: The speaker was surprised that AI could generate the mathematical ideas used in the solution.
“and I realized that IMO kind of like it's a good exam to test certain aspects of math skills, which is like problem solving or you need to have like really complete chain of thoughts, like logic, et cetera.”
“But it doesn't test like your creativity in terms of like research.”
Claim: The IMO does not assess a person's creativity in mathematical research.
“It doesn't test your capabilities of doing conjectures.”
Claim: The IMO does not assess a person's ability to formulate mathematical conjectures.
“It doesn't test your capabilities of learning like advanced knowledge or like applying advanced knowledge.”
Claim: The IMO does not assess a person's ability to learn or apply advanced mathematical knowledge.
“And so I think 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 brand teaser style.”
Claim: The speaker characterizes most IMO problems as more like brain teasers.
“So like you can solve them, but it doesn't mean that you are good mathematicians.”
Claim: Solving IMO problems alone does not establish that someone is a good mathematician.
“I mean, I can feel the AGI vibe from the solutions,”
Claim: The speaker perceives an AGI-like quality in the AI-generated mathematical solutions.
“but I think we're still not there.”
Claim: The speaker thinks AI has not yet reached artificial general intelligence (AGI).
“I mean CMO is Chinese method Olympiad and so In terms of difficulty, CMO is kind of similar to IMO.”
“In terms of difficulty, CMO is kind of similar to IMO.”
“I would say it's super competitive in China.”
Claim: The Chinese Mathematical Olympiad (CMO) is highly 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 then like getting getting the gold medal IMO. And so so it's similar.”
“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 then like getting getting the gold medal IMO. And so so it's similar.”
“uh it's it's all about probability like there's so many people can compete as CMO and so like a lot of students are pretty good but just like six people um were selected”
Claim: Many students compete in the CMO, and only six are selected despite many being strong competitors.
“uh it's it's all about probability like there's so many people can compete as CMO and so like a lot of students are pretty good but just like six people um were selected”
“Yeah, so I'll say so for IMO they're like for four categories like algebra combinatorics geometry number theory usually combinatorics is kind of more the most challenging and creative especially for AI so like at one time I was at like this conference which is Frontiers Math Symposium so basically they invited like 30 to 40 mathematicians to kind of assess the capabilities of Alpha Mini High and many other advanced AIs.”
Claim: The four IMO problem categories are algebra, combinatorics, geometry, and number theory.
“for four categories like algebra combinatorics geometry number theory usually combinatorics is kind of more the most challenging and creative especially for AI so like at one time I was at like this conference which is Frontiers Math Symposium so basically they invited like 30 to 40 mathematicians to kind of assess the capabilities of Alpha Mini High and many other advanced AIs.”
“for four categories like algebra combinatorics geometry number theory usually combinatorics is kind of more the most challenging and creative especially for AI so like at one time I was at like this conference which is Frontiers Math Symposium so basically they invited like 30 to 40 mathematicians to kind of assess the capabilities of Alpha Mini High and many other advanced AIs.”
“Yes, we realize that if it's like a textbook stuff or like step-by-step problem, then AI can solve it.”
Claim: AI systems can solve textbook-style problems and problems that proceed step by step.
“if we require creativity, especially like in computer science, you kind of need to create some example and then try to prove them.”
“uh that is the minimal bound or like the upper bound it's the lower bound of the upper bound then ai kind of sucks at that and so i think um this is why no ai can solve the last problem but it also is super hard for human as well 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”
Claim: The last problem of the International Mathematical Olympiad is also extremely difficult for humans.
“uh that is the minimal bound or like the upper bound it's the lower bound of the upper bound then ai kind of sucks at that and so i think um this is why no ai can solve the last problem but it also is super hard for human as well 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 discompose a problem into several steps and then you know that if you can solve each step then you can solve the whole problem but then for the last problem you kind of need to do a lot of uh experiments or like you need to look at the smaller examples and”
“uh that is the minimal bound or like the upper bound it's the lower bound of the upper bound then ai kind of sucks at that and so i think um this is why no ai can solve the last problem but it also is super hard for human as well 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 discompose a problem into several steps and then you know that if you can solve each step then you can solve the whole problem but then for the last problem you kind of need to do a lot of uh experiments or like you need to look at the smaller examples and”
Claim: Solving the last IMO problem requires extensive experimentation or examination of smaller examples.
“Try to create some examples, try to create some solutions for that small examples and try to figure out if you can prove it that is the minimal number.”
“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.”
Claim: A better benchmark for mathematics is needed.
“Most of the benchmarks that people are using right now is like AMI, IMO, USAIMO, all these like competition math problems. But like they just test like a certain aspect of the 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.”
“But like they just test like a certain aspect of the 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 human to become practitioners 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”
“for human to become practitioners 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”
“skills into three categories. So one is mathematical knowledge and understanding. And then the second is like problem solving and communication. and then lastly it's like learning meta skills and creativity so you need to know how to learn new knowledge you need to know how to you need to how to think abstractly and then transfer tools across domains for example like you want to use probabilistics method in carbon nectarist then you kind of know how to do this transfer learning stuff”
“And so you need to know all the math knowledge, like definition, theories, lemmas, etc.”
“And you also need to understand theories, 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,”
Claim: The speaker says mathematical ability requires calculation skills and analytical skills.
“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 problem solving and communication probably is the the most skills that you require”
“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 problem solving and communication probably is the the most skills that you require”
“and then lastly it's like learning meta skills and creativity so you need to know how to learn new knowledge you need to know how to you need to how to think abstractly and then transfer tools across domains for example like you want to use probabilistics method in carbon nectarist then you kind of know how to do this transfer learning stuff”
“And in mathematical modeling, you need to know how to translate real-world scenarios into formal mathematical models and then generalization,”
“which is you look at a few examples and you immediately come up with an idea, I can generate this to a more powerful theorem and see if I can prove that.”
“And one very important piece of mathematician is that creativity.”
Claim: The speaker considers creativity a very important component of being a mathematician.
“so you need to very very creative like when you look at look at one object or one example then you basically say okay now I think I can invent some new methods and you can invent some new theory and lastly it's 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 lines are parallel or these two lines are perpendicular or even just look at algebra problems and you know like okay this”
“look at one object or one example then you basically say okay now I think I can invent some new methods and you can invent some new theory and lastly it's 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 lines are parallel or these two lines are perpendicular or even just look at algebra problems and you know like okay this This group has this structure.”
“And so those are like the main pieces I think will define a mathematician.”
“for the logical thinking and reasoning, I think we can, a lot of people trying to use lean, because like Our AI work super well for very fine-tuned one, and so if we can just use Ling to kind of become the verifier, then it's easy.”
“So I think we probably will see very powerful reasoning models in math very soon.”
“But then for creativity, this is a little bit hard because there is no measurement to...”
Claim: The speaker says creativity is difficult to assess because there is no measurement for it.
“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 problem in aisle 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 in terms of creativity and and just like in it times you need like specific domain knowledge to kind of create this reward”
“And I think I started seeing more and more mathematicians working together with AI scientists, researchers,”
Claim: The speaker says mathematicians are increasingly working with AI scientists and researchers.
“and I think this is a good combo because if you are just like AI 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.”
“But then if you're just a mathematician, you maybe know the concept, but you don't know how to apply that to AI research.”
“research and so so basically I think we'll see we will start seeing more and more mathematicians working together with AI scientists and my my guess I mean different people have different opinions and then my guess is I believe in IL so if for each category we can figure out the way to auto evaluate the results Then after that, it would just be compute and data.”
“We probably will publish the first draft, first version in a few weeks.”
Claim: The speaker predicts that the first draft of the benchmark will be published in a few weeks.
“a sub-frontier math still problem focused, but then I think we need the more skills breakdown.”
Claim: The speaker thinks mathematics needs a more detailed breakdown of skills.
“hyperbolic, the goal of hyperbolic is that we want to democratize AI innovation and try to accelerate AI evolution.”
Claim: Hyperbolic's goal is to democratize AI innovation and accelerate the evolution of AI.
“And so I would position this as a hobby project.”
Claim: The speaker characterizes the project as a hobby project.
“we will probably give people some credits if they actually can solve, we'll give some researchers some GPU credits if they can actually solve some problems in the benchmark.”
Claim: The project will probably award researchers GPU credits for solving problems in its benchmark.
“Yeah, I think different approach have different challenges.”
Claim: Different approaches to AI mathematics have different challenges.
“Natural language is easier to gather data but harder to verify but”
“it's more human readable right for lean they're not enough data for lean right they're like probably 1 million tokens in 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 if we really can reach like 1 trillion token I think then you can start”
“it's more human readable right for lean they're not enough data for lean right they're like probably 1 million tokens in 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 if we really can reach like 1 trillion token I think then you can start”
Claim: Some professors and PhD researchers are working toward building a very large Lean dataset.
“it's more human readable right for lean they're not enough data for lean right they're like probably 1 million tokens in 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 if we really can reach like 1 trillion token I think then you can start”
Claim: Natural-language reasoning is more human-readable than the alternative being discussed.
“it's more human readable right for lean they're not enough data for lean right they're like probably 1 million tokens in 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 if we really can reach like 1 trillion token I think then you can start doing some cool AI training on top of that um 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 even use Lean and can solve that.”
Claim: The speaker was surprised that OpenAI and Google DeepMind solved the IMO problem without using Lean.
“like AI neural networks is basically a black box and it's like experimental science.”
“prediction whether we will first see like a mathematician AI built on top of Lean or built on top of natural language but by general I feel like both approaches might should work and I think mathematicians would like both of them”
“prediction whether we will first see like a mathematician AI built on top of Lean or built on top of natural language but by general I feel like both approaches might should work and I think mathematicians would like both of them”
“I know some professors in London are trying to using Bing to write the proof for Fermat's last theorem.”
Claim: Some professors in London are attempting to use Bing to produce a proof of Fermat's Last Theorem.
“And so that's pretty impressive if you can do it.”
“I would say it's i think definitely possible um like”
Claim: The speaker thinks it is definitely possible to formalize a proof of Fermat's Last Theorem in Lean.
“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 he's he's hoping to finish that in like two or three years and uh and then basically like if ling is not complete then he can just build more more libraries on top of that so so everything is doable it's just time”
Claim: The speaker believes the Lean formalization work is achievable and mainly requires time.
“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 he's he's hoping to finish that in like two or three years and uh and then basically like if ling is not complete then he can just build more more libraries on top of that so so everything is doable it's just time”
“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 he's he's hoping to finish that in like two or three years and uh and then basically like if ling is not complete then he can just build more more libraries on top of that so so everything is doable it's just time”
“And I think he's got time and he got resources.”
Claim: The speaker believes Kevin Buzzard has the time and resources to pursue the Lean proof project.
“I feel like a lot of AI, like a lot of AI models built in industry is just like a bigger scale of like research results.”
Claim: The speaker thinks many industry-built AI models primarily scale up existing research results.
“They, probably they will use like existing research, but it's just more. More like larger scale, more systematic and more data.”
“I mean, I know when I read like the Google DeepMind report, they said they can now do like parallel thinking. Basically, the model can.”
Claim: According to the Google DeepMind report the speaker read, its model can perform parallel thinking.
“can like parallelly try different new ideas they try to like leverage more multi-step reasoning sorry they would try to like figure out new reinforcement learning techniques that could leverage multi-step reasoning I think that's probably like a very important important step I know I was pretty bad at multi-step but now seems like they figure out a way to kind of”
“can like parallelly try different new ideas they try to like leverage more multi-step reasoning sorry they would try to like figure out new reinforcement learning techniques that could leverage multi-step reasoning I think that's probably like a very important important step I know I was pretty bad at multi-step but now seems like they figure out a way to kind of”
“can like parallelly try different new ideas they try to like leverage more multi-step reasoning sorry they would try to like figure out new reinforcement learning techniques that could leverage multi-step reasoning I think that's probably like a very important important step I know I was pretty bad at multi-step but now seems like they figure out a way to kind of”
“can like parallelly try different new ideas they try to like leverage more multi-step reasoning sorry they would try to like figure out new reinforcement learning techniques that could leverage multi-step reasoning I think that's probably like a very important important step I know I was pretty bad at multi-step but now seems like they figure out a way to kind of train using AI for multi-step reasoning and I think that's like pretty impressive in terms of the solution and”
Claim: The speaker thinks researchers have found a way to use AI training to develop multi-step reasoning.
“But then I would say none of this will probably worth like the best paper at NeurIPS,”
Claim: The speaker thinks these techniques probably would not merit the best paper award at NeurIPS.
“but it's more about like you just be the best in terms of each technique and just get more data, get more compute.”
“yeah i think it's reasonably known that deepthink and o3 pro and grok4 heavy are all like parallel thinking right like they all just run like 10 different variations of the same model and then they have a judge model choose the best result i yeah i'm not sure like i think that the existence proof that there's been something qualitatively different”
“really different is the is the wall clock time going from 60 hours to to you know under 45 that's that's an order of magnitude change and it is not that typically that is not achieved by scaling up existing ideas you have to just do new ideas because this is a it's an efficiency issue”
“really different is the is the wall clock time going from 60 hours to to you know under 45 that's that's an order of magnitude change and it is not that typically that is not achieved by scaling up existing ideas you have to just do new ideas because this is a it's an efficiency issue”
“it one order of magnitude better i don't think so it's like two times better”
Claim: The speaker estimates that a B200 GPU is about 2× better, not 10× better.
“yes uh so i would say 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 the same for any any any job too it kind of give you a like a benchmark or like a like a matrix to see how good these model are but you really need to put them into the battlefield right and the goal of a mathematician is you want to push forward the frontier of math”
“like a matrix to see how good these model are but you really need to put them into the battlefield right and the goal of a mathematician is you want to push forward the frontier of math”
Claim: The speaker says a mathematician's goal is to advance the frontier of mathematics.
“And so I would say the next step is trying to solve some open problems that's like open for 30 years, 50 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 I define math AGI.”