# QED-Nano: Teaching a Tiny Model to Prove Hard Theorems

arXiv: https://arxiv.org/abs/2604.04898 · HTML: https://mlsanity.com/paper/2604.04898/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 29 of its 41 references that are in the map.
- First posted on arXiv 6 Apr 2026.

## Builds on (most cited first, 29 of 29)

- [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://mlsanity.com/paper/2402.03300/) (2024)
- [DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning](https://mlsanity.com/paper/2501.12948/) (2025)
- [Tree of Thoughts: Deliberate Problem Solving with Large Language Models](https://mlsanity.com/paper/2305.10601/) (2023)
- [Scaling LLM Test-Time Compute Optimally can be More Effective than Scaling Model Parameters](https://mlsanity.com/paper/2408.03314/) (2024)
- [Humanity's Last Exam](https://mlsanity.com/paper/2501.14249/) (2025)
- [Rubrics as Rewards: Reinforcement Learning Beyond Verifiable Domains](https://mlsanity.com/paper/2507.17746/) (2025)
- [MathArena: Evaluating LLMs on Uncontaminated Math Competitions](https://mlsanity.com/paper/2505.23281/) (2025)
- [The False Promise of Imitating Proprietary LLMs](https://mlsanity.com/paper/2305.15717/) (2023)
- [FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI](https://mlsanity.com/paper/2411.04872/) (2024)
- [AIMO-2 Winning Solution: Building State-of-the-Art Mathematical Reasoning Models with OpenMathReasoning dataset](https://mlsanity.com/paper/2504.16891/) (2025)
- [Optimizing Test-Time Compute via Meta Reinforcement Fine-Tuning](https://mlsanity.com/paper/2503.07572/) (2025)
- [Common 7B Language Models Already Possess Strong Math Capabilities](https://mlsanity.com/paper/2403.04706/) (2024)
- [DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning](https://mlsanity.com/paper/2511.22570/) (2025)
- [Winning Gold at IMO 2025 with a Model-Agnostic Verification-and-Refinement Pipeline](https://mlsanity.com/paper/2507.15855/) (2025)
- [Proof or Bluff? Evaluating LLMs on 2025 USA Math Olympiad](https://mlsanity.com/paper/2503.21934/) (2025)
- [Towards Robust Mathematical Reasoning](https://mlsanity.com/paper/2511.01846/) (2025)
- [e3: Learning to Explore Enables Extrapolation of Test-Time Compute for LLMs](https://mlsanity.com/paper/2506.09026/) (2025)
- [Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics](https://mlsanity.com/paper/2601.14027/) (2026)
- [Step 3.5 Flash: Open Frontier-Level Intelligence with 11B Active Parameters](https://mlsanity.com/paper/2602.10604/) (2026)
- [Recursive Self-Aggregation Unlocks Deep Thinking in Large Language Models](https://mlsanity.com/paper/2509.26626/) (2025)
- [PipelineRL: Faster On-policy Reinforcement Learning for Long Sequence Generation](https://mlsanity.com/paper/2509.19128/) (2025)
- [The Open Proof Corpus: A Large-Scale Study of LLM-Generated Mathematical Proofs](https://mlsanity.com/paper/2506.21621/) (2025)
- [Brains vs. Bytes: Evaluating LLM Proficiency in Olympiad Mathematics](https://mlsanity.com/paper/2504.01995/) (2025)
- [Reliable Fine-Grained Evaluation of Natural Language Math Proofs](https://mlsanity.com/paper/2510.13888/) (2025)
- [Reasoning Cache: Continual Improvement Over Long Horizons via Short-Horizon RL](https://mlsanity.com/paper/2602.03773/) (2026)
- [Scaling Generative Verifiers For Natural Language Mathematical Proof Verification And Selection](https://mlsanity.com/paper/2511.13027/) (2025)
- [Project Aletheia: Verifier-Guided Distillation of Backtracking for Small Language Models](https://mlsanity.com/paper/2601.14290/) (2026)
- [Solving a Research Problem in Mathematical Statistics with AI Assistance](https://mlsanity.com/paper/2511.18828/) (2025)
- [Lattice-Valued Bottleneck Duality](https://mlsanity.com/paper/2410.00315/) (2024)

## Built on by (most cited first, 3 of 3)

- [Recursive Agent Optimization](https://mlsanity.com/paper/2605.06639/) (2026)
- [Trust the Critic More](https://mlsanity.com/paper/2609.39247/) (2026)
- [Splicing Hints into Reasoning Traces: Learning from Demonstrator Failures](https://mlsanity.com/paper/2610.13996/) (2026)

## Abstract (arXiv)

Proprietary AI systems have recently demonstrated impressive capabilities on complex proof-based problems, with gold-level performance reported at the 2025 International Mathematical Olympiad (IMO). However, the training pipelines behind these systems remain largely undisclosed, and their reliance on large "internal" models and scaffolds makes them expensive to run, difficult to reproduce, and hard to study or improve upon. This raises a central question: can small, open models also be trained to achieve competitive reasoning performance on difficult Olympiad-level math? In this paper, we answer this question by building QED-Nano, a 4B model post-trained for Olympiad-level proofs. Our training recipe has three stages: (1) supervised fine-tuning to imbue good proof-writing styles by distilling from DeepSeek-Math-V2, (2) reinforcement learning (RL) with rubric-based rewards, and (3) expanding RL with a reasoning cache, which decomposes long proofs into iterative summarize-and-refine cycles and enables stronger test-time reasoning. QED-Nano surpasses the proof-generation performance of much larger open models, including Nomos-1 and GPT-OSS-120B, and approaches the performance of proprietary models like Gemini 3 Pro, at a fraction of the inference cost. To support further research on open mathematical reasoning, we release the full QED-Nano pipeline, including the QED-Nano and QED-Nano-SFT models, the FineProofs-SFT and FineProofs-RL datasets, and the training and evaluation code.