lm-provers/QED-Nano
TEXT GENERATIONConcurrency Cost:1Model Size:4BQuant:BF16Ctx Length:32kPublished:Feb 12, 2026License:apache-2.0Architecture:Transformer0.1K Open Weights Warm
QED-Nano is a 4 billion parameter model developed by lm-provers, explicitly post-trained to excel at proof-writing. Based on Qwen3-4B-Thinking-2507, it achieves an impressive 40% on the IMO-ProofBench benchmark, matching GPT-OSS-120B. This model is uniquely optimized for mathematical reasoning and theorem proving, leveraging an agentic scaffold for enhanced performance.
Loading preview...
QED-Nano: A Specialized Proof-Writing Model
QED-Nano is a 4 billion parameter model from lm-provers, specifically post-trained to enhance its capabilities in writing mathematical proofs. Despite its relatively small size, it demonstrates strong performance on challenging benchmarks, making it a notable model for domain-specific reasoning tasks.
Key Capabilities
- Exceptional Proof-Writing: Achieves a 40% score on the IMO-ProofBench benchmark, a significant +20% improvement over its Qwen3 base model, and matches the performance of much larger models like GPT-OSS-120B.
- Agentic Scaffold Integration: Utilizes an agent scaffold that scales inference-time compute to over 1 million tokens per problem, allowing it to approach the performance of Gemini-3-Pro in certain configurations.
- Specialized Training: Post-trained using a combination of supervised fine-tuning and reinforcement learning with a reasoning cache on a diverse set of Olympiad proof problems.
Good for
- Automated Theorem Proving: Ideal for tasks requiring rigorous mathematical proof generation.
- Mathematical Research Assistance: Can serve as an assistive tool for researchers and students working on complex mathematical problems.
- Domain-Specific Reasoning: Excels in highly specialized reasoning domains where logical deduction and proof construction are paramount.