QED-Nano: Teaching a Tiny Model to Prove Hard Theorems
Who needs 1T parameters? Olympiad proofs with a 4B model
Artifacts for the QED Nano release
Who needs 1T parameters? Olympiad proofs with a 4B model
Note A compact 4B model that can write Olympiad-level proofs through extended reasoning
Note A variant of Qwen3-4B-Thinking-2507, fine-tuned on reasoning traces from DeepSeek-Math-V2
Note The dataset used to train QED-Nano-SFT
Note The dataset used to train QED-Nano
Note IMOProofBench, a benchmark for mathematical theorem proving by Google we used in our evaluation.
Note Benchmark constructed by converting the original ProofBench benchmark to one for mathematical theorem proving.
Note A collection of all human annotations in MathArena. Used to decide on our RL grader.
Note An in-distribution benchmark for grading proofs constructed from our training data. Used to decide on our RL grader.