Atlas

Models

← All models

QED-Nano

LM-Provers · 2026-02-12 · 4B parameters

QED-Nano is a dense 4-billion-parameter theorem-proving checkpoint based on Qwen3-4B-Thinking-2507 and post-trained with supervised fine-tuning and reinforcement learning on Olympiad-level proof problems. Its separately evaluated agent scaffold can scale inference-time computation up to two million tokens per problem, but the released model itself is the checkpoint recorded here.

Benchmark scores

BenchmarkScore
AIME 202577.5
AIME 202682.5
Apex (MathArena)1.6
Apex Shortlist22.3
ArXivMath 01/202637.0
ArXivMath 02/202614.1
ArXivMath 12/202526.5
BRUMO 202587.5
Capability138.5
CMIMC 202559.4
Final-Answer Comps — Overall42.7
HMMT Feb 202576.7
HMMT Feb 202664.4
HMMT Nov 202575.0
SMT 202579.7
Loading Atlas data…