lm-provers/QED-Nano

Text Generation • 4B • Updated about 6 hours ago • 169 • 45

Note A compact 4B model that can write Olympiad-level proofs through extended reasoning

lm-provers/QED-Nano-SFT

Text Generation • 4B • Updated 1 day ago • 11 • 3

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.