Powerful math reasoning models will arrive soon using Lean as a verifier
Dr. Jasper Zhang · ⚡️Math Olympiad gold medalist explains OpenAI and Google DeepMind IMO Gold Performances · Jul 24, 2025 · at 19:37
Dr. Jasper Zhang explains how formal proof assistants like Lean enable effective reinforcement learning for logical math reasoning.
0:00 / 0:11exact quote · 11.9s
▶ Watch the full episode on YouTube → 720p mp4 · rendered on demand · StarZero watermark
“And so if you can just use lean to kind of become the verifier, then it's easy. So I think we probably will see very powerful reasoning models in, in math very soon.”
quote is from the automated transcript, cleaned for reading: filler sounds and stutters are removed, nothing is rephrased. names can be misheard (the analysis reads context, assessments check outside sources). how →
More from Dr. Jasper Zhang
OpenAI's IMO performance was not officially verified by the IMO
“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 ask, like, three previous IMO analysts to review them.”
Scaling math AI becomes purely compute and data once auto-evaluation works
“And then my guess is, I believe in IL, so 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.”
Formalizing Fermat's Last Theorem in Lean is doable in 2-3 years
“It's I think definitely possible. Yeah. Like he, so the professor is Kevin buzzard and he got like a grant and now he just like focused on writing the proof for Ling. Like he's hoping to finish that in like two or three years. And then basically like if Ling i…”
Zhang confirms OpenAI's unverified IMO proofs are mathematically correct
“I read the proof that it's still correct, but it's just, like, less official, and that's why people kind of, like, kind of OpenAI received a few backlash over the weekend, and on Monday, DeepMind officially confirmed they have the gold medal and also fully ver…”
AI models fail at creative combinatorics problems requiring example construction
“If it's like a textbook stuff or like a step-by-step problem, then AI can solve it. But, however, if it requires, like, creativity especially, like, in combinatorics, you kind of need to create, ah, some example, and then try to prove them, ah, that it's the m…”
Industry AI progress stems from scaling existing research systematically
“A lot of AI like, a lot of AI models built in industry is just, like, a bigger scale of, like in like, research results. They probably they will use, like, existing research, but it's just more, more, like, larger scale, more systematic and more data.”