Teaching Tiny Models to Prove Hard Theorems | Lewis Tunstall | HF ML Club India EP1

About the speaker: Lewis Tunstall is a Machine Learning Engineer at Hugging Face, where he leads the research team's efforts to develop open-source tools and recipes for post-training LLMs. He's the co-developer of popular models such as Zephyr and SmolLM3, as well as large-scale community projects like Open R1. Lewis is also the co-author of widely read technical content like The Smol Training Playbook, O'Reilly's NLP with Transformers book, and Hugging Face's NLP course. About the talk: Can we train small language models to solve hard Olympiad-level proof problems at a level close to large frontier models such as Gemini 3 Pro? Surprisingly, the answer is yes! In this talk, I'll discuss the training of QED-Nano; a compact 4B model post-trained to write Olympiad-level mathematical proofs entirely in natural language. I'll discuss our multi-stage training recipe, the challenges with doing long-horizon RL, and how we scaled inference-time compute to enable the model to reason for millions of tokens per proof. Resources: Gemini Meeting Notes - https://docs.google.com/document/d/1kBzjEUA4TDY1grL8Jmt7Y4hJBLpQc698YKl8vgKD-50/edit?usp=drive_link Join the club: https://huggingface.co/hf-ml-club-india Follow socials for more updates: x.com/ariG23498 x.com/RisingSayak x.com/_lewtun