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.
Figures & tables
Figure 1: IMO-ProofBench ( Luong et al., 2025 ) grade as a function of model size. QED-Nano outperforms open models of similar size and remains competitive with much larger systems.
Figure 2: Example of a grading scheme.
Figure 3: RL training curves with rubric-based rewards (left) and corresponding evaluation metrics on IMO-ProofBench and ProofBench (right)
Figure 4: Training reward as a function of optimization steps for standard RL and RL with RC.
Figure 5: Per-turn mean reward during RC training.
Figure 6: Average grade on IMO-ProofBench versus RC turns.
Model
IMO-ProofBench
ProofBench
IMO-AnswerBench
Qwen3-4B-Thinking-2507
20.4 (2.6)
19.5 (0.9)
55.8
QED-Nano (SFT initialization only)
39.5 (2.9)
33.3 (0.5)
57.5
QED-Nano
40.0 (0.6)
44.9 (3.4)
67.5
QED-Nano (+ RSA test-time scaffold)
56.9 (5.9)
62.6 (4.0)
76.5
Qwen3-30B-A3B-Thinking-2507
27.6 (1.0)
26.1 (2.4)
67.0
Qwen3-235B-A22B-Thinking-2507
34.1 (0.7)
33.7 (1.1)
70.5
Table 1: Comparison of QED-Nano (4B) with leading open- and closed-source models on IMO-ProofBench, ProofBench, and IMO-AnswerBench benchmarks. We report the avg@3 grade (%) for the proof-based benchmarks to account for their relatively small size compared to IMO-AnswerBench.
Scaffold
Avg. grade (%)
Avg. tokens
Tokens vs. single turn
Single Turn
40.0
93,690
1.00 ×
Reasoning Cache (training)
44.0
237,379
2.53 ×
DeepSeek Math
54.0
1,605,879
17.14 ×
RSA
56.9
2,045,764
21.84 ×
Table 2: Comparing test-time scaffolds with QED-Nano on IMO-ProofBench, illustrating a trade-off between token usage and performance. In geeneral, we observe that the RSA and DeepSeekMath scaffolds are the most performant, with RSA needing more tokens but attaining the best performance.
Model
Summary of proof style by human annotator
QED-Nano
QED-Nano typically produces proofs that are well structured, explicit, and easy to follow. Its main stylistic weakness is a strong preference for computation-heavy arguments for geometry problems.
QED-Nano + scaffold
The scaffold version is stylistically very similar to the standalone model. The model mainly seems to improve over QED-nano on questions where QED-nano made significant, but fixable mistakes.
Qwen-3-4B-Think
The base model often writes proofs that frequently contain obvious flaws such as circular reasoning, unjustified simplifications, and other errors that are clearly related to its overoptimization for final answer performance.
Nomos-1
Nomos-1 has a much more concise, direct style. This can read elegantly but also makes hidden mistakes harder to detect.
Table 3: Qualitative summary of the proof-writing style of the models.
Appendix figures & tables5 assets
Supplementary material from the paper’s appendix.
Appendix
Model
Simple
OPC
ProofBench
ProofBench Strict
GIMO
GPT-OSS-20B-medium
1.56
1.57
1.43
1.21
1.36
Appendix
Table 4: Results on the MathArena grading benchmark. Lower is better.
Model
ProofBench Strict
ProofBench Strict (with ref)
GPT-OSS-20B-medium
1.19
1.26
GPT-OSS-20B-high
1.17
1.19
GPT-OSS-120B-medium
1.16
1.24
Appendix
Table 5: Results on our in-distribution grading benchmark. Lower is better.
Number of turns
Avg. grade (%)
Avg. tokens
3
40.0
261,892
5
42.4
434,367
7
54.0
578,928
Appendix
Table 6: Effect of scaling the number of turns for the reasoning cache on ProofBench.
Figure 7: Comparison between quantity and uniqueness in the SFT dataset.
Base model
LR
ProofBench ↑
Qwen3-4B Base
1×10−6
0.00 ± 0.00
3×10−6
0.29 ± 0.11
5×10−6
0.07 ± 0.07
1×10−5
0.21 ± 0.08
2×10−5
0.09 ± 0.09
3×10−5
0.19 ± 0.07
Appendix
Table 7: ProofBench results for the Qwen3-4B SFT sweeps. Rows are grouped by base model and separated by horizontal rules. Within each group, each row corresponds to one learning rate and reports the mean ± SEM over 75 graded ProofBench problems at the 620-step checkpoint; boldface marks the best learning rate within each base-model group.